Linearizability

Stell dir eine Variable x vor. In einem System mit Linearizability verhält sich x so, als gäbe es nur eine einzige Kopie davon. Egal ob du 100 Server hast (Replikas). Wenn Client A x=5 schreibt und "OK" bekommt. Dann muss Client B (der eine Nanosekunde später liest) 5 sehen. Es darf niemals passieren, dass Client B noch 0 sieht (Stale Read). Das ist die stärkste Form der Konsistenz. Es gibt keine "Zeitparadoxien". Der Preis: Wenn das Netzwerk langsam ist, muss das System stehenbleiben (CP im CAP-Theorem).

Merksatz: Das stärkste Konsistenzmodell für verteilte Systeme, das garantiert, dass jede Operation atomar zu einem einzigen Zeitpunkt zwischen Aufruf und Antwort stattfindet, sodass sich das System verhält, als gäbe es nur eine einzige Kopie der Daten.

ZooKeeper / Etcd: Nutzen Consensus (Raft/ZAB), um Linearizability für Writes zu garantieren. (Reads sind oft "Sequential Consistent", es sei denn man fordert "Linearizable Read").
Google Spanner: Garantiert "External Consistency" (was Linearizability + Uhrzeit ist).

1. The Real-Time Constraint

Linearizability respektiert die echte Zeit (Wall-Clock Time). Wenn Operation A endet (Zeit $t_1$), bevor Operation B beginnt (Zeit $t_2$), dann muss A vor B passieren. Andere Modelle (Sequential Consistency) erlauben, dass B vor A rutscht, solange es für einen Beobachter logisch aussieht. Linearizability erlaubt das nicht.

2. Composable

Ein riesiger Vorteil: Linearizability ist komponierbar. Wenn System A linearisierbar ist und System B linearisierbar ist, dann ist auch das Gesamtsystem A+B linearisierbar. Das gilt für andere Modelle (wie Serializability) NICHT.

1. Linearization Points (L-Points)

Wie beweist man, dass ein komplexer Algorithmus (wie eine lock-free Queue) linearisierbar ist? Man sucht den Linearization Point. Das ist die exakte Code-Zeile (oder der ASM-Befehl), an dem die Operation "wirklich" passiert. Bei einer CAS-Operation (Compare-And-Swap) ist es genau der Moment, in dem die CPU den Speicherwert austauscht. Alles davor ist "Vorbereitung", alles danach ist "Aufräumen". Wenn man für jede Methode einen L-Point findet, der zwischen Start und Ende der Methode liegt, ist der Beweis für Linearizability erbracht.

2. Wait-Freedom vs. Linearizability

Linearizability ist ein Sicherheits-Property (was darf passieren?). Wait-Freedom ist ein Liveness-Property (wird es jemals fertig?). In der High-Performance Produktion (z.B. im Linux Kernel Scheduler) sucht man Algorithmen, die beides erfüllen. Ein wait-free Algorithmus garantiert, dass jeder Thread nach einer endlichen Anzahl von Schritten fertig wird, unabhängig von anderen Threads. Linearizability garantiert dabei, dass die Ergebnisse für alle Threads logisch konsistent aussehen. Das zu kombinieren ist die "Königsdisziplin" des Concurrent Programmings.

3. TLA+ und die Grenzen von Paxos/Raft

In der Forschung nutzt man TLA+ (Temporal Logic of Actions), um Linearizability in Protokollen wie Raft formal zu beweisen. Dabei zeigt sich oft: Ein Protokoll kann linearisierbare Writes garantieren, aber standardmäßig nur Sequential Consistent Reads liefern (weil ein Reader vielleicht einen veralteten Leader fragt). Um "Linearizable Reads" zu erhalten, muss der Leader vor jeder Antwort erst wieder ein Quorum von Followern fragen ("Read Index") oder eine "Lease" (Zeitfenster) besitzen. Diese feinen Details entscheiden in der Produktion darüber, ob deine Datenbank bei einem Netzwerk-Partition-Fehler (Split Brain) Daten verliert oder nicht.