Sequentielle Konsistenz

In einer sequentiell konsistenten gleichzeitigen Ausführung scheinen Aktionen in einer globalen Totalordnung stattzufinden, wobei jedes Lesen einer bestimmten Variablen den Wert des letzten Schreibvorgangs sieht, der diese Variable beeinflusst hat. Die Totalordnung für Aktionen muss mit der Programmreihenfolge übereinstimmen. Ein Programm hat einen Datenwettlauf für eine gegebene Eingabe, wenn eine seiner sequentiell konsistenten Ausführungen zwei konfliktreiche Aktionen nebeneinanderstellt.

Dies ist das am einfachsten zu verstehende Speichermodell für Menschen, obwohl es nicht alle Verwirrung beseitigt, da Operationen an unerwarteten Stellen aufgeteilt werden können.

Happens-before-Konsistenz

Das Programm enthält eine Sammlung von Synchronisationsaktionen, die in Python derzeit Lock-Akquisitionen und -Freigaben sowie Thread-Starts und -Joins umfassen. Synchronisationsaktionen finden in einer globalen Totalordnung statt, die mit der Programmreihenfolge übereinstimmt (sie müssen nicht in einer Totalordnung stattfinden, aber das vereinfacht die Beschreibung des Modells). Eine Lock-Freigabe synchronisiert mit allen späteren Akquisitionen desselben Locks. Ähnlich gilt für t = threading.Thread(target=worker)

• Ein Aufruf von t.start() synchronisiert sich mit der ersten Anweisung in worker().
• Die Rückgabe von worker() synchronisiert sich mit der Rückgabe von t.join().
• Wenn die Rückgabe von t.start() vor (siehe unten) einem Aufruf von t.isAlive() erfolgt, der False zurückgibt, synchronisiert sich die Rückgabe von worker() mit diesem Aufruf.

Wir nennen die Quelle der synchronizes-with-Kante eine Release-Operation auf der betreffenden Variablen, und die Zielkante eine Acquire-Operation.

Die happens before-Ordnung ist die transitive Hülle der Programmreihenfolge mit den synchronizes-with-Kanten. Das heißt, Aktion A geschieht vor Aktion B, wenn

• A vor B in der Programmreihenfolge liegt (was bedeutet, dass sie im selben Thread laufen)
• A synchronisiert sich mit B
• Sie können B erreichen, indem Sie von A aus Happens-before-Kanten folgen.

Eine Ausführung eines Programms ist happens-before-konsistent, wenn jeder Lesevorgang R den Wert eines Schreibvorgangs W derselben Variablen sieht, so dass

• R nicht vor W geschieht, und
• Es gibt keinen anderen Schreibvorgang V, der W überschrieben hat, bevor R die Chance hatte, ihn zu sehen. (Das heißt, es kann nicht sein, dass W vor V vor R geschieht.)

Sie haben einen Datenwettlauf, wenn zwei konfliktierende Aktionen nicht durch happens-before zusammenhängen.

class Queue:
    def __init__(self):
        self.l = []
        self.cond = threading.Condition()

    def get():
        with self.cond:
            while not self.l:
                self.cond.wait()
            ret = self.l[0]
            self.l = self.l[1:]
            return ret

    def put(x):
        with self.cond:
            self.l.append(x)
            self.cond.notify()

myqueue = Queue()

def worker1():
    x = [7]
    myqueue.put(x)

def worker2():
    y = myqueue.get()
    print y

thread1 = threading.Thread(target=worker1)
thread2 = threading.Thread(target=worker2)
thread2.start()
thread1.start()

Zombie-Werte

Dieses Beispiel stammt aus dem Java Memory Model

Anfangs gilt p is q und p.x == 0.

Thread 1	Thread 2
r1 = p	r6 = p
r2 = r1.x	r6.x = 3
r3 = q
r4 = r3.x
r5 = r1.x

Kann erzeugen r2 == r5 == 0, aber r4 == 3, was beweist, dass p.x von 0 auf 3 und zurück auf 0 ging.

Ein guter Compiler möchte die redundante Ladung von p.x bei der Initialisierung von r5 optimieren, indem er einfach den Wert wiederverwendet, der bereits in r2 geladen wurde. Wir erhalten das seltsame Ergebnis, wenn Thread 1 den Speicher in dieser Reihenfolge sieht

Auswertung	Berechnet	Warum
r1 = p
r2 = r1.x	r2 == 0
r3 = q	r3 ist p
p.x = 3		Nebeneffekt von Thread 2
r4 = r3.x	r4 == 3
r5 = r2	r5 == 0	Optimiert aus r5 = r1.x, weil r2 == r1.x.

Inkonsistente Reihenfolgen

Aus N2177: Sequential Consistency for Atomics, auch bekannt als Independent Read of Independent Write (IRIW).

Anfangs gilt a == b == 0.

Thread 1	Thread 2	Thread 3	Thread 4
r1 = a	r3 = b	a = 1	b = 1
r2 = b	r4 = a

Wir könnten r1 == r3 == 1 und r2 == r4 == 0 erhalten, was beweist, dass a vor b geschrieben wurde (Daten von Thread 1), und dass b vor a geschrieben wurde (Daten von Thread 2). Siehe Spezielle Relativitätstheorie für ein reales Beispiel.

Dies kann geschehen, wenn Thread 1 und Thread 3 auf Prozessoren laufen, die sich nahe beieinander befinden, aber weit entfernt von den Prozessoren, auf denen Threads 2 und 4 laufen, und die Schreibvorgänge nicht über die gesamte Maschine übertragen werden, bevor sie für nahegelegene Threads sichtbar werden.

Weder Acquire/Release-Semantik noch explizite Speicherbarrieren können hier helfen. Die Konsistenz von Ordnungen ohne Sperrung erfordert detaillierte Kenntnisse des Speichermodells der Architektur, aber Java benötigt dies für Volatiles, also könnten wir eine Dokumentation für dessen Implementierer verwenden.

Ein Happens-before-Wettlauf, der kein sequentiell konsistenter Wettlauf ist

Aus dem POPL-Paper über das Java-Speichermodell [#JMM-popl].

Anfangs gilt x == y == 0.

Thread 1	Thread 2
r1 = x	r2 = y
if r1 != 0	if r2 != 0
y = 42	x = 42

Kann r1 == r2 == 42 erzielt werden???

In einer sequentiell konsistenten Ausführung gibt es keine Möglichkeit, eine aufeinanderfolgende Lese- und Schreiboperation auf dieselbe Variable zu erhalten, daher sollte das Programm als korrekt synchronisiert (wenn auch fragil) betrachtet werden und sollte nur r1 == r2 == 0 ergeben. Die folgende Ausführung ist jedoch happens-before-konsistent

Anweisung	Wert	Thread
r1 = x	42	1
if r1 != 0	wahr	1
y = 42		1
r2 = y	42	2
if r2 != 0	wahr	2
x = 42		2

WTF, fragst du dich vielleicht. Da es im ursprünglichen Programm keine Happens-before-Kanten zwischen Threads gab, kann das Lesen von x in Thread 1 beliebige Schreibvorgänge aus Thread 2 sehen, auch wenn diese nur stattfanden, weil das Lesen sie sah. Es gibt Datenwettläufe im Happens-before-Modell.

Wir wollen das nicht zulassen, daher reicht das Happens-before-Modell für Python nicht aus. Eine Regel, die wir zu Happens-before hinzufügen könnten, um dies zu verhindern, wäre

Wenn es in keiner sequentiell konsistenten Ausführung eines Programms Datenwettläufe gibt, sollte das Programm sequentiell konsistente Semantik haben.

Java erhält diese Regel als Satz, aber Python möchte vielleicht nicht die gesamte Maschinerie, die Sie zur Beweisführung benötigen.

Selbstlegitimierende Werte

Ebenfalls aus dem POPL-Paper über das Java-Speichermodell [#JMM-popl].

Anfangs gilt x == y == 0.

Thread 1	Thread 2
r1 = x	r2 = y
y = r1	x = r2

Kann x == y == 42 erzielt werden???

In einer sequentiell konsistenten Ausführung nein. In einer happens-before-konsistenten Ausführung ja: Das Lesen von x in Thread 1 darf den in Thread 2 geschriebenen Wert sehen, da keine Happens-before-Beziehungen zwischen den Threads bestehen. Dies könnte geschehen, wenn der Compiler oder Prozessor den Code wie folgt transformiert:

Thread 1	Thread 2
y = 42	r2 = y
r1 = x	x = r2
if r1 != 42
y = r1

Es kann ein Sicherheitsproblem verursachen, wenn der spekulierte Wert ein geheimes Objekt ist oder auf den Speicher zeigt, den ein Objekt zuvor belegt hat. Java legt großen Wert auf solche Sicherheitsprobleme, aber Python muss sie vielleicht nicht haben.

Uninitialisierte Werte (direkt)

Aus mehreren klassischen Double-Checked-Locking-Beispielen.

Anfangs gilt d == None.

Thread 1	Thread 2
while not d: pass	d = [3, 4]
assert d[1] == 4

Dies könnte einen IndexError auslösen, die Assertion fehlschlagen lassen oder, ohne entsprechende Sorgfalt bei der Implementierung, einen Absturz oder anderes undefiniertes Verhalten verursachen.

Thread 2 kann tatsächlich implementiert sein als

r1 = list()
r1.append(3)
r1.append(4)
d = r1

Da die Zuweisung an d und die Elementzuweisungen unabhängig sind, können der Compiler und der Prozessor dies optimieren zu

r1 = list()
d = r1
r1.append(3)
r1.append(4)

Was offensichtlich falsch ist und den IndexError erklärt. Wenn wir tiefer in die Implementierung von r1.append(3) schauen, stellen wir möglicherweise fest, dass es und d[1] nicht gleichzeitig ohne eigene Wettlaufbedingungen laufen können. In CPython (ohne GIL) würden diese Wettlaufbedingungen zu undefiniertem Verhalten führen.

Es gibt auch ein subtiles Problem auf der Leseseite, das dazu führen kann, dass der Wert von d[1] veraltet ist. Irgendwo in der Implementierung von list speichert es seine Inhalte als Array im Speicher. Dieses Array könnte sich im Cache von Thread 1 befinden. Wenn der Prozessor von Thread 1 d aus dem Hauptspeicher neu lädt, ohne den Speicher neu zu laden, der die Werte 3 und 4 enthalten sollte, könnte er stattdessen veraltete Werte sehen. Soweit ich weiß, kann dies tatsächlich nur auf Alphas und möglicherweise Itaniums vorkommen, und wir müssen es wahrscheinlich ohnehin verhindern, um Abstürze zu vermeiden.

Uninitialisierte Werte (Flag)

Aus mehreren weiteren Double-Checked-Locking-Beispielen.

Anfangs gilt d == dict() und initialized == False.

Thread 1	Thread 2
while not initialized: pass	d[‘a’] = 3
r1 = d[‘a’]	initialized = True
r2 = r1 == 3
assert r2

Dies könnte einen KeyError auslösen, die Assertion fehlschlagen lassen oder, ohne entsprechende Sorgfalt bei der Implementierung, einen Absturz oder anderes undefiniertes Verhalten verursachen.

Da d und initialized unabhängig sind (außer in Gedanken des Programmierers), können der Compiler und der Prozessor diese fast beliebig neu anordnen, außer dass die Assertion von Thread 1 nach der Schleife bleiben muss.

Inkonsistente Garantien durch Abhängigkeit von Datenabhängigkeiten

Dies ist ein Problem mit Java final Variablen und der vorgeschlagenen Datenabhängigkeitsordnung in C++0x.

Führe zuerst aus

g = []
def Init():
    g.extend([1,2,3])
    return [1,2,3]
h = None

Dann in zwei Threads

Thread 1	Thread 2
while not h: pass	r1 = Init()
assert h == [1,2,3]	freeze(r1)
assert h == g	h = r1

Wenn h Semantik ähnlich einer Java final Variable hat (außer dass sie einmal schreibbar ist), dann kann, obwohl die erste Assertion garantiert erfolgreich ist, die zweite fehlschlagen.

Datenabhängige Garantien, wie sie final bietet, funktionieren nur, wenn der Zugriff über die finale Variable erfolgt. Es ist nicht einmal sicher, auf dasselbe Objekt über eine andere Route zuzugreifen. Leider sind die Garantien von final aufgrund der Funktionsweise von Prozessoren nur dann günstig, wenn sie schwach sind.

Daten-Rennfreie Programme sind sequentiell konsistent

Wir möchten, dass Programmierer ihre Programme so nachvollziehen können, als wären sie sequentiell konsistent. Da es schwierig ist festzustellen, ob man einen Happens-before-Wettlauf geschrieben hat, wollen wir Programmierer nur dazu verpflichten, sequentielle Wettläufe zu verhindern. Das Java-Modell erreicht dies durch eine komplizierte Kausalitätsdefinition, aber wenn wir diese nicht aufnehmen wollen, können wir diese Eigenschaft einfach direkt festlegen.

Keine Sicherheitslücken durch von-der-Luft-gelesen

Wenn das Programm einen selbstlegitimierenden Wert erzeugt, könnte dies den Zugriff auf ein Objekt aufdecken, das das Programm lieber nicht sehen sollte. Auch hier behandelt das Java-Modell dies mit der Kausalitätsdefinition. Wir könnten diese Sicherheitsprobleme verhindern, indem wir spekulative Schreibvorgänge auf gemeinsam genutzte Variablen verbieten, aber ich habe keinen Beweis dafür, und Python benötigt diese Sicherheitsgarantien möglicherweise ohnehin nicht.

Beschränke Neuordnungen statt Happens-before zu definieren

Die Speichermodelle von .NET [#CLR-msdn] und x86 [#x86-model] basieren auf der Definition, welche Neuordnungen Compiler zulassen dürfen. Ich denke, es ist einfacher, mit einem Happens-before-Modell zu programmieren, als über alle möglichen Neuordnungen eines Programms nachzudenken, und es ist einfacher, genügend Happens-before-Kanten einzufügen, um ein Programm korrekt zu machen, als genügend Speicherzäune einzufügen, um dasselbe zu tun. Daher, obwohl wir einige Neuordnungsbeschränkungen auf die Happens-before-Basis legen könnten, glaube ich nicht, dass Pythons Speichermodell ausschließlich Neuordnungsbeschränkungen sein sollte.

Atomare, unsortierte Zuweisungen

Zuweisungen von primitiven Typen sind bereits atomar. Wenn Sie 3<<72 + 5 einer Variablen zuweisen, kann kein Thread nur einen Teil des Wertes sehen. Jeremy Manson schlug vor, dies auf alle Objekte auszudehnen. Dies ermöglicht es Compilern, Operationen zur Optimierung neu anzuordnen, ohne einige der verwirrenderen uninitialisierten Werte zuzulassen. Die Grundidee ist, dass beim Zuweisen einer gemeinsam genutzten Variablen Leser keine Änderungen sehen können, die am neuen Wert vor der Zuweisung vorgenommen wurden, oder am alten Wert nach der Zuweisung. Wenn wir also ein Programm wie dieses haben

Anfangs gilt (d.a, d.b) == (1, 2), und (e.c, e.d) == (3, 4). Wir haben auch class Obj(object): pass.

Thread 1	Thread 2
r1 = Obj()	r3 = d
r1.a = 3	r4, r5 = r3.a, r3.b
r1.b = 4	r6 = e
d = r1	r7, r8 = r6.c, r6.d
r2 = Obj()
r2.c = 6
r2.d = 7
e = r2

(r4, r5) kann (1, 2) oder (3, 4) sein, aber nichts anderes, und (r7, r8) kann entweder (3, 4) oder (6, 7) sein, aber nichts anderes. Im Gegensatz zu wenn Schreibvorgänge Releases und Lesevorgänge Acquires wären, ist es legal, dass Thread 2 (e.c, e.d) == (6, 7) und (d.a, d.b) == (1, 2) sieht (außerhalb der Reihenfolge).

Dies gibt dem Compiler viel Flexibilität bei der Optimierung, ohne dass Benutzer seltsame Werte sehen können. Da es jedoch von Datenabhängigkeiten abhängt, führt es zu einigen eigenen Überraschungen. Zum Beispiel könnte der Compiler das obige Beispiel frei zu

Thread 1	Thread 2
r1 = Obj()	r3 = d
r2 = Obj()	r6 = e
r1.a = 3	r4, r7 = r3.a, r6.c
r2.c = 6	r5, r8 = r3.b, r6.d
r2.d = 7
e = r2
r1.b = 4
d = r1

optimieren, solange er nicht zuließ, dass die Initialisierung von e über eine der Initialisierungen von Mitgliedern von r2 hinausging, und ähnlich für d und r1.

Dies hilft auch, die Happens-before-Konsistenz zu begründen. Um das Problem zu verstehen, stellen Sie sich vor, dass der Benutzer unsicher eine Referenz auf ein Objekt veröffentlicht, sobald er sie erhält. Das Modell muss einschränken, welche Werte über diese Referenz gelesen werden können. Java besagt, dass jedes Feld vor dem ersten Sehen des Objekts durch jemanden mit 0 initialisiert wird, aber Python hätte Schwierigkeiten, „jedes Feld“ zu definieren. Wenn wir stattdessen sagen, dass Zuweisungen an gemeinsam genutzte Variablen einen Wert sehen müssen, der mindestens so aktuell ist wie zum Zeitpunkt der Zuweisung, dann laufen wir keine Probleme mit früher Veröffentlichung.

Zwei Ebenen von Garantien

Die meisten anderen Sprachen mit Garantien für ungesperrte Variablen unterscheiden zwischen normalen Variablen und volatilen/atomaren Variablen. Sie bieten mehr Garantien für die volatilen. Python kann dies nicht einfach tun, da wir keine Variablen deklarieren. Das mag wichtig sein oder auch nicht, da Python-Sperren nicht wesentlich teurer sind als normaler Python-Code. Wenn wir diese Ebenen zurückbekommen wollen, könnten wir

1. Eine Reihe von atomaren Typen ähnlich wie Java’s [5] oder C++’s [6] einführen. Leider könnten wir ihnen mit = nicht zuweisen.
2. Ohne Variablen deklarationen zu verlangen, könnten wir auch festlegen, dass alle Felder eines bestimmten Objekts atomar sind.
3. Den Mechanismus __slots__ [7] mit einer parallelen __volatiles__-Liste und vielleicht einer __finals__-Liste erweitern.

Sequentielle Konsistenz

Wir könnten einfach die sequentielle Konsistenz für Python übernehmen. Dies vermeidet alle oben genannten Gefahren, verbietet aber auch viele Optimierungen. Soweit ich weiß, ist dies das aktuelle Modell von CPython, aber wenn CPython lernen würde, einige Variablenlesungen zu optimieren, würde es diese Eigenschaft verlieren.

Wenn wir dies übernehmen, kann Jythons dict-Implementierung möglicherweise nicht mehr ConcurrentHashMap verwenden, da diese nur verspricht, geeignete Happens-before-Kanten zu erstellen, aber keine sequentielle Konsistenz garantiert (obwohl vielleicht die Tatsache, dass Java-Volatiles total geordnet sind, übertragen wird). Sowohl Jython als auch IronPython müssten wahrscheinlich AtomicReferenceArray oder das Äquivalent für alle __slots__-Arrays verwenden.

Anpassung des x86-Modells

Das x86-Modell lautet

1. Ladungen werden nicht mit anderen Ladungen neu geordnet.
2. Speicher werden nicht mit anderen Speichern neu geordnet.
3. Speicher werden nicht mit älteren Ladungen neu geordnet.
4. Ladungen können mit älteren Speichern an verschiedenen Orten neu geordnet werden, aber nicht mit älteren Speichern an demselben Ort.
5. In einem Mehrprozessorsystem gehorcht die Speicherordnung der Kausalität (die Speicherordnung respektiert die transitive Sichtbarkeit).
6. In einem Mehrprozessorsystem haben Speicher an derselben Stelle eine Totalordnung.
7. In einem Mehrprozessorsystem haben gesperrte Anweisungen eine Totalordnung.
8. Ladungen und Speicher werden nicht mit gesperrten Anweisungen neu geordnet.

In der Acquire/Release-Terminologie scheint dies zu besagen, dass jeder Speicher ein Release und jede Ladung ein Acquire ist. Dies ist etwas schwächer als sequentielle Konsistenz, da es inkonsistente Ordnungen zulässt, aber Zombie-Werte und die sie erzeugenden Compiler-Optimierungen verbietet. Wir müssten das Modell wahrscheinlich irgendwie abschwächen, um Compilern ausdrücklich zu erlauben, redundante Variablenlesungen zu eliminieren. Das x86-Modell kann auch auf anderen Plattformen teuer zu implementieren sein, obwohl dies aufgrund der Verbreitung von x86 möglicherweise nicht viel ausmacht.

Upgrade oder Downgrade auf ein alternatives Modell

Wir können ein anfängliches Speichermodell übernehmen, ohne zukünftige Implementierungen vollständig einzuschränken. Wenn wir mit einem schwachen Modell beginnen und später stärker werden wollen, müssten wir nur die Implementierungen ändern, nicht die Programme. Einzelne Implementierungen könnten auch ein stärkeres Speichermodell garantieren, als die Sprache fordert, obwohl dies die Interoperabilität beeinträchtigen könnte. Andererseits können wir, wenn wir mit einem starken Modell beginnen und es später abschwächen wollen, eine from __future__ import weak_memory Anweisung hinzufügen, um zu deklarieren, dass einige Module sicher sind.

CPython

Verwendet den GIL, um zu garantieren, dass andere Threads keine komischen Neuordnungen sehen, und führt so wenige Optimierungen durch, dass ich glaube, dass es auf Bytecode-Ebene tatsächlich sequentiell konsistent ist. Threads können zwischen zwei beliebigen Bytecodes wechseln (statt nur zwischen Anweisungen), sodass zwei Threads, die gleichzeitig ausführen

i = i + 1

mit i anfänglich 0 könnten leicht mit i==1 enden, anstatt des erwarteten i==2. Wenn sie ausführen

i += 1

stattdessen gibt CPython 2.6 immer die richtige Antwort, aber es ist leicht vorstellbar, dass eine andere Implementierung diese Anweisung nicht atomar macht.

PyPy

Verwendet ebenfalls einen GIL, betreibt aber wahrscheinlich genug Optimierungen, um die sequentielle Konsistenz zu verletzen. Ich weiß sehr wenig über diese Implementierung.

Jython

Bietet echte Nebenläufigkeit gemäß dem Java-Speichermodell und speichert alle Objektfelder (außer denen in __slots__?) in einer ConcurrentHashMap, die ziemlich starke Ordnungsgarantien bietet. Lokale Variablen in einer Funktion haben möglicherweise weniger Garantien, die sichtbar werden könnten, wenn sie in eine Closure aufgenommen und dann an einen anderen Thread übergeben würden.

IronPython

Bietet echte Nebenläufigkeit gemäß dem CLR-Speichermodell, was es wahrscheinlich vor uninitialisierten Werten schützt. IronPython verwendet eine gesperrte Map, um Objektfelder zu speichern, und bietet mindestens so viele Garantien wie Jython.