next up previous contents
Next: Speichermodell und Synchronisierung Up: Das Speichermodell Previous: Formalisierung   Inhalt

Sequential Consistency

Die Komplexität nebenläufiger Berechnungen auf einem gemeinsamen Speicher wurde früh erkannt. Lamport formulierte daher das Modell der ,,Sequential Consistency``: die beobachteten Veränderungen des Speichers müssen einer global geordneten Ausführung der Speicheroperationen entsprechen, wobei diese pro Prozessor in Programmordnung erfolgen [Lamport, 1979]. Viele der klassischen Synchronisierungsalgorithmen wie z.B. ,,Dekker's Algorithm`` beruhen auf ,,Sequential Consistency``.

Unglücklicherweise verhindert ,,Sequential Consistency`` viele der oben angesprochenen Optimierungen. Da nicht bekannt ist, welche Operationen von nebenläufigen Prozessen auf dem Speicher ausgeführt werden, können Programmoperationen im Gegensatz zum sequentiellen Fall nicht transparent umgeordnet werden. Bezogen auf das formale Modell bedeutet ,,Sequential Consistency`` eine Präzedenz zwischen je zwei im Programm aufeinanderfolgenden Aufträgen. Der erwartete Effizienzgewinn durch den Einsatz mehrerer Prozessoren wird somit durch den Verlust an Optimierungen geschmälert oder gar zunichte gemacht. Aus diesem Grunde implementieren moderne Multiprozessorarchitekturen weitaus lockerere Speichermodelle ([Adve and Gharachorloo, 1995] geben eine sehr gute Einführung). Diese Speichermodelle garantieren nicht, wann genau ein Prozessor Auswirkungen von Speicheroperationen anderer Prozessoren wahrnehmen kann2.9.

Um das Verhalten des Prozessors zu beeinflussen und die Sichtbarkeit von Schreiboperationen an bestimmten Programmpunkten zu erzwingen, bieten genannte Architekturen explizite Markierungsinstruktionen (sogenannte memory barriers). Diese geben sozusagen Grenzmarkierungen vor, innerhalb derer optimiert werden darf, und ermöglichen somit den konsistenten Informationstransfer über den gemeinsamen Speicher.

Im Modell entspricht eine memory barrier einem Auftrag, der von allen Variablen liest und auf alle schreibt. Mit Hilfe der Datenflußrelation stellt eine memory barrier also transitiv Präzedenzen zwischen den vorhergehenden und den folgenden Speicheroperationen her; im obigen Beispiel sich somit der ,,unerwünschte`` Zustand x = 0, ok = true im Speicher verhindern2.10.


next up previous contents
Next: Speichermodell und Synchronisierung Up: Das Speichermodell Previous: Formalisierung   Inhalt

2001-02-28