EMZETT.
Login

Emzett Wiki

Ada: Tasks, geschützte Objekte und Verträge

Properties1
tagsprogrammiersprachen, ada

4 Min. Lesezeit

Kurz: Nebenläufigkeit ist in Ada Teil der Sprache. Eine Task läuft parallel zum Hauptprogramm:

Teil des Kurses Ada

Kapitel 5 von 8 im Kurs Ada. Mit Fortschritt, Quiz und Zertifikat auf der Lernseite.

Tasks

Nebenläufigkeit ist in Ada Teil der Sprache. Eine Task läuft parallel zum Hauptprogramm:

with Ada.Text_IO; use Ada.Text_IO;
 
procedure Main is
 
   task type Arbeiter (Id : Positive; Anzahl : Positive);
 
   task body Arbeiter is
      Summe : Natural := 0;
   begin
      for I in 1 .. Anzahl loop
         Summe := Summe + I;
      end loop;
      delay 0.01 * Id;
      Put_Line ("Arbeiter" & Positive'Image (Id) & ": " & Natural'Image (Summe));
   end Arbeiter;
 
   A1 : Arbeiter (1, 10);
   A2 : Arbeiter (2, 100);
   A3 : Arbeiter (3, 1000);
begin
   null;   -- Hauptprogramm wartet automatisch auf seine Tasks
end Main;

Ausgabe:

Arbeiter 1:  55
Arbeiter 2:  5050
Arbeiter 3:  500500

Das Programm endet erst, wenn alle Tasks, die in ihm deklariert sind, fertig sind.

Rendezvous

Tasks kommunizieren über Entries (Rendezvous):

with Ada.Text_IO; use Ada.Text_IO;
 
procedure Main is
 
   task Puffer is
      entry Ablegen (X : Integer);
      entry Holen (X : out Integer);
   end Puffer;
 
   task body Puffer is
      Wert : Integer := 0;
   begin
      for I in 1 .. 3 loop
         accept Ablegen (X : Integer) do
            Wert := X;
         end Ablegen;
         accept Holen (X : out Integer) do
            X := Wert * 2;
         end Holen;
      end loop;
   end Puffer;
 
   Ergebnis : Integer;
begin
   for I in 1 .. 3 loop
      Puffer.Ablegen (I * 10);
      Puffer.Holen (Ergebnis);
      Put_Line (Integer'Image (Ergebnis));
   end loop;
end Main;

Ausgabe:

20
 40
 60

Geschützte Objekte

Ein protected object garantiert exklusiven Zugriff auf gemeinsame Daten – ohne explizite Sperren. Vier Tasks zählen gleichzeitig; ein declare-Block endet erst, wenn alle Tasks fertig sind:

with Ada.Text_IO; use Ada.Text_IO;
 
procedure Main is
 
   protected Zaehler is
      procedure Erhoehe;
      function Wert return Natural;
   private
      Stand : Natural := 0;
   end Zaehler;
 
   protected body Zaehler is
      procedure Erhoehe is begin Stand := Stand + 1; end Erhoehe;
      function Wert return Natural is (Stand);
   end Zaehler;
 
begin
   declare
      task type Zaehle;
      task body Zaehle is
      begin
         for I in 1 .. 1000 loop
            Zaehler.Erhoehe;
         end loop;
      end Zaehle;
      Gruppe : array (1 .. 4) of Zaehle;
   begin
      null;
   end;   -- der Block endet erst, wenn alle Tasks fertig sind
   Put_Line (Natural'Image (Zaehler.Wert));
end Main;

Ausgabe:

4000

Verträge (Ada 2012+)

Vor- und Nachbedingungen sowie Prädikate schreibt man direkt an die Deklaration. Mit -gnata prüft die Laufzeit sie:

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Assertions;
 
procedure Main is
   subtype Gerade is Integer with Dynamic_Predicate => Gerade mod 2 = 0;
 
   function Teile (A, B : Integer) return Integer
     with Pre  => B /= 0,
          Post => Teile'Result * B <= A;
 
   function Teile (A, B : Integer) return Integer is (A / B);
 
   function Wurzel (X : Natural) return Natural
     with Post => Wurzel'Result * Wurzel'Result <= X
                  and (Wurzel'Result + 1) * (Wurzel'Result + 1) > X;
 
   function Wurzel (X : Natural) return Natural is
      R : Natural := 0;
   begin
      while (R + 1) * (R + 1) <= X loop
         R := R + 1;
      end loop;
      return R;
   end Wurzel;
 
   G : Gerade := 4;
begin
   Put_Line (Integer'Image (Teile (17, 5)));
   Put_Line (Integer'Image (Wurzel (50)));
   Put_Line (Integer'Image (G));
   Put_Line (Integer'Image (Teile (1, 0)));
exception
   when Ada.Assertions.Assertion_Error => Put_Line ("Vertragsverletzung: Vorbedingung");
end Main;

Ausgabe:

3
 7
 4
Vertragsverletzung: Vorbedingung

Hinweis

Verträge werden nur mit gnatmake -gnata geprüft; ohne diesen Schalter ignoriert der Compiler sie. Für Beweise statt Tests dient SPARK mit dem Werkzeug GNATprove.

Merke

  • Tasks (task) laufen parallel; Rendezvous über entry und accept
  • protected-Objekte schützen gemeinsame Daten automatisch vor gleichzeitigem Zugriff
  • Ein declare-Block mit Tasks endet erst, wenn alle Tasks fertig sind
  • Verträge: Pre, Post, Prädikate und Invarianten; mit SPARK sogar beweisbar

Übungsaufgabe

Schreibe einen Producer/Consumer mit einem geschützten Puffer und zwei Tasks.

Quiz zur Selbstkontrolle

Weiter im Kurs

Zurück: Pakete, Generics und Objekte

Weiter: Container, Dateien und Zeit

Alle Kapitel: Ada im Überblick

Graphansicht

Backlinks