2a. Ergänzungen und Erweiterungen


2a.0 Notation


con $S_1; \ldots; S_n$ end entspricht
       Thread t1 = new Thread(new R1());
       ...
       Thread tn = new Thread(new Rn());

       t1.start(); ... tn.start();

       t1.join(); ... tn.join();
zusammen mit
      class Ri implements Runnable {
            public void run() { Si; }
      }


atomic $S_1; \ldots; S_n$ end entspricht
       Object lock = new Object();
       ...
       synchronized (lock) { S1; ...; Sn; }


await B then $S_1; \ldots; S_n$ end entspricht
   /* init */
           Object condb = new Object();
   
   /* waiter */  
           synchronized (condb) {
                  while (! B) condb.wait();
                  S1; ...; Sn; 
           }
   
   /* tester */  
           // B koennte wahr werden
           if (B) condb.notify();


2a.1 Annahmen zum Prozessormodell

Um einschätzen zu können, an welchen Stellen und in welchen Situationen wir synchronisieren müssen, wollen wir uns kurz über die dafür wichtigen Prozessoreigenschaften informieren. Daraus leiten wir dann einige Regeln zur Verwendung von atomic bzw. synchronized ab.

  In den meisten registerbasierten CPUs, d.h. in allen modernen Prozessoren, sind die elementaren Maschinenoperationen  oft atomar. Auch in interpretierten Programmiersprachen wie Java sind die Operationen mit Datentypen, die im Prozessor per Maschinenbefehl ausgeführt werden, atomar. Genauer werden wir folgende Annahmen machen.  

Die atomaren Datentypen von Java sind in der Abbildung 1.3 (in Abschnitt 2) zusammengestellt. Dort sind long und double als nicht atomar gekennzeichnet. Weiter sind auch zusammengesetzte Objekte meist nicht atomar.

Die obigen Annahmen sind oft bei CPUs mit parallelen Ausführungseinheiten für Berechnungen und Adressdekodierungen nicht erfüllt, aber es ist sichergestellt, daß die obigen Annahmen aus Programmsicht erfüllt sind. Zum Beispiel auf Rechnern mit Cache-Architektur (wie bei fast allen RISC-CPUs) gilt folgendes:  

Für die Programmierung von Parallelrechnern ergeben sich somit folgende Regeln:

1.
Es sollen keine Annahmen über den zeitlichen Ablauf der Operationen getroffen werden! Alle Abhängigkeiten sind explizit abzuwarten (wie das geschieht, wird im nächsten Abschnitt besprochen).
2.
Falls in einem Programmteil keine globalen Variablen gelesen oder geschrieben werden, ist der Programmteil atomar.
3.
Falls bei der Auswertung eines Ausdrucks eine einzige globale Variable nur einmal gelesen oder geschrieben wird, ist die Auswertung atomar.
4.
Die Zuweisung zu einer lokalen Variablen x= expr ist atomar, falls die Auswertung von expr atomar ist.
5.
Die Zuweisung zu einer globalen Variablen x= expr ist atomar, falls die Auswertung von expr nur lokale Variablen benötigt, die nicht Ergebnis einer Berechnung mit globalen Variablen sind, oder die enthaltenen globalen Variablen nicht von einem anderen Prozeß beschrieben werden.
Zum Beispiel sind die Auswertungen in der Multiplikation von Matrizen atomar, da die Elemente der Matrizen A und B nur gelesen werden, die Variable s jeweils lokal deklariert ist und die Elemente der Matrix C nur einmal geschrieben werden.

2a.2 Interferenz

Bei noch nicht richtig synchronisierten Programmen kann es vorkommen, daß Programmzustände in anderen Prozessen den Zustand in einem Prozeß beeinflussen. Dieses Verhalten nennt man Interferenz.  Das Ziel der parallelen Programmierung ist es, diese Beeinflussung zu erkennen, zu vermeiden, beziehungsweise die wechselseitigen Beeinflussungen zu synchronisieren.

Die Möglichkeiten zur Vermeidung von Interferenz sind die folgenden:

2a.3 Programmeigenschaften

Bevor wir uns im nächsten Kapitel an die Implementierung von parallelen Algorithmen wagen, wollen wir in diesem Abschnitt der Frage nachgehen, ob ein Programm ``richtig'' oder ``korrekt'' ist, d.h. ob ein Programm in jeder Situation genau das tut, was es soll, und ob es die Ergebnisse liefert, die wir erwarten. In kniffeligen Situationen wird man versuchen, die Nachweise für die Korrektheit streng formal durchzuführen, damit nur ja kein entscheidender Fall vergessen wird. Eine Besprechung dieses Formalismus, (genannt axiomatische Semantik)   liegt außerhalb der Thematik dieses Buches. Wer sich dafür interessiert, kann dies z.B. in dem Buch von Andrews [And91] finden. Wir geben hier nur eine kurze Einführung in die Konzepte. Dabei führen wir zunächst die nötigen Begriffe ein und besprechen dann die für parallele Programme wichtigen Begriffe genauer. Besonders der letzte Teil ist wegen der Scheduling-Problematik im weiteren wichtig.

Um über die Korrektheit von Programmen zu diskutieren, benutzt man die Begriffe ``Sicherheit''  und ``Lebendigkeit''.   Ein Programm ist sicher, falls keine schlechten (fehlerhaften) Zustände eintreten können. Ein Programm ist lebendig, falls irgendwann alle gewünschten Zustände eintreten.

Bei sequentiellen Programmen haben diese Eigenschaften folgende Bedeutung.

Sicherheit:
partielle Korrektheit.  Der Programmteil oder eine Methode liefert für alle möglichen Eingaben (die zulässig sind, und für die terminiert wird) die richtigen Ergebnisse.
Lebendigkeit:
Terminierung . Der Programmteil oder eine Methode endet nach endlich-vielen Schritten, d.h. nach endlicher Zeit.
Ein Programmteil wird als korrekt bezeichnet, falls es partiell korrekt ist und terminiert.  Die Trennung der beiden Begriffe kommt daher, daß der Nachweis der partiellen Korrektheit meist mit Mitteln der Prädikatenlogik (zum Teil auch maschinell) machbar ist, während der Nachweis der Terminierung oft mächtigere Methoden verlangt.  

Bei parallelen Programmen kommen folgende Bedingungen, die wir im folgenden ausführlicher besprechen, hinzu.

Sicherheit:
Keine Interferenz in kritischen Bereichen und keine Verklemmung (Deadlock-Freiheit).   
Lebendigkeit:
Jeder Programmteil erhält eine `faire' Chance ausgeführt zu werden (fair scheduling).   Es tritt kein Live Lock  ein; dabei tut jeder nicht terminierte Prozeß etwas, aber ohne die Arbeit voranzubringen.

Ein Nachweis für die Korrektheit eines parallelen Programms setzt sich dann zusammen aus den Nachweisen der Korrektheit für die sequentiellen Abschnitte (partielle Korrektheit und Terminierung), aus Beweisen für Interferenz-Freiheit und Deadlock-Freiheit von nebenläufigen Abschnitten sowie Beweisen für die Fairness des benutzten oder implementierten Schedulings.      

2a.3.1 Sicherheit

  Bei den formalen Beweisen werden jedem Programmteil zwei Prädikate zugeordnet (Prädikate sind Boolesche Ausdrücke die auch andere mathematische Konstrukte enthalten dürfen). Das erste Prädikat wird als Vorbedingung (Precondition) bezeichnet und beschreibt die Bedingung, die gelten muß, damit der Programmteil sinnvoll ausgeführt werden kann. Und das zweite, als Nachbedingung (Postcondition) bezeichnet, beschreibt die Bedingung, die gilt, nachdem der Programmteil ausgeführt wurde. Eine Bedingung heißt Invariante, wenn sie sowohl vor als auch nach der Ausführung eines Programmteils gilt. Ein Programm ist damit partiell korrekt, falls die Vorbedingung des ersten Programmteils und die Nachbedingung des letzten (ausgeführten) Programmteils die gewünschte Anforderung für das Programm erfüllt und falls die Vorbedingungen aller Programmteile von den Nachbedingungen der vorhergehenden Programmteile erfüllt (impliziert) werden.         

Beweise für die Deadlock-Freiheit kann man damit wie folgt konzipieren. Wenn etwa BAD ein Prädikat bezeichnet, das einen Deadlock charakterisiert, so könnte man zeigen, daß

für alle Vorbedingungen Q in allen Programmteilen gilt
Q $\Longrightarrow$ $\neg$ BAD.
Womit dann bewiesen wäre, daß die Bedingung BAD nicht eintreten kann, das Programm also Deadlock-frei wäre.

Eine andere Technik benutzt eine Invariante  I, die in allen Programmteilen gilt, und zeigt

I $\Longrightarrow$ $\neg$ BAD.
Wodurch dann ebenfalls sichergestellt ist, daß BAD nicht eintreten kann.

Ist das nicht möglich, kann eventuell noch durch sogenanntes exclusion of configurations    zum Beispiel durch explizites await sichergestellt werden, daß keine Interferenz auftritt.

2a.3.2 Lebendigkeit

   Bei der Programmeigenschaft Lebendigkeit unterscheiden wir die entsprechenden Eigenschaften des Laufzeitsystems des Computers und den vom Programmierer realisierten Ablauf des gesamten parallelen Programms. Zunächst muß das Laufzeitsystem des Computers natürlich durch die richtige Implementierung von con, atomic und await dafür sorgen, daß kein Programmteil bevorzugt wird und auch die await-Bedingungen genügend oft wahr werden. Aber auch das Programm selbst muß so geschrieben sein, daß nicht durch ungünstige zeitliche Abläufe einige Programmteile nicht ausgeführt werden. In diesem Abschnitt führen wir die notwendigen Begriffe ein; die Anwendung dieser Begriffe auf Java wird in Abschnitt 6.5 [von K+Y] vorgestellt.

Die Eigenschaften des Laufzeitsystems des Computers werden unter dem Begriff Scheduling-Strategien zusammengefaßt.   Hier werden folgende Begriffe unterschieden  

1.
unconditionally fair  für atomare Aktionen.
2.
weak fair:  unconditionally fair, und bei await werden die Bedingungen auch einmal wahr.
3.
strong fair:  unconditionally fair, und bei await werden die Bedingungen unendlich oft wahr.

Der erste Begriff verlangt die Fairness beim con- und atomic-Statement. Die beiden anderen Begriffe beziehen sich auf den Fall, daß das await Statement hinzukommt. Zur Verdeutlichung der Begriffe betrachten wir einige Beispiele.


  
Abbildung 2.4: unconditionaly fair Scheduling
\framebox{
\begin{minipage}{10cm}
\begin{tabbing}
cont={\bf true}; \\
{\bf co...
.../ {\bf end}; \\
cont={\bf false}; \\
{\bf end};
\end{tabbing}\end{minipage}}

 

In Abbildung 2.4 wird bei `unconditionally fair' Scheduling auch das Statement cont=false einmal ausgeführt, wodurch dann die while-Schleife beendet wird und das con-Statement terminiert. Ein unconditional fair Scheduling ist vom Betriebssystem z.B. durch Round-Robin-Prozess-Scheduling einfach realisierbar.  Dabei werden die Prozesse wie Perlen an einem Rosenkranz reihum aktiviert und deaktiviert.

In Abbildung 2.5 folgt bei `weak fair' Scheduling u.U. keine Terminierung, denn das await-Statement wird zwar unendlich oft ausgeführt, aber es ist nicht sichergestellt, daß in diesem Moment `try' den Wert true hat. In diesem Fall wird `cont' nie auf false gesetzt, und das while-Statement terminiert nicht. Nur bei `strong fair' Scheduling folgt die Terminierung, da dann garantiert wird, daß das await-Statement unendlich oft ausgeführt wird und die Bedingung auch unendlich oft den Wert true annimmt.


  
Abbildung 2.5: weak und strong fair scheduling
\framebox{
\begin{minipage}{9.5cm}
\begin{tabbing}
cont={\bf true}; try={\bf fa...
...f then }cont={\bf false}\ {\bf end}; \\
{\bf end}
\end{tabbing}\end{minipage}}

   

Wie man sieht, kann das nur der Fall sein, wenn das await-Statement genau zwischen den Statements try=true und try=false an der Stelle `tick' ausgeführt wird. Die Bestimmung dieses Zeitpunkts ist aber nur nach eingehender Analyse des Programmtextes möglich und kann praktisch nicht vom Betriebssystem und dem Laufzeitsystem durchgeführt werden. Dies ist nur in Spezialfällen realisierbar.

Für den Programmierer bedeutet dies, daß man sich in der Regel auf unconditionally fair Scheduling für atomare Aktionen verlassen kann. Praktisch nie wird aber ein strong fair Scheduling für await realisiert sein. Das heißt beim Entwickeln von Programmen müßte an Stellen, wie beim obigen Beispiel bei tick, ein weiteres await eingeführt werden, das wartet bis das andere await die Veränderung gesehen hat.


© Universität Mannheim, Rechenzentrum, 2000-2010.

Last modified: Wed Sep 12 21:29:36 CEST 2009