next up previous contents
Next: Sequential Consistency Up: Das Speichermodell Previous: Das Speichermodell   Inhalt

Formalisierung

Moderne Prozessoren werden abstrakt in Form von processor architectures spezifiziert, um im folgenden als Prozessorfamilie mehrere Entwicklungszyklen zu durchlaufen. Hierzu zählen die SPARC-, Alpha- und PowerPC-Architekturen [Weaver and Germond, 1994,Sites, 1992,May et al., 1994]. Um sicherzustellen, daß die Prozessoren auch in Multiprozessor-Umgebungen ein vorhersagbares Verhalten aufweisen, muß das Speichermodell formuliert werden. Insbesondere durch die hohe Komplexität nebenläufiger Ausführung bietet sich eine formale Beschreibung an.

Beispielhaft wird hier grob eine Formalisierung mit Hilfe schematischer Auftragssysteme [Jessen and Valk, 1987] skizziert: ein auszuführendes Programm bzw. ein Fragment, das dem Prozessor bereits vorliegt, entspricht in diesem Modell einer Ausführungsfolge w eines schematischen Auftragssystems mit Lese- und Schreibaufträgen auf Registern und dem globalen Speicher2.8. Durch das Speichermodell können Präzedenzen auf den Aufträgen definiert sein, die über die Wahrung des Datenflusses, d.h. die Werteübertragungsrelation hinausgehen.

Das Prozessorverhalten läßt sich nun mit Hilfe des Modells spezifizieren: eine Ausführung w' durch den Prozessor wird dann als korrekt angesehen, wenn w' äquivalent zu w ist, d.h. für beliebige Eingaben das selbe Ergebnis liefert.

Gebräuchliche Speichermodelle für Multiprozessoren fordern keine zusätzlichen Präzedenzen auf den Aufträgen, d.h., unter Wahrung des Daten- und Kontrollflusses sind beliebige Umordnungen von Speicheroperationen möglich. Das hat zur Folge, daß die ,,von außen`` sichtbare Zustandsfolge der Speichervariablen von w' sich von der von w unterscheiden kann. Die Auswirkungen werden anhand eines Beispiels erläutert. Gegeben sei das folgende Codefragment:

  ; initially: x = 0, ok = false
  store x, <some value>
  store ok, true

Die ensprechende Ausführungsfolge lautet dann

w = l0[],s0[x,ok],l1[],s1[x],l2[],s2[ok],l3[x,ok],s3[]

(l0,s0,l3,s3 stellen den Initialisierungs- bzw. Ausgabeauftrag dar). Das zugehörige Auftragssystem ist in Abbildung 2.10 abgebildet.

Abbildung 2.10: Auftragssystem
\includegraphics{nebenlaeufigkeit/util/memory-model-1}

Die Ausführungsfolge

w' = l0[],s0[x,ok],l2[],s2[ok],l1[],s1[x],l3[x,ok],s3[]

ist äquivalent zu w. Aus diesem Grunde können beide Zuordnungen legal vertauscht werden. Es wäre somit für ein anderes Programm möglich, den inkonsistenten Zustand x = 0, ok = true im Speicher zu beobachten.

Dieses Modell ist unvollständig und verdeutlicht lediglich den Charakter und Eigenschaften eines Speichermodells. Eine realistische Spezifikation findet sich in [Broy, 1995]; hier wird mit anderen Mitteln das Speichermodell der Alpha-Architektur formalisiert.


next up previous contents
Next: Sequential Consistency Up: Das Speichermodell Previous: Das Speichermodell   Inhalt

2001-02-28