Knowledge & Learning/WISS_LERN.iso/doslern/computer/educard/bs___3.sti

Text File | 1992-03-04 | 71.9 KB | 2,207 lines

YCPAA #!!# - Synchronisation -
@CEInhalt

@CPDas Thema von BS___3 ist
die Synchronisation paralleler Prozesse.

Start mit ⌐Parallelität@BS___3¬
AHBAA #!!# Parallelität
@EH                 Synchronisation paralleler Prozesse
@HB
@HEParallelität
@HB
  a) Parallelität im engeren Sinn
     Unter Parallelität im engeren Sinn versteht man das gleichzeitige
     Ablaufen mehrerer Prozesse.

  b) Parallelität im weiteren Sinn
     Unter Parallelität im weiteren Sinn versteht man, daß Prozesse in
     beliebiger, nicht festgelegter Reihenfolge, die im Grenzfall
     sequentiell sein kann, ablaufen dürfen.

     Notation:@HA   PARBEGIN S1; S2; ...; Sn PAREND@HB

     Man darf dabei nicht annehmen, daß bei einem zweiten Durchlauf des
     Programms die gleiche Reihenfolge wie beim ersten Durchlauf
     eingehalten wird.
@HB  c) Darstellung paralleler Abläufe
     Es gibt versciedene Möglichkeiten, parallele Abläufe darzustellen.
     Dies sind unter anderem:

     - Schreibweise einer Programmiersprache

       @HA   PARBEGIN S1; S2; ...; Sn PAREND@HB

     - Beschreibung durch einen Präzedenzgraphen

                          @HAS1
              @HO┌───────────┼───────────┐
             \│/         \│/         \│/
              @HAS2          S3          S4
              @HO└───────────┼───────────┘
                         \│/
                          @HAS5

@HB      - Ordnungsrelation, zum Beispiel "<" = zeitlich vor

        @HAS1 < S2 < S5
        S1 < S3 < S5        @HB(siehe Präzedenzgraph von oben)@HA
        S1 < S4 < S5


           @HBsiehe auch ⌐Parallelismus@BS1¬

           @HBweiter mit ⌐Synchronisation II@BS___3¬
AHBAA #!!# Synchronisation II
@HENotwendigkeit der Synchronisation
@HB
Parallele Prozesse müssen synchronisiert werden, damit nicht mehrere
Prozesse gleichzeitig auf exklusive ⌐Betriebsmittel@BS1¬ zugreifen können,
so entstehende Fehler also ausgeschlossen sind.

Beispiel:
  2 parallele Prozesse haben die Anweisung @HAx := x + 1@HB
  Korrektes Ergebnis: @HAx := x + 1 + 1@HB
  Ohne Synchronisation könnte es passieren, daß beide Prozesse gleich-
  zeitig den Wert von x lesen, ihn um 1 erhöhen und abspeichern.
  Das Ergebnis wäre : @HAx := x + 1@HB

  Damit das korrekte Ergebnis zustande kommt, muß der gleichzeitige
  Zugriff auf den Wert x durch ⌐Synchronisation@BS1¬ ausgeschlossen werden.



@HEDefinition des Begriffs "Synchronisation"
@HB
Unter Synchronisation versteht man die gegenseitige zeitliche Abstimmung
paralleler Prozesse beim Zugriff auf gemeinsame exklusiv benutzbare
Betriebsmittel.

Die gegenseitige zeitliche Abstimmung bzw. den gegenseitigen zeitlichen
Ausschluß kann man dadurch erreichen, daß man Befehlsfolgen zu unteilbaren
Operationen zusammenfaßt, die nur sequentiell ablaufen können.

Eine andere Möglichkeit ist die des "kritischen Gebiets".







@HEDefinition des Begriffs "kritisches Gebiet"
@HB
Prozesse dürfen nicht gleichzeitig auf einen gemeinsamen Datenbereich oder
ein gemeinsames, exklusives Betriebsmittel zugreifen.

Der Programmabschnitt, in dem ein Prozeß einen solchen Zugriff vornimmt
(vornehmen will), heißt kritisches Gebiet.

Ein kritisches Gebiet ist dadurch gekennzeichnet, daß die Operationen in
solch einem Gebiet nur von einem einzigen Prozeß ausgeführt werden dürfen.
Ohne Synchronisationsmethoden könnten jedoch mehrere Prozesse gleichzeitig
auf ihnen arbeiten.

           @HBweiter mit ⌐Interrupts sperren@BS___3¬
AHBAA #!!# Interrupts sperren
@EH             Synchronisation durch Sperren von Interrupts
@HB
@HESperren von Interrupts
@HB
Befehle höherer Programmiersprachen bestehen aus mehreren Elementar-
operationen. Eine Synchronisationsmethode ist die, diese Befehle unteilbar
zu machen, das heißt wenn ein Befehl ausgeführt wird, so werden alle
dazugehörigen Elementaroperationen unmittelbar hintereinander ausgeführt.
Es kann nicht innerhalb des Befehls zu einem Prozeßwechsel kommen.

Bei Rechenanlagen mit nur einer CPU (siehe ⌐Systemkern@BS1¬) erfolgen
Prozeßwechsel auf Grund von ⌐Interrupt@BS2¬s. Um einen Befehl unteilbar zu
machen, muß man also diese Interrupts sperren.

Vorteil:

   - Diese Synchronisationsmethode ist bei Anlagen mit nur einer einzigen
     CPU anderen Verfahren vorzuziehen, da sie nicht so aufwendig ist.
@HBNachteile:

   - Das Sperren kann nicht jeder Benutzer machen, sondern darf nur von
     privilegierten Benutzern (Supervisor) gemacht werden.

   - Die Methode sollte nur angewendet werden, wenn zwischen dem Sperren
     und der Freigabe von Interrupts nur wenige einfache Operationen, die
     die CPU nur sehr, sehr kurz belegen, ausgeführt werden.

     Sonst könnten noch nicht behandelte Interrupts verloren gehen.

   - Die Methode ist nicht anwendbar auf Mehrprozessor-Systemen, da man
     nur die Interrupts des eigenen Prozessors sperren kann, aber nicht
     die der anderen.

                 weiter mit ⌐LOCK und UNLOCK@BS___3¬

                 siehe auch ⌐Unterbrechungssperre@BS2¬
AHBAA #!!# LOCK und UNLOCK
@EH                 Synchronisation durch LOCK und UNLOCK
@HB
LOCK und UNLOCK sind Befehle über die insbesondere Mehrprozessor-
Anlagen verfügen. Sie sind wie folgt definiert:

@HALock (x)
  LOCK : { IF x = 0 THEN x := 1
                    ELSE GoTo LOCK } ;             {...} = unteilbar

Unlock (x)
  UNLOCK : {x := 0};@HB

Die Variable x ist mit 0 initialisiert. Auf sie können alle Prozesse
zugreifen.




@HBBei dieser Synchronisationsmethode wird mit kritischen Gebieten
gearbeitet. Der Lock-Befehl kennzeichnet den Beginn des kritischen
Gebietes und der Unlock-Befehl dessen Ende.

     @HA    Lock (x);
           @HLkritisches Gebiet@HA
         Unlock (x);@HB

Beim Befehl Lock (x) wird die Variable x solange getestet bis sie den
Wert 0 hat. Ist x = 0, so wird x auf 1 gesetzt und der Prozeß betritt
das kritische Gebiet.
Andere Prozesse die jetzt in das kritische Gebiet wollen, bleiben in der
Warteschleife von Lock (x) hängen.
Erst wenn der Prozeß das kritische Gebiet verlassen hat, was er durch den
Unlock (x) Befehl anzeigt, kann ein anderer Prozeß das kritische Gebiet
betreten (durch Unlock (x) wurde x ja wieder auf 0 gesetzt).
Es kann auch nur genau einer wieder das kritische Gebiet betreten, da die
Abfrage bei Lock (x) unteilbar ist.
@HBVorteil gegenüber ⌐Interrupts sperren@BS___3¬:

   -  Diese Synchronisationsmethode kann sowohl auf Einprozessor- wie auch
      auf Mehrprozessor-Anlagen laufen.

Nachteile:

   - Phänomen des @HPbusy waiting@HB oder auch @HPpolling@HB genannt:
     Prozesse warten aktiv auf das Freiwerden des kritischen Gebietes.
     Sie belasten den Prozessor mit ihrer ständigen Abfrage, obwohl er
     inzwischen andere Arbeit erledigen könnte.

     Besser wäre es, wenn der wartende Prozeß stillgelegt würde und genau
     dann wieder aktiviert würde, wenn das kritische Gebiet wieder frei
     ist.



@HB   - Die Methode ist nicht sicher, d. h. sie kann zu ⌐Deadlock@BS1¬s führen.
     Beispiel:
       In einem System sind die Prozesse mit Prioritäten versehen und der
       Prozessor wir dem Prozeß mit höchster Priorität zugewiesen.
       Die Situation:

         Ein Prozeß niedriger Priorität befindet sich im kritischen Gebiet
         und möchte es verlassen, also die Unlock-Operation ausführen.
         Ein Prozeß höherer Priorität will das kritische Gebiet betreten.
         Er beschäftigt mit seiner Abfrage ständig die CPU und gibt dem
         Prozeß mit niedriger Priorität nie die Gelegenheit die CPU zu
         benutzen um x auf 0 zu setzen und damit das kritische Gebiet zu
         verlassen. Deadlock.

     Besser wäre es hier mit dynamischen Prioritäten zu arbeiten.
     Die Priorität des wartenden Prozesses wird in festen Zeitintervallen
     erniedrigt. Irgendwann hat der Prozeß die Möglichkeit, das kritische
     Gebiet zu verlassen.
@HEAnwendung in der Praxis
@HB
Auf Siemens Rechenanlagen der Serie 7000 gibt es für den LOCK-Befehl den
Maschinenbefehl Test-and-Set (TS (x)). Er ist unteilbar und arbeitet auf
der Adresse x. Er vergleicht den Inhalt der Speicherzelle mit der
Adresse x mit Null und hält das Ergebnis in einem Register fest. Ist der
Inhalt Null, so steht in dem Register eine 1 (für TRUE) und das Byte mit
der Adresse x wird Bit für Bit auf 1 gesetzt.

Die Programmierung sieht dann so aus:
@HA
  x := 0                          X      DC X,'00'
    :                                       :
    :                                       :
  Lock (x)                        LOOP:  TS X
                                         BZ LOOP
  @HLKritisches Gebiet                      Kritisches Gebiet@HA
  Unlock (x)                             MVI X, 0
@HBDie Anweisungsfolge
@HA
  TS X
  BZ LOOP
@HB
sperrt auch den Bus, deshalb ist die Verwendung von
@HA
  BZ BRANCH ON ZERO
@HB
besser.


          weiter mit ⌐Dekker@BS___3¬
AHBAA #!!# Dekker
@EH                       Synchronisation nach Dekker
@HB
Wie schon bei der ⌐Synchronisation@BS1¬ mit ⌐LOCK und UNLOCK@BS___3¬ erfolgt
diese auch hier mit Synchronisations-Variablen, also Sprachelementen, die
in allen Sprachen vorkommen.

Es werden im weiteren nur zyklisch, parallel arbeitende Prozesse
betrachtet, das heißt Prozesse bewerben sich immer gleichzeitig um das
selbe kritische Gebiet.









@HBBei der Lösung des Synchronisationsproblems müssen folgende Forderungen
beachtet werden:

  1. Die Lösung soll symmetrisch sein, das heißt die Prozesse sollen
     gleich aufgebaut sein.

  2. Die Arbeitsgeschwindigkeit der Prozesse darf keine Rolle spielen.

  3. Hält ein Prozeß außerhalb des kritischen Gebietes an (er stirbt), so
     darf er nicht die anderen Prozesse blockieren.

  4. Wollen mehrere Prozesse gleichzeitig das kritische Gebiet betreten,
     so darf dies nur genau einem erlaubt werden.

Die einzigen unteilbaren Operationen sind hier:
  a) Lesezugriff auf den Speicher
  b) Schreibzugriff auf den Speicher

@HESynchronisationslösung für 2 parallele Prozesse (nach Dekker)
@HA
VAR
s1, s2, Turn : Integer;
BEGIN
  s1 := 1;          @HB(* 1 bewirbt sich nicht              *)@HA
  s2 := 1;          @HB(* 2 bewirbt sich nicht              *)@HA
  Turn := 1;        @HB(* Kritisches Gebiet KG von 1 belegt *)@HA











  @HAPARBEGIN
    process_1 : CYCLE                process_2 : CYCLE
      BEGIN                            BEGIN
        s1 := 0;                         s2 := 0;    @HB(* Bewerbung um KG *)
@HA        WHILE s2 = 0 DO                  WHILE s1 = 0 DO
          IF Turn = 2 THEN                 IF Turn = 1 THEN
            BEGIN                            BEGIN   @HB(* Warten bis frei *)
@HA              s1 := 1;                         s2 := 1; @HB(* Bew. zurück  *)
@HA              WHILE Turn = 2 DO;               WHILE Turn = 1 DO;
              s1 := 0;                         s2 := 0; @HB(* Bew. um KG   *)
@HA            END;                             END;
        @HLKritisches Gebiet                Kritisches Gebiet; @HB(* hinein   *)
@HA        Turn := 2;                       Turn := 1;     @HB(* KG freigeben *)
@HA        remainder of cycle 1             remainder of cycle 2
      END;                             END;
  PAREND
END;
@HBMan kann den Algorithmus folgendermaßen beschreiben:

@HB  Bewirb dich um kritisches Gebiet.            @HAs1 := 0;
@HB  Hat der andere Prozeß sich beworben          @HAWHILE s2 = 0 DO
@HB  und ist im kritischen Gebiet,                @HA  IF Turn = 2 THEN
@HB  dann ziehe eigene Bewerbung zurück           @HA    BEGIN
@HB  und warte bis er KG verlassen hat.           @HA      s1 := 1;
@HB                                               @HA      WHILE Turn = 2 DO;
@HB  Hat er es verlassen, bewerbe dich erneut.    @HA      s1 := 0;
@HB                                               @HA    END;
@HB  Hat der andere Prozeß sich nicht beworben,
@HB  betrete das kritische Gebiet.                @HL   kritisches Gebiet
@HB  Hast du das kritische Gebiet verlassen,
@HB  sage dies dem anderen Prozeß                 @HATurn = 2;
@HB  und lösche deine Bewerbung.                  @HAs1 := 1;


                 @HBweiter mit ⌐Dijkstra@BS___3¬
AHBAA #!!# Dijkstra            *
@HESynchronisationslösung für N parallele Prozesse (nach Dijkstra)
@HA
PROGRAM Process_i (b, c, k);

  CONST
  MöchteGern = ...; @HB(* Antragsteller für das kritische Gebiet *)@HA
  N = ...;          @HB(* Anzahl Prozesse                        *)@HA

  TYPE
  Prozeß-Menge = 1..N;

  VAR
  Nicht-Bewerber : SET OF Prozeß-Menge; @HB(* wollen gar nicht hinein  *)@HA
  NotMember      : SET OF Prozeß-Menge; @HB(* sind nicht im Kr. Gebiet *)@HA
  Y : SET OF Prozeß-Menge;              @HB(* ??? *)@HA
  Auserwählter : Prozeßmenge;           @HB(* dürfte wenn er will      *)@HA
  KrGebietFrei : Boolean;               @HB(* wenn ja dann los         *)@HA

@HABEGIN
  WHILE TRUE DO
    BEGIN @HB(* Bewerbung um kritisches Gebiet *)@HA
      KrGebietFrei := FALSE;
      Nicht-Bewerber := Nicht-Bewerber - {MöchteGern};
      Y := {1..N} - {MöchteGern};               @HB(* nie benutzt ??? *)@HA
      REPEAT @HB(* geeigneten Bewerber suchen *)@HA
        IF Auserwählter <> MöchteGern THEN
          BEGIN @HB(* MöchteGern wird NotMember *)@HA
            NotMember := NotMember + {MöchteGern};
            IF Auserwählter IN Nicht-Bewerber THEN
              Auserwählter := MöchteGern;
          END   @HB(* MöchteGern wird NotMember *)@HA
        ELSE
          BEGIN
            NotMember := NotMember - {MöchteGern};
            KrGebietFrei := (NotMember + {MöchteGern}) = {1..N};
          END;
@HA      UNTIL KrGebietFrei;
      @HLK R I T I S C H E S   G E B I E T@HA
      NotMember := NotMember + {MöchteGern}; @HB(* bin wieder zurück  *)@HA
      Nicht-Bewerber := Nicht-Bewerber + {MöchteGern} @HB(* erledigt *)@HA
    END;  @HB(* Bewerbung um kritisches Gebiet *)@HA
END.@HB

@HBBeschreibung des Algorithmusses:
                                          @HA:
                                          @HAWHILE TRUE DO
                                          @HA  BEGIN
                                          @HA    ok := FALSE:
@HBBewerbe dich um das kritische Gebiet      @HA    b := b - {i};
                                          @HA    REPEAT
@HBWenn du nicht der ausgewählte Prozeß zum  @HA      IF k <> i THEN
@HBBetreten des kritischen Gebiets bist,     @HA        BEGIN
@HBdann wirst du in die Menge der Bewerber   @HA          c := c + {i};
@HBaufgenommen
@HBund wenn der ausgewählte Prozeß sich      @HA          IF k ε b THEN
@HBnicht beworben hat,
@HBdann wirst du zum ausgewählten Prozeß.    @HA            k := i
                                          @HA        END
                                          @HA      ELSE
@HBWenn du der ausgewählte Prozeß bist,      @HA        BEGIN
@HBdann teile dies den anderen Bewerbern mit @HA          c := c - {i};
                                          @HA          ok := (c + {i} = {1..N});
                                          @HA        END;
@HBund wenn das kritische Gebiet frei ist,   @HA    UNTIL ok;
@HBbetrete es.
                                          @HL         kritisches Gebiet

@HBHast du es verlassen,                     @HA    c := c + {i};
@HBso teile dies den Bewerbern mit und
@HBziehe deine Bewerbung zurück.             @HA    b := b + {i};
                                          @HA  END;

@HBBemerkungen:

   - Der gegenseitige Ausschluß ist gewährleistet.
     Der Prozeß, der im kritischen Gebiet ist, hat sich vorher aus der
     Menge der Bewerber gestrichen.

     Will ein weiterer Prozeß das kritische Gebiet betreten, so streicht
     auch er sich aus der Menge der Bewerber, dadurch kann ok aber nicht
     TRUE werden und er bleibt in der REPEAT-Schleife.

   - Es ist auch ausgeschlossen, daß niemand das kritische Gebiet betritt,
     obwohl Bewerber da wären.

     Gelangen mehrere Prozesse gleichzeitig in den ELSE-Zweig, so kann ok
     nicht TRUE werden und sie müssen die REPEAT-Schleife erneut durch-
     laufen. Dabei gilt aber nur für einen einzigen Prozeß k = i. Dieser
     kommt erneut in den ELSE-Zweig, aber als einziger, kann somit ok auf
     TRUE setzen und das kritische Gebiet betreten.
@HB   - Es ist möglich, daß ein Prozeß verhungert, da nicht bestimmt festge-
    legt ist, wer k auf dessen Prozeßnummer setzt.

@HEVerbesserung
@HB
Um die Möglichkeit des Verhungerns auszuschließen, gibt es von einigen
Leuten Verbesserungsvorschläge zum Algorithmus von Dijkstra.

  a) @HPKnuth                         N-1@HB
     Ein Prozeß muß auf höchstens @HP2    - 1@HB Besuche anderer Prozesse ihres
     kritischen Gebietes warten, bis er selbst eines betreten kann.

  b) @HPde Bruijn                                N * (N-1)@HB
     Verbesserung von Knuths Algorithmus auf @HP───────────@HB Besuche anderer,
     bevor man selbst eins betreten kann.         @HP2@HB

  c) @HPEisenberg & Mc Guire@HB
     Verbesserung von Knuths Algorithmus auf @HPN - 1@HB Besuche anderer.
  d) @HPLamport@HB
     Reihenfolge des Betretens des kritischen Gebiets in @HPFCFS@HB.
     In diesem Fall greifen alle Prozesse auf die Daten der anderen
     Prozesse lediglich lesend zu. Nur die eigenen Daten können verändert
     werden. Dies war bei den anderen nicht der Fall.

                 weiter mit ⌐Semaphore@BS___3¬
AHBAA #!!# Semaphore
@EH                     Synchronisation mit Semaphoren
@HB
Die bisher beschriebenen Synchronisationsmethoden sind viel zu schwer-
fällig, zu undurchsichtig und haben den großen Nachteil des Pollings.

Dijkstra hat eine ökonomischere Lösung gefunden. Er hat einen neuen
Datentyp "Semaphor" eingeführt, mit dem man wartende Prozesse schlafen
legen kann, bis das Ereignis, auf das sie warten eintrifft. Dann werden
sie wieder geweckt.

Man unterscheidet zwei Typen von Semaphoren:

  a) die @HPbinären Semaphore@HB    : Wertebereich 0..1

  b) die @HPallgemeinen Semaphore@HB: Wertebereich 0..u (beliebig)


Allgemeine Semaphore sind zurückzuführen auf binäre Semaphore.
@HBEs gibt 3 verschiedene @HPOperationen auf Semaphore@HB:

  a) Initialisierung
  b) P-Operation
  c) V-Operation

@HPInitialisierung@HB
  Initialisiert wird eine Semaphorvariable (meistens) mit 1, z. B. s := 1

@HPP-Operation@HB
  Die P-Operation ist unteilbar. Sie bewirkt, daß die Semaphorvariable
  um 1 erniedrigt wird (dekrementiert wird).
  Implementierung der P-Operation:
@HA
  P (s) = { s := s - 1;                      @HI{ ... } = unteilbar@HA
            IF s < 0 THEN Warte (s) }


@HPV-Operation@HB
  Die V-Operation ist ebenfalls unteilbar und bewirkt, daß die Semaphor-
  variable um 1 erhöht wird (inkrementiert wird).
  Implementierung der V-Operation:
@HA
  V (s) = { s := s + 1;
            If s ≤ 0 THEN Wecke (s) }

@HPWarte (s)@HB
  Derjenige Prozeß, der die P-Operation ausführen will, wird schlafen
  gelegt (angehalten). In seiner Zustandsbeschreibung wird notiert, daß
  er auf eine V-Operation auf das Semaphor s wartet.

@HPWecke (s)@HB
  Ein Prozeß, der angehalten wurde und auf eine V-Operation auf das
  Semaphor s wartet, wird geweckt (aktiv gesetzt). Er kann sofort weiter-
  rechnen.

  @HBWarten mehrere Prozesse auf eine V-Operation auf dasselbe Semaphor,
  darf nur einer von ihnen geweckt werden. Die Auswahl aus der Menge der
  wartenden Prozesse kann zufallsmäßig geschehen oder, was fairer ist,
  nach dem FIFO-Prinzip. Im letzteren Fall ist gewährleistet, daß ein
  Prozeß nach einer endlich langen Wartezeit geweckt wird.

Bemerkungen:

   - Bei dieser Implementierung der P- und V-Operationen kann das
     Betriebssystem an der Größe von s erkennen, ob und wieviele Prozesse
     auf V (s) warten. Es ist also von Vorteil, für Semaphore auch
     negative Werte zuzulassen.






@HB   - Semaphore dienen in erster Linie dem Schutz kritischer Gebiete:
@HA
     Process_1: CYCLE                    Process_2: CYCLE
       BEGIN                               BEGIN
         P (s);                              P (s)
           @HLkritisches Gebiet 1                 kritisches Gebiet 2@HA
         V (s);                              V (s);
         :                                   :
         :                                   :
       END                                 END


             @HBweiter mit ⌐Erzeuger-Verbraucher@BS___3¬
AHBAA #!!# Erzeuger-Verbraucher
@HEErzeuger-Verbraucher-Problem
@HB
Beim Erzeuger-Verbraucher-Problem geht es um den Nachrichtenaustausch
zwischen Erzeugern (den Nachrichtenproduzenten) und Verbrauchern (den
Nachrichtenkonsumenten). Der @HPErzeuger@HB produziert Nachrichten und legt
diese in einem Puffer ab. Der @HPVerbraucher@HB holt die Nachrichten aus dem
Puffer und verarbeitet sie. Der @HPPuffer@HB ist ein globaler Speicher
variabler Länge.

Forderungen, die an die Lösung gestellt werden:

  1. Prozesse sollen sich beim Zugriff auf den Puffer nicht gegenseitig
     stören.
  2. Es darf nichts in den Puffer gelegt werden, wenn er voll ist.
  3. Es darf nichts aus dem Puffer geholt werden, wenn er leer ist.
  4. Die Arbeitsgeschwindigkeit von Erzeugern und Verbrauchern soll
     unabhängig voneinander sein.

@HETriviale Lösung für das Erzeuger-Verbraucher-Problem@HB

@HAVAR
Message, Leer : semaphor;

Init (Message := 0);
Init (Leer := 1);

Erzeuger    : "erzeuge Nachricht";
              P (Leer);
              "lege Nachricht in Puffer";
              V (Message);

Verbraucher : P (Message);
              "hole Nachricht aus Puffer";
              V (Leer);
              "verarbeite Nachricht";

@HBAuf diese Weise wird eine sequentielle Reihenfolge erzwungen.
Die Lösung verstößt damit gegen die Forderung der Unabhängigkeit der
Arbeitsgeschwindigkeiten für Erzeuger und Verbraucher.

Wendet man das Erzeuger-Verbraucher-Problem zum Beispiel auf eine Druck-
ausgabe an, so kommt es zum "Stottern" des Druckers. Der Erzeuger
produziert Daten für den Drucker und legt sie im Druckerpuffer ab. Der
Verbraucher holt die Daten aus dem Druckerpuffer und gibt sie auf den
Drucker. Bei einer sequentiellen Reihenfolge kann erst wieder etwas in den
Puffer gelegt werden, wenn er vom Verbraucher geleert worden ist. Die
Folge ist, daß der Drucker stottert.

Um dies zu vermeiden, verwendet man statt einem zwei Puffer, die ab-
wechselnd gefüllt und geleert werden. Zunächst wird der Puffer_1 gefüllt.
Während Puffer_1 geleert wird, wird Puffer_2 gefüllt. Ist Puffer_2
schneller gefüllt als Puffer_1 geleert, so muß der Erzeuger anhalten. Der
Verbraucher kann allerdings, nachdem er Puffer_1 geleert hat, direkt
Puffer_2 leeren.
@HBDas Füllen des einen und das Leeren des anderen Puffers kann parallel
erfolgen.

@HELösung des Erzeuger-Verbraucher-Problems für K Puffer
(Kreispuffer mit K Einheiten)

@HAVAR
Leer, Voll : Semaphor;
Puffer : ARRAY [0..K-1] OF INFO;
EX : Integer;                     @HB(* Erzeuger-Index    *)@HA
VX : Integer;                     @HB(* Verbraucher-Index *)@HA

Init (Leer := K);
Init (Voll := 0);
EX := 0;
VX := 0;


@HAErzeuger    : "erzeuge Nachricht";
              P (Leer);
              Puffer [EX] := erzeugte Nachricht;
              EX := Succ (EX);     @HB(* modulo K *)@HA
              V (Voll);

Verbraucher : P (Voll);
              "hole Nachricht aus Puffer [VX];
              VX := Succ (VX);     @HB(* modulo K *)@HA
              V (Leer);
              "verarbeite Nachricht";


                @HBweiter mit ⌐Leser-Schreiber@BS___3¬
AHBAA #!!# Leser-Schreiber
@HELeser-Schreiber-Problem

@HPProblem 1:@HB

Beim Leser-Schreiber-Problem gibt es zwei Arten von Prozessen,
Leser und Schreiber. Sie greifen auf ein gemeinsames Betriebsmittel
zu, zum Beispiel eine Datei. Dabei gelten folgende Regeln:

  a) Es können mehrere Leser gleichzeitig aktiv sein (also lesen),
     aber zum selben Zeitpunkt darf niemand schreiben.

  b) Es darf genau ein Schreiber gleichzeitig aktiv sein (also schreiben),
     aber zum selben Zeitpunkt darf niemand lesen.

  c) Bei Problem 1 gilt außerdem:
     Sollte sich während des Zugriffs von Lesern ein Schreiber
     bewerben, so muß er warten bis kein Leser mehr aktiv ist.
     Leser werden hier also bevorzugt.
@HELösung zu Problem 1:@HB (mit ⌐Semaphor@BS1¬en)
@HA
VAR
RC : Integer;                         @HB(* reader counter            *)@HA
W, Mutex : Semaphor;                  @HB(* mutex exclusion           *)@HA
                                      @HB(* = gegenseitiger Ausschluß *)@HA
Init (W := 1);
Init ( Mutex := 1);
RC := 0;









@HAWriter : P (W);                @HB(* ist jemand am Lesen oder Schreiben ?  *)
@HA         "schreiben";          @HB(* falls nein, dann los                  *)
@HA         V (W);                @HB(* Message: Ich bin fertig.              *)
@HA
@HAReader : P (Mutex);            @HB(* ändert gerade einer RC ?              *)
@HA         RC := RC + 1;         @HB(* falls nein, dann los                  *)
@HA         IF RC = 1 THEN P (W); @HB(* ich der einzige -> schreiben sperren  *)
@HA                               @HB(* eventuell auf einen Schreiber warten  *)
@HA         V (Mutex);            @HB(* fertig mit Ändern von RC              *)
@HA         "lesen";
@HA         P (Mutex);            @HB(* Zugriff auf RC schützen               *)
@HA         RC := RC - 1;
@HA         IF RC = 0 THEN V (W); @HB(* kein Leser mehr -> schreiben freigeben*)
@HA         V (Mutex);            @HB(* fertig mit Ändern von RC              *)




@HB
Bemerkungen:

   - Beim Schreiber ist das Schreiben das kritische Gebiet,
     während beim Leser die Veränderung der Variablen RC vor
     gleichzeitigem Zugriff geschützt werden muß.

   - Welche Art von Prozeß durch die V (W)-Operation geweckt wird
     ist nicht deterministisch festgelegt. Dadurch kann es
     passieren, daß die Schreiber verhungern (nämlich dann, wenn
     während ein Leser aktiv ist, mindestens ein weiterer Leser
     dazu kommt).






@HPProblem 2:@HB

  a)  ┐
      ├ wie bei Problem 1
  b)  ┘

  c) wird geändert, es soll gelten:
     Schreiber werden bevorzugt behandelt, d. h. sobald ein Schreiber
     darauf wartet, aktiviert zu werden (er schläft), dürfen keine
     weiteren Leser mehr angenommen werden.








@HELösung 2:@HB
@HAVAR
rc : Integer;             @HB(* reader counter                        *)@HA
wc : Integer;             @HB(* writer counter                        *)@HA
mutex1 : Semaphor;        @HB(* exklusiver Zugriff auf rc             *)@HA
mutex2 : Semaphor;        @HB(* exklusiver Zugriff auf wc             *)@HA
mutex3 : Semaphor;        @HB(* Bevorzugung von Schreibern vor Lesern *)@HA
w      : Semaphor;        @HB(* Schutz vor Schreiben beim Lesen und   *)@HA
                          @HB(* Schutz vor Lesen beim Schreiben       *)@HA
r      : Semaphor;        @HB(* Unterbrechung des Lesestroms          *)@HA

Init (mutex1 := 1);
Init (mutex2 := 1);
Init (mutex3 := 1);
Init (w      := 1);
Init (r      := 1);
rc := 0;
wc := 0;@HB

@HAReader : P (mutex3);                 @HB(* hier bleibt der nächste Leser   *)
@HA                                     @HB(* schon stecken                   *)
@HA           P (r);                    @HB(* darf ich lesen ?                *)
@HA                                     @HB(* jetzt kann ein weiteres P (r)   *)
                                     @HB(* nur von einem Schreiber kommen  *)
@HA             P (mutex1);
               rc := rc + 1;
               IF rc = 1 THEN P (w);
             V (mutex1);
           V (r);                     @HB(* Falls Schreiber wartet         *)
@HA         V (mutex3);
         "lesen";
         P (mutex1);
           rc := rc - 1;
           IF rc = 0 THEN V (w);
         V (mutex1);@HB


@HAWriter : P (mutex2);
           wc := wc + 1;             @HB(* die beiden Operationen sind    *)
@HA           IF wc = 1 THEN P (r);     @HB(* geteilt ! Das ist gefährlich!  *)
@HA         V (mutex2);
         P (w);
           "schreiben";
         V (w);
         P (mutex2);
           wc := wc - 1;
           IF wc = 0 THEN V (r);
         V (mutex2);@HB







@HBBemerkungen:
   - Befindet sich ein Leser zwischen der P (r)- und der V (r)-Operation,
     dann wird durch mutex3 erreicht, daß wenn überhaupt jemand auf die
     V (r)-Operation wartet, dies nur ein Schreiber sein kann. Ein Leser
     bleibt schon in P (mutex3) stecken.

   - Auf einen Schreiber kann wegen P (r) und P (mutex3) nur höchstens ein
     Leser warten und/oder wegen P (w) viele Schreiber.

   - Läßt sich der 1. Schreiber nach der Ausführung von wc := wc + 1 bis
     zur Ausführung von P (r) Zeit, dann können im Gegensatz zur Aufgaben-
     stellung während dieser Zeit beliebig viele Leser das System
     betreten !

   - Es kann doch immer nur einer gleichzeitig lesen, wegen P (mutex3) ???
     -> Verletzung von Regel a) ???


  siehe auch:                    weiter mit ⌐5 Philosophen@BS___3¬
  ⌐REGION@BS___3¬
  ⌐Monitore@BS1¬
  ⌐Monitore II@BS___3¬
AHBAA #!!# 5 Philosophen
                               @HM┌────┐@HB
                               @HM│  0 │@HB
                     @HJ└┼┘@HB       @HM└────┘@HB       @HJ└┼┘@HB
                     @HJ │@HB1                     @HJ│@HB0

                @HM┌────┐@HB                        @HM┌────┐@HB
                @HM│  1 │@HB        @HPSPAGHETTI@HB       @HM│  4 │@HB
                @HM└────┘@HB        @HO≈≈≈≈≈≈≈≈≈       @HM└────┘@HB
                    @HJ└┼┘@HB                      @HJ└┼┘@HB
                     @HJ│@HB2                       @HJ│@HB4
                        @HM┌────┐@HB   @HJ└┼┘@HB  @HM┌────┐@HB
                        @HM│  2 │@HB    @HJ│@HB3  @HM│  3 │@HB
                        @HM└────┘@HB        @HM└────┘@HB

Beim 5 Philosophen-Problem wird der Lebensrhythmus von 5 Philosophen
betrachtet, der im Abwechseln von Denken und Essen besteht. Beide Tätig-
keiten schließen sich gegenseitig aus.

@HBDas Essen erfolgt an einem kreisförmigen Tisch, auf dem 5 Teller stehen
und zwischen jedem Teller liegt eine Gabel. Jeder Philosoph i benötigt
2 Gabeln zum Essen, sowohl die links neben seinem Teller als auch die
rechts davon (gabel [i] und gabel [(i+1) mod 5]).

Die Gabeln stellen ein exklusives ⌐Betriebsmittel@BS1¬ dar, auf das der Zugriff
synchronisiert werden muß. Dies geschieht bei ⌐Semaphor@BS1¬en mit
P- und V-Operationen. Andere Lösungsmöglichkeiten sind durch
  ⌐REGION@BS___3¬-Anweisungen oder
  ⌐Monitore@BS1¬ gegeben.

@HELösungsansätze:@HB






@HEAnsatz 1:@HB

  @HAphilosoph_i : CYCLE
    BEGIN
      "denken";
      P (gabel [i]);
        P (gabel [i+1]);          @HB(* i+1 heißt natürlich (i+1) mod 5   *)
@HA          "essen";
        V (gabel [i+1]);
      P (gabel [i]);
    END;

@HBDieser Ansatz ist deadlockgefährdet. Setzen sich alle 5 Philosophen
gleichzeitig an den Tisch und jeder nimmt seine linke Gabel (gabel [i]),
dann sind alle Gabeln belegt aber keiner kann essen. Jeder wartet darauf,
daß sein rechter Nachbar dessen linke Gabel freigibt ==> Die Philosophen
erwartet ein schweres Schicksal, Deadlock.

@HEAnsatz 2:

@HBMan verlegt den Zugriff auf die Gabeln in ein geschütztes kritisches
Gebiet:
@HA
           :
      P (mutex);
        P (gabel [i]);
        P (gabel [i+1]);
      V (mutex);
           :
@HB
Diese Lösung ist nicht optimal, denn es kann vorkommen, daß ein Philosoph
warten muß, obwohl seine beiden Gabeln frei sind, weil ein anderer Philo-
soph noch auf eine seiner Gabeln wartet. Dieser versperrt das kritische
Gebiet. Man hat also eine schlechte Auslastung der Betriebsmittel.


@HBFalls man versucht, Lösung 1 zu verbessern, indem man die Gabeln
hierarchisch anordnet und verlangt, daß jeder Philosoph zuerst die Gabel
mit der kleineren Nummer ergreift, kann es zwar nicht mehr passieren, daß
alle Gabeln vergeben sind und keiner ißt, aber das Manko der 2. Lösung
(ein Philosoph muß warten, obwohl seine beiden Gabeln frei wären) bleibt.

@HEAnsatz 3:@HB

Man führt Zustandsvariablen z [i] für jeden Philosophen i ein:

   Zustand 0 : denken
   Zustand 1 : hungrig sein
   Zustand 2 : essen

   ... -> Zustand 0 -> Zustand 1 -> Zustand 2 -> Zustand 0 -> ...

Auf diese Weise will man gewährleisten, daß ein Philosoph essen kann,
wenn seine Gabeln frei sind.
@HBDer Lebenszyklus eines Philosophen besteht jetzt in dem Zyklus
denken, hungrig sein, essen, denken, ...

Um vom Zustand 1 in den Zustand 2 zu gelangen müssen folgende
Bedingungen erfüllt sein:

  1) @HPz [i]   =  1@HB        Philosoph i muß hungrig sein

  2) @HPz [i-1] <> 2@HB        sein linker Nachbar  darf nicht essen

  3) @HPz [i+1] <> 2@HB        sein rechter Nachbar darf nicht essen

Ein Philosoph kann nur essen, wenn diese 3 Bedingungen gleichzeitig
gelten. Er muß also die Zustände seiner beiden Nachbarn prüfen. Wenn
beide nicht essen, so darf er es tun.
Falls er warten muß, so kann ihn nur der Nachbar wecken, der seine
Gabel zurückgibt. Dieser muß daher, wenn er seine Gabeln zurückgibt,
testen, ob seine Nachbarn essen wollen und sie gegebenenfalls wecken.

@HEAlgorithmus:

@HAVAR
mutex   : Semaphor;
z       : ARRAY [0..4] OF 0..2;
i       : Integer;
privsem : ARRAY [0..4] OF Semaphor;

Init (mutex := 1);
FOR i := 0 TO 4 DO z [i] := 0;
FOR i := 0 TO 4 DO Init (privsem [i] := 0);






@HAPhilosoph_i : CYCLE
  BEGIN
    "denken";
    P (mutex);
      "hungrig werden": z [i] := 1;
      "teste Zustände der Nachbarn:
       Wenn sie nicht essen, so ist dein neuer Zustand essen
       und mache P (privsem [i])";
    V (mutex);
    P (privsem [i]);
    "essen";
    P (mutex);
      "denken": z [i] := 0;
      "teste ob linker Nachbar essen will:
       Wenn er will, wecke ihn: V (privsem [i-1])";
      "teste ob rechter Nachbar essen will:
       Wenn er will, wecke ihn: V (privsem [i+1])";
    V (mutex);
@HA  END;@HB

@HBBemerkungen:
   - Durch die beiden P (privsem [i]) legt sich jeder Philosoph gleich
     zweimal schlafen und muß erst durch seine beiden Nachbarn geweckt
     werden, bevor er endlich essen kann. ???

   - Ein Philosoph, der mit dem Essen fertig ist, weckt seine beiden
     Nachbarn. Wenn ihm dann gleich darauf einfällt, wieder essen zu
     wollen, so muß er erst warten, bis seine Nachbarn damit fertig sind,
     falls diese während seiner Essenszeit hungrig waren. ???

   - Es ist nicht sicher, daß jeder Philosoph nach einer endlich langen
     Zeit essen kann (livelock). Dies kann man verhindern, indem man an
     die einzelnen Philosophen dynamische Prioritäten verteilt, die mit
     der Wartezeit steigen.



@HBVorteile von Semaphoren:
   - mächtiges und flexibles Instrument zur Synchronisation
   - Prozessor wird nicht durch "busy-waiting" unnötig belegt

Nachteile:
   - Synchronisation mit Semaphoren ist meist undurchsichtig und
     schwer zu konstruieren.
   - Es kann weder zur Compilezeit noch zur Laufzeit die Plausibilität
     erkannt werden. Man kann keine Schreibfehler (P statt V oder
     umgekehrt, P-Operation auf falsches Semaphor) erkennen.
   - Man sieht nicht, welche V-Operation zu welcher P-Operation gehört.
   - Beweismethoden sind schwer zu entwickeln und anzuwenden.

Bemerkung:
   - Semaphor-Operationen sind eher den Assembler-Befehlen zuzuordnen,
     als Konstrukten höherer Programmiersprachen.

@HEAnsatz für "Beweise von Semaphor-Operationen"
@HB
Charakteristische Variablen bei Semaphor-Operationen sind

  a) @HPnv [s]@HB : Anzahl bisher ausgeführter V-Operationen auf s
  b) @HPnp [s]@HB : Anzahl der begonnenen und vollendeten P-Operationen auf s
  c) @HPna [s]@HB : Anzahl der jemals begonnenen P-Operationen auf s

Für die P-Operation gilt:              Für die V-Operation gilt:
@HA
P (s) : { na [s] := na [s] + 1;        V (s) : { nv [s] := nv [s] + 1;
          s := s - 1;                            s := s + 1;
          IF s < 0 THEN Warte (s);               IF s ≤ 0 THEN Warte (s);
          np [s] := np [s] + 1; }              }
@HB
Dabei hat immer folgende Invariante zu stimmen:
@HP
        np [s] = min {na [s], c [s] + nv [s]}   @HBsiehe ⌐Habermann@BS___3¬


                @HBweiter mit ⌐Region@BS___3¬
AHBAA #!!# Region
Ein @HPbedingtes kritisches Gebiet@HB wird definiert durch

   @HAREGION V WHEN B DO Si END;@HB

wobei @HPV@HB  : eine Menge gemeinsam benutzbarer Betriebsmittel ist, die im
           Vereinbarungsteil mit dem Präfix @HAshared@HB bei der Typ-Angabe
           dazu gekennzeichnet wurde.

      @HPB@HB  : ein boolscher Aurdruck / eine Bedingung ist
           (der Teil "WHEN B" ist optional).

      @HPSi@HB : Anweisungen sind, die wie in einem kritischen Gebiet ablaufen
           (Si kann nur ausgeführt werden, wenn ein Prozeß im Besitz
           von V ist und B true ist):




@HBEs müssen folgende Forderungen erfüllt sein, damit man von einem
kritischen Gebiet sprechen kann:

  1) Während der Bearbeitung der Si kann V nicht an einen anderen
     ⌐Prozeß@BS1¬ vergeben werden.

  2) Die in B vorkommenden Variablen können nur in kritischen Gebieten
     geändert werden.

  3) Si selbst darf keine region-Anweisung sein, da sonst Deadlocks
     entstehen können.







@HEArbeitsweise der region-Anweisung:
@HB
Bei der Ausführung der Anweisung wird versucht, die in V aufgelisteten
⌐Betriebsmittel@BS1¬ für den Prozeß zu reservieren.

Können nicht sämtliche in V aufgeführten Betriebsmittel reserviert werden,
so muß der Prozeß alle bereits belegten Betriebsmittel wieder freigeben
und später neu gestartet werden.

Hat die Reservierung funktioniert, so wird der boolsche Ausdruck B ausge-
wertet:

  Ist das Ergebnis false, dann müssen wieder alle Betriebsmittel freige-
  geben werden und der Prozeß wird später neu gestartet.

  Ist das Ergebnis true, dann werden die Anweisungen Si ausgeführt und
  anschließend alle Betriebsmittel wieder freigegeben.

@HEProgrammierung eines kritischen Gebietes:

  @HAVAR
  mutex : SHARED T;
     :
     :
     :
  REGION mutex DO S END;        @HB(* S ist das kritische Gebiet *)

@HEErzeuger-Verbraucher-Problem

@HBDie Problemstellung lautet:
  Es gibt beliebig viele Erzeuger und Verbraucher. Zu jedem Erzeuger i
  gibt es einen Verbraucher i. Erzeuger und Verbraucher arbeiten auf
  einem gemeinsamen ⌐Puffer@BS1¬ der Größe N. Der Erzeuger kann nur dann
  eine Nachricht in den Puffer legen, wenn er einen freien Platz findet.
  Der Verbraucher i kann nur dann eine Nachricht aus dem Puffer holen,
  wenn Nachrichten für ihn vorliegen (ni > 0).
@HELösung 1:@HB

  @HAVAR
  v : SHARED RECORD
        f : Integer;          @HB(* freie Pufferplätze *)@HA
        n : ARRAY [prozesse] OF Integer;
                              @HB(* Anzahl Nachrichten für Prozeß *)@HA
      END;

  Init (f = N; für alle i: n [i] = 0);

  Erzeuger_i :    REGION v WHEN f > 0 DO
                    BEGIN
                      f := f - 1;
                      n [i] := n [i] + 1;
                      "lege Nachricht in den Puffer"
                    END;

  @HAVerbraucher_i : REGION v WHEN n [i] > 0 D
                    BEGIN
                      f := f + 1;
                      n [i] := n [i] - 1;
                      "hole Nachricht aus Puffer"
                    END;

@HEAnmerkungen:@HB
   - Die Unabhängigkeit von der Arbeitsgeschwindigkeit wird hier verletzt.

     Existiert ein Prozeßpaar mit schnellem Erzeuger aber langsamen Ver-
     braucher, so kann bald der gesamte Speicher mit Nachrichten für den
     langsamen Verbraucher belegt sein. Alle anderen Prozesse müssen dann
     darauf warten, daß dieser wieder Platz schafft, indem er seine Nach-
     richten aus dem Puffer holt.

     Alle Prozesse können somit nur mit der Geschwindigkeit des langsamen
     Verbrauchers arbeiten.
@HB   - Die Lösung 1 verstößt auch gegen die Forderung, daß ein Prozeß
     nicht andere Prozesse blockieren darf, wenn er außerhalb des
     kritischen Gebietes anhält (stirbt).

     Stirbt ein Verbraucher außerhalb des kritischen Gebietes, so ist
     irgendwann der Puffer nur noch mit Nachrichten für diesen Prozeß
     belegt. Andere Erzeuger und Verbraucher können nicht mehr mit dem
     Puffer arbeiten und werden blockiert.

Die beiden Verstöße kann man vermeiden, indem man jedem Erzeuger-
Verbraucher-Paar einen Mindestanteil ri am Puffer garantiert. Stehen
zusätzlich noch Puffereinheiten zur Verfügung, dürfen diese von allen
Prozessen benutzt werden.





@HELösung 2:

  @HAVAR
  v : SHARED RECORD
        f    : Integer        @HB(* zusätzliche freie Pufferplätze *)@HA
        n, r : ARRAY [prozesse] OF Integer;
      END;

  Init (f = N - Σ ri ; für alle i : ri = const, ni = 0)
               i=0

  Erzeuger_i :    REGION v WHEN (n [i] < r [i] OR f > 0) DO
                    BEGIN
                      n [i] := n [i] + 1;
                      IF n [i] > r [i] THEN f := f - 1;
                      "lege Nachricht in den Puffer";
                    END;

  @HAVerbraucher_i : REGION v WHEN n [i] > 0 DO
                    BEGIN
                      IF n [i] > r [i] THEN f := f + 1;
                      n [i] := n [i] - 1;
                      "hole Nachricht aus Puffer";
                    END;

@HELeser-Schreiber-Problem@HB

@HPProblem 1:@HB
Leser und Schreiber wollen auf ein gemeinsames Betriebsmittel zugreifen,
zum Beispiel eine Datei. Dabei gelten folgende Regeln:

  a) Mehrere Leser können gleichzeitig aktiv sein, aber zum gleichen
     Zeitpunkt kein Schreiber
  b) Genau ein Schreiber darf aktiv sein, zum gleichen Zeitpunkt kein
     weiterer Schreiber oder Leser
  c) Leser werden bevorzugt

@HELösung 1:

  @HAVAR
  rc : SHARED Integer;

  Init (rc := 0);

  Reader : REGION rc DO rc := rc + 1 END;
           "lesen"
           REGION rc DO rc := rc - 1 END;

  Writer : REGION rc WHEN rc = 0 DO "schreiben" END;





@HEAnmerkung:@HB

Entscheidend ist die Variable rc, die die Leser zählt.
Auf sie darf nur exklusiv zugegriffen werden, deshalb ist sie das
eigentliche exklusive Betriebsmittel.



@HPProblem 2:@HB

  a) ┐
     ├ wie bei Problem 1
  b) ┘

  c) Schreiber werden bevorzugt



@HELösung 2:

  @HAVAR
  rc, wc : SHARED Integer;

  Init (rc := 0; wc := 0);

  Reader : REGION (rc, wc) WHEN wc = 0 DO rc := rc + 1 END;
           "lesen"
           REGION (rc) DO rc := rc - 1 END;

  Writer : REGION (wc) DO wc := wc + 1 END;
           REGION rc WHEN rc = 0 DO "schreiben" END;
           REGION (wc) DO wc := wc - 1 END;




@HEAnmerkung:
@HB
Der Writer durchläuft 3 REGION-Anweisungen.

Zunächst erhöht er wc um 1, so daß danach auf jeden Fall wc > 0 ist
und sich somit kein reader vordrängeln kann.

Dann versucht der Writer zu schreiben. Das Schreiben ist in ein
kritisches Gebiet gelegt, damit garantiert nur ein einziger Writer
schreiben kann. Durch die Bedingung rc = 0 kann nicht gleichzeitig ein
Reader lesen.

In der 3. REGION Anweisung wird wc wieder um 1 erniedrigt.





@HE5-Philosophen-Problem
@HB
Lösung des ⌐5 Philosophen@BS___3¬-Problems unter Verwendung von
REGION-Anweisungen:

  @HAVAR
  Gabel : SHARED ARRAY [0..4] OF T;

  Philosoph_i : CYCLE
                  "denken"
                  REGION (Gabel [i], Gabel [i+1]) DO "essen" END;
                END;
@HEAnmerkungen:@HB
   - Vorausgesetzt ist, daß die REGION-Implementierung den Zugriff auf
     einzelne Elemente des SHARED ARRAY erlaubt.
   - Schwierigkeiten bei Semaphoren, z. B. Test ob Philosoph_i essen darf,
     sind hier der Implementation überlassen.
   - Es besteht immer noch das Problem des "Livelocks".
@HEVorteile bei der Verwendung von REGIONs:@HB
   - Zur Compilezeit können schon triviale Synchronisationsfehler, wie
     vergessene Variablen (damit kein synchronisierter Zugriff),
     Schreibfehler, Schachtelung von REGION-Anweisungen, erkannt und
     berichtigt werden.

   - Das REGION-Konzept hat die gleiche Mächtigkeit wie Semaphore
     (Man kann Semaphore durch REGIONs darstellen.)

@HENachteil bei der Verwendung von REGIONs:@HB
   - Das REGION-Konzept ist unökonomisch in Bezug auf die Betriebsmittel,
     da zu Beginn einer REGION-Anweisung alle Betriebsmittel reserviert
     werden müssen und diese für die ganze REGION-Zeit belegt sind.


               weiter mit ⌐Monitore II@BS___3¬
AHBAA #!!# Monitore II
Ein Monitor ist eine Sammlung von Daten und Prozeduren. Man kann ihn
ansehen als ein Programmstück, das man als abstrakten Datentyp des
⌐Betriebssystem@BS1¬s auffassen kann.

Aufbau:

  @HA<Monitorname> : MONITOR;
                    BEGIN
                      <Deklaration lokaler Daten>
                      <Folge lokaler Prozeduren>
                      <Initialisierung lokaler Daten>
                    END;

@HBDie lokalen Prozeduren eines Monitors können von allen Prozessen
benutzt werden.



@HBDer gegenseitige Ausschluß von Prozessen wird bei Monitoren dadurch
erreicht, daß in einem Monitor immer nur ein einziger Prozeß, also nur
eine lokale Prozedur, aktiv sein kann.

Beim Eintritt in einen Monitor haben alle lokalen Daten definierte Werte,
die auch nicht verloren gehen, wenn der Monitor verlassen wird.

Ein ⌐Prozeß@BS1¬ (lokale Prozedur) kann mit "wait" in den Wartezustand
übergehen und kann mit "signal" geweckt werden.

Welches "wait" zu welchem "signal" gehört, wird über eine Variable vom
Typ "condition" geregelt.

  @HAVAR
  q : condition;



  @HAq.wait :@HB
  Das aufgerufene Programm wird angehalten und geht in den Wartezustand
  über (Warten auf ein Signal der Variablen q).
  Der beteiligte Monitor ist während der Wartezeit frei für andere
  Prozesse (der schlafende Prozeß ist ja nicht aktiv).
  Der schlafende Prozeß besitzt immer noch den Monitor. Er verleiht ihn
  quasi nur an einen anderen Prozeß.
  Unterschied zur P-Operation (siehe ⌐Semaphor@BS1¬):
  Bei P (q) muß man nur warten, wenn q = 0 gilt.
  Bei q.wait muß der Prozeß immer warten.








  @HAq.signal :@HB
  Es wird untersucht, ob es einen Prozeß gibt, der auf q wartet. (Dann
  gibt die Variable ein Signal.)
  Kein Prozeß wartet auf q:
    In diesem Fall ist die signal-Operation wirkungslos und kommt einer
    leeren Operation gleich.
  Mindestens ein Prozeß wartet auf q:
    Es wird ein Prozeß geweckt und sofort aktiviert, dadurch findet er
    die lokalen Monitordaten so vor, wie sie zum Zeitpunkt der signal-
    Operation existierten (d. h. der aktivierte Prozeß kann hinter seiner
    q.wait-Operation weitermachen).
    Der signalisierende Prozeß befindet sich im selben Monitor wie der
    wartende und muß deshalb jetzt selbst in den Wartezustand übergehen,
    da zu einem Zeitpunkt nur ein einziger Prozeß im Monitor aktiv sein
    kann und das ist in diesem Fall der geweckte.
  Unterschied zur V-Operation:
    Nach der V (q)-Operation muß nicht unbedingt (je nach Implementation)
    ein sofortiger Prozeßwechsel stattfinden, wie es hier der Fall ist.
  @HAq.queue :@HB
  Ist eine boolsche Funktion, mit der man abfragen kann, ob es Prozesse
  gibt, die auf die Variable q vom Typ condition warten.
  q.queue = true  heißt, es gibt Prozesse, die auf q warten
  q.queue = false heißt, niemand wartet auf q.
  Unterschied zu Semaphore:
  Beim Arbeiten mit Semaphoren ist es nicht möglich, die Größe von
  Semaphorvariablen abzufragen.

@HEImplementierung eines binären Semaphors durch einen Monitor

@HBIndem man angibt, wie Semaphore durch Monitore darstellbar sind,
kann man zeigen, daß Monitore die gleiche Mächtigkeit besitzen wie
Semaphore:




@HAPV: MONITOR;
         BEGIN
           VAR
           Busy : Boolean;      @HB(* true  = ein Prozeß aktiv  *)@HA
                                @HB(* false = kein Prozeß aktiv *)@HA
           NonBusy : Condition;
           PROCEDURE P;
             BEGIN
               IF Busy THEN NonBusy.Wait;
               Busy := TRUE;
             END;
           PROCEDURE V;
             BEGIN
               Busy := FALSE;
               IF NonBusy.Queue THEN NonBusy.Signal;
             END;
           Busy := FALSE;
         END;

@HEAufruf:
@HA  PV.P;
    @HLkritisches Gebiet@HA
  PV.V;

@HB    weiter mit  ⌐Monitor-Beispiele@BS___3¬
    siehe auch: Lexikondefinition ⌐Monitore@BS1¬
                   ⌐Monitore - Beweis@BS___3¬
                   ⌐Region@BS___3¬
                   ⌐Semaphor@BS1¬
                   ⌐LOCK und UNLOCK@BS___3¬
AHBAA #!!# Monitor-Beispiele
@HELösung des Erzeuger-Verbraucher-Problems mit Monitoren
@HB
Für die Problemstellung siehe ⌐Erzeuger-Verbraucher@BS___3¬.
Monitore werden erläutert im Kapitel ⌐Monitore II@BS___3¬.

Angegeben wird eine Lösung von Hoare, bei der eine faire Verplanung des
gemeinsam benutzten Puffers stattfindet. Dies wird erreicht, indem beim
Übergang in den Wartezustand dem Prozeß eine Priorität mitgegeben wird,
die beim Wecken wartender Prozesse ausgewertet wird. Es wird stets der
Prozeß mit der kleinsten Priorität geweckt.

q.wait wird damit erweitert zu q.wait (prio).






Hoare teilt den Erzeuger-Verbraucher-Paaren keine festen Pufferanteile zu,
sondern macht folgende Feststellungen für eine faire Verplanung:

   - Ein nicht aktives Erzeuger-Verbraucher-Paar benötigt keinen Puffer.

   - Wenn ein Verbraucher wesentlich schneller ist als der Erzeuger, wird
     das Paar in der Regel nicht mehr als 2 Puffereinheiten belegen.

   - Zur fairen Verplanung genügt es, demjenigen Prozeß freigewordenen
     Puffer zuzuteilen, der im Augenblick den wenigsten Platz belegt.
     Je weniger Pufferplatz ein Prozeß belegt, desto größer soll also
     seine Priorität sein.






@HELösung:
@HA
  BufferAllocator:
    MONITOR
      BEGIN
        VAR
        Free : Integer;         @HB(* Anzahl der freien Pufferplätze *)@HA
        NonEmpty : Condition;
        Count : ARRAY [1..K] OF Integer;   @HB(* Prioritäten für K   *)@HA
                                    @HB(* Erzeuger-Verbraucher-Paare *)@HA

        PROCEDURE Acquire (i : 1..K; VAR Adr : BufferAdr);
          BEGIN
            IF Free = 0 THEN NonEmpty.Wait (Count [i]);
            Free := Free - 1;
            Count [i] := Count [i] + 1;
            Adr := ...;        @HB(* lege Nachricht unter Adr ab     *)@HA
          END;
@HA
        PROCEDURE Release (i : 1..K; Adr : Buffer);
          BEGIN
            Free := Free + 1;
            Count [i] := Count [i] - 1;
            ... := Adr;
            "hole Nachricht aus dem Puffer"
            NonEmpty.Signal;
          END;

        Free := Speichergröße;         @HB(* Initialisierung *)@HA
        FOR j := 1 TO K DO             @HB(* "               *)@HA
          Count [j] := 0;





@HBAufruf:
   - Der Erzeuger ruft den Monitor auf mit:

       @HABufferAllocator.Acquire (i, Adr)@HB

     wobei i die eigene Prozeßnummer und Adr die Adresse eines freien
     Pufferplatzes ist.

   - Der Verbraucher ruft den Monitor auf mit:

       @HABufferAllocator.Release (i, Adr)@HB

     wobei i die eigene Prozeßnummer und Adr die Adresse des freizu-
     gebenden Pufferplatzes ist.




@HELösung des Leser-Schreiber-Problems mit Monitoren
@HB
Zur allgemeinen Problemstellung siehe ⌐Leser-Schreiber@BS___3¬.

@HPProblemstellung 1@HB

Der Zugriff von Lesern und Schreibern auf ein gemeinsames ⌐Betriebsmittel@BS1¬,
zum Beispiel eine Datei, soll nach folgenden Regeln ablaufen:

  a) Schreiber dürfen nur einzeln (exklusiv) arbeiten.

  b) Mehrere Leser dürfen gleichzeitig arbeiten.

  c) Solange es Schreibanwärter gibt, dürfen keine Leser ihre Arbeit
     beginnen.



@HELösung 1:
@HA
  ReadWrit :
    MONITOR;
      BEGIN
        VAR
        rc, wc : Integer
        OkToRead, OkToWrite : Condition;

        PROCEDURE StartRead;
          BEGIN
            IF wc > 0 THEN OkToRead.Wait;
            rc := rc + 1;
            OkToRead.Signal;
          END;



        @HAPROCEDURE EndRead;
          BEGIN
            rc := rc - 1;
            IF rc = 0 THEN OkToWrite.Signal;
          END;

        PROCEDURE StartWrite;
          BEGIN
            wc := wc + 1;
            IF (rc > 0) OR (wc > 1) THEN OkToWrite.Wait;
          END;

        PROCEDURE EndWrite;
          BEGIN
            wc := wc - 1;
            IF wc > 0 THEN OkToWrite.Signal
                      ELSE OkToRead.Signal;
          END;
@HA
        rc := 0;             @HB(* Initialisierung *)@HA
        wc := 0;             @HB(* "               *)@HA
      END;
@HB
Aufruf:
   - Der Leser ruft den Monitor auf mit:
        @HAReadWrite.StartRead;
        "lesen"
        ReadWrite.EndRead;@HB

   - Der Schreiber ruft den Monitor auf mit:
        @HAReadWrite.StartWrite;
        "schreiben"
        ReadWrite.EndWrite;



@HPProblemstellung 2:
@HB
Wie unter Problemstellung 1, jedoch mit neuen Regeln:

  a) Schreiber dürfen nur einzeln (exklusiv) arbeiten.

  b) Mehrere Leser dürfen gleichzeitig arbeiten.

  c) Ein neuer Schreiber darf nicht arbeiten, wenn (mindestens) ein
     Leser wartet.

  d) Ein neuer Leser darf nicht arbeiten, wenn (mindestens) ein
     Schreiber wartet.





@HELösung 2:
@HB
Lediglich die Prozedur EndWrite muß umgeschrieben werden zu:
@HA
  PROCEDURE EndWrite;
    BEGIN
      wc := wc - 1;
      IF OkToRead.Queue THEN OkToRead.Signal
                        ELSE OkToWrite.Signal;
    END;
@HB
Der Aufruf erfolgt wie bei Lösung 1.






@HELösung des 5 Philosophen Problems mit Monitoren
@HB
Zur Problemstellung siehe ⌐5 Philosophen@BS___3¬.

@HELösung 5 Philosophen
@HA
  Philosoph :
    MONITOR;
      BEGIN
        VAR
        NrForks : ARRAY [0..4] OF 0..2;
        Fork    : ARRAY [0..4] OF Condition;
        i       : Integer;





        PROCEDURE GetForks (i : 0..4);
          BEGIN
            IF NrForks [i] < 2 THEN Fork [i].Wait;
            NrForks [i-1] := NrForks [i-1] - 1;    @HB(* i±1 = i±1 MOD 5 *)
@HA            NrForks [i+1] := NrForks [i+1] - 1;
          END;

@HA        PROCEDURE PutForks (i : 0..4);
          BEGIN
            NrForks [i-1] := NrForks [i-1] + 1;
            NrForks [i+1] := NrForks [i+1] + 1;
            IF NrForks [i-1] = 2 THEN Fork [i-1].Signal;
            IF NrForks [i+1] = 2 THEN Fork [i+1].Signal;
          END;

        FOR i := 0 TO 4 DO NrForks [i] := 2;

      END;
@HBAufruf:
  Der Philosoph i ruft den Monitor auf mit:
@HA
     "denken"
     Philosoph.GetForks (i);
     "essen"
     Philosoph.PutForks (i);


@HEWeitere Lösungsansätze zur Synchronisation
@HB
   - ⌐Guarded Commands@BS2¬

   - Path-Expressions

   - Petri-Netze




       @HBweiter mit ⌐Habermann@BS___3¬
AHBAA #!!# Habermann
@HEBeweismethoden für parallele Prozesse

@HBDie Tests auf Korrektheit bei sequentiellen Programmen sind auf
parallele Prozesse nicht anwendbar, weil die Bearbeitungsreihenfolge
unvorhersehbar und nicht reproduzierbar ist. Hier können nur mathe-
matische Korrektheitsbeweise Sicherheit geben.

@HEBeweismethode nach Habermann

@HBDie Beweismethode nach Habermann ist speziell anwendbar auf parallele
Prozesse, die durch P- und V-Operationen synchronisiert werden. Die
Grundidee der Methode besteht darin, während des Laufes der Prozesse die
⌐Synchronisation@BS1¬svorgänge mitzuzählen. Man arbeitet mit Zählern, die
lediglich Informationen über die Vergangenheit beinhalten ("history
variables") und nicht implementiert werden müssen. Zusätzlich stellt man
eine Invariante auf, die aus diesen Zählern besteht. Sie muß zu jedem
Zeitpunkt gültig sein. Man testet dann die Verträglichkeit der Zählerzu-
stände mit der Invariante zum Zweck:
@HB  - der richtigen Synchronisation
  - der ⌐Deadlock@BS1¬-Untersuchung
  - eventuell: Fairness


@HEZähler und ihre Bedeutung:

  @HPna [s] @HB: number of attempted P-Operations
           Anzahl der jemals begonnenen P-Operationen auf ⌐Semaphor@BS1¬ s

  @HPnp [s] @HB: number of successfull P-Operations
           Anzahl der begonnenen und vollendeten P-Operationen auf s

  @HPnv [s] @HB: number of V-Operations
           Anzahl der ausgeführten V-Operationen auf s



@HEInvariante und ihre Aussage:
@HP
  np [s] = min {na [s]; c [s] + nv [s]}    mit c [s] = Initialwert von s
@HB
Die Gleichung besagt:

  a) Es können nicht mehr Prozesse die P-Operation beendet haben, als sie
     sie begonnen haben:
     @HP
     np [s] <= na [s]
     @HB
  b) Es können nicht mehr Prozesse die P-Operation beendet haben als der
     durch Initialwert und V-Operationen gegebene Wert:
     @HP
     np [s] <= c [s] + nv [s]
     @HB


@HEBeispiel: Kritisches Gebiet
@HB
Ein kritisches Gebiet besteht aus dem Programmstück

@HA  P (s);
    Anweisungen
  V (s);

@HBmit einem gegebenen Initialwert von s, c [s]. Dieser Initialwert
gibt die maximal zulässige Anzahl von Prozessen im kritischen Gebiet an.
Es sei c [s] = 1.

a) Zu beweisen:
@HE   Es kann sich höchstens genau ein Prozeß im kritischen Gebiet aufhalten.

@HBNach Durchlaufen von P (s) und vor der Ausführung von V (s) gilt auf
Grund der Invariante:
  @HPnp [s] <= 1 + nv [s]@HB

@HBdas heißt, das kritische Gebiet kann höchstens einmal mehr betreten
werden als es verlassen wurde.

@HBb) Zu beweisen:
@HE   Deadlockfreiheit

@HBEin Deadlock ist aufgetreten, wenn Prozesse am Betreten des
kritischen Gebiets gehindert werden, obwohl kein Prozeß im kritischen
Gebiet ist.

  Annahme: Es gibt wartende Prozesse.              @HPnp [s] < na [s]@HB
  Aus der Invariante folgt demnach                 @HPnp [s] = 1 + nv [s]@HB

  Wenn aber niemand im kritischen Gebiet ist,
  dann muß es genau so oft verlassen wie           @HPnp [s] = nv [s]@HB
  betreten worden sein.

@HB  Man erhält also einen Widerspruch, was besagt,
  daß die Annahme falsch ist.

@HEBeispiel: Erzeuger-Verbraucher-Problem
@HB
Zur allgemeinen Problemstellung siehe ⌐Erzeuger-Verbraucher@BS___3¬.
@HA
  CONST
  BufSize = ...;

  VAR
  Leer, Voll : Semaphor;
  Puffer : ARRAY [0..BufSize - 1] OF Info;
  ex : Integer;                @HB(* Erzeuger-Index    *)@HA
  vx : Integer;                @HB(* Verbraucher-Index *)@HA



@HA  BEGIN
    ex := 0;        @HB(* ex + 1 = ex + 1 MOD BufSize *)@HA
    vx := 0;        @HB(* vx + 1 = vx + 1 MOD BufSize *)@HA
    Voll := 0;
    PARBEGIN
      BEGIN @HB(* Erzeuger *)@HA             BEGIN @HB(* Verbraucher *)@HA
        "erzeuge Blabla";                P (Voll);
        P (Leer);                        "hole Blabla aus Puffer [vx]";
     @HJα@HA  Puffer [ex] := Blabla;        @HJß@HA  vx := vx + 1;
        ex := ex + 1;                    V (Leer);
        V (Voll);                        "verarbeite Blabla";
      END;                             END;
    PAREND;
  END;




@HBGehen wir im folgenden von 1 Erzeuger und 1 Verbraucher aus.

  a) Zu beweisen:
     Wenn beide Prozesse gleichzeitig auf den Puffer zugreifen, dann muß
     garantiert sein, daß sie nicht beide auf das gleiche Pufferelement
     zugreifen.

     Ein Parallelbetrieb ist also nur dann möglich, wenn BufSize ≥ 2 ist.
     Ein gleichzeitiger Zugriff auf den Puffer ist dann möglich, wenn sich
     der Erzeuger bei Marke @HJα@HB und der Verbraucher bei Marke @HJß@HB
     befindet.

     Zugriff auf den Puffer bei @HJα@HB:
       dann gilt für den Erzeuger   : @HLnp [Leer] = nv [Voll] + 1       @HJ1@HB
       für die Invariante gilt hier : @HLnp [Leer] ≤ BufSize + nv [Leer] @HJ2@HB
                                      mit c [Leer] = BufSize


@HB     Zugriff auf den Puffer bei @HJß@HB:
       dann gilt für den Verbraucher: @HLnp [Voll] = nv [Leer] + 1       @HJ3@HB
       für die Invariante gilt hier : @HLnp [Voll] ≤    0    + nv [Voll] @HJ4@HB
                                      mit c [Voll] = 0

     Wenn beide Prozesse auf das selbe Pufferelement zugreifen, muß gelten

                      @HLex = vx@HB

     Beim Start gilt: @HLex = vx = 0@HB

     Die Anzahl der Änderungen der beiden Variablen beträgt, wenn die
     beiden Prozesse sich gerade bei @HJα@HB bzw. @HJß@HB befinden:
@HL
       Anzahl Änderungen von ex = np [Leer] - 1
                                = np [Voll]                           @HJ5@HL
       Anzahl Änderungen von vx = np [Voll] - 1
                                = np [Leer]                           @HJ6@HB
@HB     Mit Gleichung @HJ4      @HLnp [Voll] ≤ nv [Voll]
@HB     und Gleichung @HJ2      @HLnp [Voll] = nv [Leer] + 1
@HB     erhält man
@HL                      nv [Leer] + 1 ≤ nv [Voll]
@HB     bzw. @HL                        1 ≤ nv [Voll] - nv [Leer]
@HB     und mit Gleichung @HJ5@HB und @HJ6@HL    1 ≤ ex - vx
@HB
     Man sieht, daß ex um mindestens eine Einheit vs vorausgeht.

     Andererseits gilt:   @HLnv [Voll] = np [Leer] - 1         @HBaus @HJ1@HB
                  und     @HLnp [Leer] ≤ BufSize + nv [Leer]   @HBaus @HJ2@HB

     woraus man erhält:   @HLnv [Voll] ≤ BufSize + nv [Leer] - 1@HB
                  bzw.    @HLnv [Voll] - nv [Leer] ≤ BufSize - 1
                            ex      -   vx      ≤ BufSize - 1
@HB
     Das bedeutet, ex kann vx nicht einholen.     q. e. d.

@HB  b) Zu beweisen:
     Deadlockfreiheit

     Wenn ein Deadlock auftritt,
     dann muß gelten:            @HL            np < na
@HB     Beim Erzeuger gilt für
     die Invariante:             @HL     np [Leer] = BufSize + nv [Leer]
@HB     Beim Verbraucher gilt für
     die Invariante:             @HL     np [Voll] = nv [Voll]
@HB
     Wenn kein Prozeß arbeitet, haben genau so viele Prozesse
     ihre Arbeit beendet wie begonnen
       Beim Erzeuger gilt daher   :   @HLnp [Leer] = nv [Leer]@HB
       Beim Verbraucher gilt daher:   @HLnp [Voll] = nv [Voll]@HB

     Da BufSize > 0 ist, ergibt sich ein Widerspruch. Die Annahme, daß
     ein Deadlock auftreten könnte, ist also falsch.

@HEAnmerkung:

@HBBedingte P- und V-Operationen sind mit dieser Methode schwierig
zu beweisen.


         weiter mit ⌐Owicki / Gries@BS___3¬
AHBAA #!!# Owicki / Gries
@HBDie Tests auf Korrektheit bei sequentiellen Programmen sind auf
parallele Prozesse nicht anwendbar, weil die Bearbeitungsreihenfolge
unvorhersehbar und nicht reproduzierbar ist. Hier können nur mathe-
matische Korrektheitsbeweise Sicherheit geben.

@HEBeweismethode nach Owicki / Gries

@HBDiese Beweismethode geht von der von Hoare entwickelten Notation:

@HA  {precondition} statement {postcondition}

@HBfür sequentielle Programme aus. Dabei ist die Grundidee, Programm-
folgen in elementare Operationen zu zerlegen, diese im einzelnen durch
bestimmte Beweisregeln zu verifizieren und sie dann wieder zu größeren
Einheiten zusammenzusetzen.




                 @HAa, b, c
@HBHoare Notation: @HA─────────
                 @HA   d

@HBbedeutet: wenn a, b und c wahr sind, dann ist auch d wahr.

                                      @HA{P AND B} S {P}
@HBBeispiel für WHILE-Statement: @HA────────────────────────────────
                               @HA{P} WHILE B DO S {P AND NOT B}








@HBUm Beweismethoden entwickeln zu können haben Owicki / Gries zwei
Sprachelemente definiert:

  a) COBEGIN, COEND was dem PARBEGIN, PAREND entspricht

  b) AWAIT B THEN S                 (* Ähnlichkeit mit ⌐Region@BS___3¬ *)
     wobei B Boolscher Ausdruck und
           S eine Anweisung, die weder COBEGIN noch AWAIT enthält.

Wenn ein Prozeß ein AWAIT-Statement ausführen will, dann wird er so
lange zurückgestellt, bis B wahr ist. Dann wird S wie eine unteilbare
Operation ausgeführt. Nach dem Ende von S wird die Parallelarbeit
fortgesetzt.





@HBDie Beweisregeln für die beiden Sprachelemente lauten:

  a) COBEGIN
@HA                       {Pi} Si {Qi}        für i = 1..n
        ───────────────────────────────────────────────────────────
         {P1, ..., Pn} COBEGIN S1; S2; ...; Sn COEND {Q1, ..., Qn}

@HB     Da S1, S2, ..., Sn parallel arbeiten dürfen, müssen die
     Zusicherungen (Pi, Qi) unabhängig voneinander sein.

  b) AWAIT
@HA            {P AND B} S {Qi}
        ────────────────────────
         {P} AWAIT B THEN S {Q}

     @HBDas AWAIT-Statement kann nur betreten werden, wenn B wahr ist.
     Nach dem Verlassen des Statements kann über B keine Aussage gemacht
     werden.

@HEBeispiel:

@HBZu beweisen ist folgendes Programmstück, das als Ergebnis x = 3
liefert:

@HA     x := 0;
     COBEGIN
       AWAIT TRUE THEN x := x + 1;
       AWAIT TRUE THEN x := x + 2;
     COEND;








     @HAx := 0;
     @HB{x = 0}
     @HACOBEGIN @HB{x = 0}
       @HB{x = 0 OR x = 2}
       @HAAWAIT TRUE THEN x := x + 1;
       @HB{x = 1 OR x = 3}

       @HB{x = 0 OR x = 1}
       @HAAWAIT TRUE THEN x := x + 2;
       @HB{x = 2 OR x = 3}
     @HACOEND;
     @HB{(x = 1 OR x = 3) AND (x = 2 OR x = 3)} ==> {x = 3}

@HBFür dieses triviale Beispiel ist die Beweismethode geeignet,
aber sie ist nicht realistisch für umfangreichere Programme.



@HBEin wenig kann man sich helfen, indem man Hilfsvariablen einführt.
Dabei muß man aber beachten:

  1. Hilfsvariablen h dürfen nur in Zuweisungen der Form h := expr
     vorkommen, wobei expr eine Expresssion ist, in der kein h
     vorkommen darf.

  2. hi darf nur in Statement Si vorkommen

  3. Das Originalprogramm muß nach dem Entfernen der Hilfsvariablen
     erhalten bleiben.






@HBDas obige Beispiel lautet dann:

     @HAx := 0;
     h1 := 0;
     h2 := 0;
     COBEGIN
       AWAIT TRUE THEN
         BEGIN
           x := x + 1;
           h1 := 1;
         END;
       AWAIT TRUE THEN
         BEGIN
           x := x + 2;
           h2 := 2;
         END;
     COEND;
     @HBmit {x = h1 + h2} als Invariante
@HBDie Beweismethode von Gries und Owicki erlaubt es auch, Semaphor-
Konstruktionen zu beweisen. Dazu muß man allerdings die P- und
V-Ausdrücke in das AWAIT-Statement übersetzen.

@HBDie ursprüngliche Definition für Semaphore:

@HA  P (s) ::= { IF s = 0 THEN Warte (s);
              s := s - 1; }

  V (s) ::= { s := s + 1;
              IF "jemand wartet auf s" THEN Wecke (s); }

@HBwird dann zu:

@HA  P (s) ::= AWAIT s > 0 THEN s := s - 1;

  V (s) ::= AWAIT TRUE THEN s := s + 1;

@HEErweiterung der Beweismethode
@HBOwicki und Gries haben bei ihrer Erweiterung folgende zwei Statements
entwickelt:

  a) RESOURCE r1 (SHARED VARIABLE LIST), ..., rm (SHARED VARIABLE LIST):
       COBEGIN S1 ||...|| Sn COEND

  b) WITH r WHEN B DO S                  (* critical section statement *)
     (zum Vergleich: REGION V THEN B DO S)
     wobei r eine Menge von Betriebsmitteln (shared variables),
           B Boolean Expression und
           S Statement, das die Variablen aus r verwendet, ist.

Wenn ein Prozeß versucht das Critical-Section-Statement auszuführen,
wird er solange zurückgestellt, bis B wahr ist und r nicht von einem
anderen Prozeß verwendet wird. Ist B wahr und der Prozeß besitzt r, dann
wird S ausgeführt. Nach dem Ende von S ist r wieder frei für andere
Prozesse.
@HBDas Statement kann nur innerhalb von parallelen Prozeßabläufen vor-
kommen. Für das gleiche r ist eine Verschachtelung des Statements nicht
erlaubt.

Durch die folgenden Syntaxregeln wird erreicht, daß alle shared
variables, wegen denen es zu Synchronisationsproblemen kommen kann,
durch das kritische Gebiet (critical section statement) geschützt sind.

  a) Wenn eine Variable x zur Resource r gehört, dann darf x nur in einem
     kritischen Gebiet für r vorkommen.

  b) Wenn x in einem Statement S verändert wird, dann muß es zu einer
     Resource r gehören.

Diese beiden Regeln vereinfachen die Korrektheitsbeweise von Programmen
und sie sind vom Compiler überprüfbar.



@HBFür die Betriebsmittel r wurde eine Invariante I (r) definiert. Sie
muß wahr sein, wenn die parallele Abarbeitung der Prozesse beginnt und
im weiteren immer dann gültig, wenn kein kritisches Gebiet (critical
section statement) für r ausgeführt ist (das heißt vor dem Betreten des
kritischen Gebietes für r stehen die Betriebsmittel r zur Verfügung und
nach dem Verlassen des kritischen Gebiets für r werden alle Betriebs-
mittel die zu r gehören wieder freigegeben).










@HBDie Invariante wird bei den beiden Beweisaxiomen verwendet:

  a) Axiom für paralleles Arbeiten

@HA                     für alle i:     {Pi} Si {Qi}
        ───────────────────────────────────────────────────────────
               {I (r) AND P1 AND ... AND Pn} RESOURCE r:
         COBEGIN S1 ||...|| Sn COEND {I (r) AND Q1 AND ... AND Qn}

@HB  b) Axiom für kritisches Gebiet

@HA           {I (r) AND P AND B} S {I (r) AND Q}
          ─────────────────────────────────────
               {P} WITH r WHEN B DO S {Q}


    @HBweiter mit ⌐Monitore - Beweis@BS___3¬
    @HBsiehe auch: Beweismethode nach ⌐Habermann@BS___3¬
AHBAA #!!# Monitore - Beweis
@HEBeweismethoden für Monitore (nach Hoare)
@HBFür Monitore wurden folgende Beweisregeln aufgestellt:

  1. {true}      Initialisierung   {J AND E}
  2. {J AND E}   jede Prozedur     {J AND E}
  3. {J AND E}   cond.wait         {J AND B}
  4. {J AND B}   cond.signal       {J AND E}

Dabei bedeutet

@HPJ@HB: Eine Invariante, die die Korrektheit der Monitordaten zusichern soll.
@HPB@HB: Eine Zusicherung, daß für jede cond-Variable eine signal-Operation
   ausgeführt wird. B beschreibt die Bedingungen, die für das Wecken
   Voraussetzung sind.
@HPE@HB: Eine Zusicherung, daß unnötiges Warten nicht erlaubt ist, das heißt
   daß nach einer signal-Operation sofort ein Prozeß geweckt wird
   (wichtig, weil dann der geweckte Prozeß genau die Daten vorfindet, wie
   sie bei der signal-Operation gelten).
@HBMan kann sich die Arbeit des Beweises erleichtern, indem man auch hier
"history-variables" verwendet. (Sie dienen nur der Beschreibung und
werden nicht implementiert.)

Als nächstes sucht man sich eine Invariante und zeigt, daß sie
tatsächlich gilt.

@HEBeispiel: Erzeuger-Verbraucher Problem

@HBHistory-Variables:
  @HPA@HB : enthält alle Infos, die jemals in den Puffer gelegt wurden
  @HPR@HB : enthält alle Infos, die jemals aus dem Puffer entfernt wurden
  @HPS@HB : enthält alle Infos, die im Puffer liegen (Differenz von A und R)

Invariante:

   @HPA = R konkat S@HB              mit konkat = Verkettung, Konkatenation

@HEDer Monitor mit History-Variables:

@HABoundedBuffer : MONITOR
  BEGIN
    VAR
    A, R : ARRAY [1..unendlich] OF Message;
    S : ARRAY [1..BufSize] OF Message;
    NotFull, NotEmpty : Condition;

    PROCEDURE Append (x : Message);
      BEGIN
        IF S.Lenght = BuffSize THEN NotFull.Wait;
        A := A konkat <x>;
        S := S konkat <X>;
        IF NotEmpty.Queue THEN NotEmpty.Signal;
      END;


    PROCEDURE Remove (x : Message);
      BEGIN
        IF S.Length = 0 THEN NotEmpty.Wait;
        x := S.First;
        S := S.Rest;
        R := R konkat <x>;
        IF NotFull.Queue THEN NotFull.Signal;
      END;

    @HB(* Initialisierung: *)@HA
    A := R := S := <>        @HB(* empty *)@HA
  END;

@HBS.Append (x) bedeutet S := S konkat <x>
S.Remove (x) bedeutet x := S.First; S := S.Reset




@HBInvariante: A = R konkat S

@HEBeweis der append-Prozedur:

  @HB{A = R konkat S} ==> {A konkat <x> = R konkat S konkat <x>}
  @HAA := A konkat <x>;
  @HB{A = R konkat S konkat <x>}
  @HAS := S konkat <x>;
  @HB{A = R konkat S}








@HEBeweis der remove-Prozedur:

  @HB{A = R konkat S AND S ist nicht leer} ==>
  {A = R konkat S.First konkat S.Rest}
  @HAx := S.First;
  @HB{A = R konkat <x> konkat S.Rest}
  @HAS := S.Rest;
  @HB{A = R konkat <x> konkat S}
  @HAR := R konkat <x>;
  @HB{A = R konkat S}

@HBDie Initialisierung sowie die Funktionsweise von signal und wait
muß noch bewiesen werden. Dann hat man gezeigt, daß A = R konkat S
tatsächlich invariant ist.




@HEBeweis der Initialisierung:

  @HB{true} ==> {<> = <> konkat <>}
  @HAA := <>;
  @HB{<> = <> konkat <> AND A = <>} ==> {A = <> konkat <>}
  @HAR := <>;
  @HB{A  = <> konkat <> AND R = <>} ==> {A = R  konkat <>}
  @HAS := <>;
  @HB{A  =  R konkat <> AND S = <>} ==> {A = R  konkat S }


@HB     weiter mit: Deadlocks, ⌐Betriebsmittel II@BS___4¬
     siehe auch: ⌐Monitore@BS1¬
                 ⌐Monitore II@BS___3¬