Begriff
Sequential Consistency
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Schwächer als Linearizability, aber oft gut genug. Es ist egal, wann genau etwas passiert (Echtzeit ist irrelevant). Wichtig ist nur, dass alle Teilnehmer die gleiche Reihenfolge sehen. Beispiel: A postet: "Wer will Eis?" B postet: "Ich!" C liest. Linearizability: C sieht erst A, dann B. Sequential: C könnte erst B, dann A sehen ("Ich!" -> "Wer will Eis?"). Das wäre verwirrend, aber erlaubt, solange D das auch so sieht. Aber meistens meint man: Die Befehle eines Programms werden in der Reihenfolge ausgeführt, wie sie im Code stehen. Erklärt von Leslie Lamport (1979).
Merksatz: Ein Konsistenzmodell, das sicherstellt, dass die Ausführung von Operationen so erscheint, als ob sie in einer bestimmten sequenziellen Reihenfolge stattgefunden hätten, die mit der Programmreihenfolge jedes einzelnen Prozessors übereinstimmt.
- Java
volatile: Garantiert Sequential Consistency für diese Variable. - CPU Memory Models: x86 garantiert fast Sequential Consistency (TSO). ARM ist viel schwächer (Relaxed).
- ZooKeeper: Garantiert Sequential Consistency für Updates.
1. Definition
"The result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program." Es erlaubt das "Verschieben" von Operationen verschiedener Prozessoren gegeneinander, solange die lokale Ordnung erhalten bleibt.
2. Lipton's Sandwich
Ein Beweis-Trick. Man kann Sequentielle Konsistenz beweisen, indem man Operationen "nach links" oder "nach rechts" schiebt (Commuting Operations), bis alles seriell aussieht.
1. TSO (Total Store Order) auf x86
Echte Hardware ist fast nie Sequential Consistent, weil sie dann zu langsam wäre (sie müsste bei jedem Write auf alle Caches warten).
Intel x86 nutzt TSO. Alle Schreibbefehle eines Kerns werden in einen Store Buffer gelegt.
Andere Kerne sehen die Writes vielleicht später. Aber: Der Schreibende Kern sieht seine eigenen Writes sofort.
Der einzige Fall, der Sequential Consistency bricht: Wenn zwei Kerne gleichzeitig schreiben und gleichzeitig lesen (Dekker's Algorithmus). Um das zu fixen, brauchen Programmierer MFENCE oder LOCK-Instruktionen, die den Store Buffer leeren (Flush).
2. SC-DRF (Sequential Consistency for Data Race Free Programs)
Das ist das Versprechen moderner Sprachen (Java, C++11, Go). "Wenn du dein Programm so schreibst, dass es keine Data Races hat (also alle geteilten Variablen mit Locks oder Atomic geschützt sind), dann garantieren wir dir, dass sich das Programm verhält, als wäre es Sequential Consistent." Hinter den Kulissen macht der Compiler und die CPU immer noch wilden Optimierungs-Voodoo, aber durch die Locks wird sichergestellt, dass du davon nichts merkst. Das ist der Kompromiss zwischen Performance und geistiger Gesundheit der Entwickler.
3. Sequential vs. Linearizability
Oft verwechselt.
- Linearizability: Jede Operation wirkt sofort (atomar). Wenn ich um 12:00:00:001 schreibe, sieht jeder, der um 12:00:00:002 liest, den neuen Wert.
- Sequential Consistency: Die Zeit ist dehnbar. Wenn ich schreibe, sieht mein Nachbar es vielleicht erst eine Sekunde später – Hauptsache, er sieht alle meine Schreibvorgänge in der richtigen Reihenfolge und wir beide einigen uns auf eine globale Reihenfolge mit allen anderen Teilnehmern. Sequential ist also "lokaler". Es skaliert besser in verteilten Systemen, weil man keine global synchronisierte Uhr (Atomic Clock) braucht.
Quick-Check
Schneller als Linearizability?
Ja. Man muss nicht auf die echte Uhr warten. Caches dürfen genutzt werden, solange sie sich synchronisieren.Reicht das?
Für Social Media User Feeds ("Timeline") oft ja. Für Bankkonten nein.ARM?
ARM-CPUs sind nicht Sequential Consistent. Sie können Befehle wild umordnen (Out-of-Order). Man braucht "Memory Barriers", um SC zu erzwingen.