Alle Schedules auszuführen beweist ein kleines Programm, kostet aber die Zahl der Verzahnungen. Echte Werkzeuge nehmen zwei Abkürzungen. Ein Race-Detektor beobachtet einen Lauf und meldet die Variablen, die in einem anderen Schedule wettlaufen könnten. Ein Model Checker merkt sich die gesehenen Zustände. Für zwei Threads mit 10 Schritten sind das 184.756 Schedules gegen 121 Zustände.
Eine Spur und eine Frage
Ein Race-Detektor führt keine Threads aus. Er liest eine Spur: jedes Lesen und Schreiben gemeinsamer Daten und jedes Acquire und Release einer Sperre. Unsere Programme werden zu Listen solcher Operationen, und interleave macht aus einem Programm und einem Schedule die Spur dieses Laufs. Zwei Threads, die je x lesen und schreiben und keine Sperre nutzen, ergeben die vier Ereignisse unten. In diesem Schedule endet Thread 0, bevor Thread 1 beginnt, ein Test sähe also die richtige Antwort. Die Frage des Detektors ist eine andere: Hätten sich die beiden Threads überlappen können?
def interleave(programs, schedule): position = [0] * len(programs) trace = [] for tid in schedule: kind, name = programs[tid][position[tid]] position[tid] += 1 trace.append((tid, kind, name)) return traceunlocked = [[("read", "x"), ("write", "x")], [("read", "x"), ("write", "x")]]trace = interleave(unlocked, [0, 0, 1, 1])print(trace)
[(0, 'read', 'x'), (0, 'write', 'x'), (1, 'read', 'x'), (1, 'write', 'x')]
Lockset: Welche Sperre schützt diese Variable?
Der erste Detektor nutzt eine Disziplin: Jede gemeinsame Variable sollte durch eine Sperre geschützt sein, die bei jedem Zugriff gehalten wird. Die Lockset-Regel verfolgt die Sperren jedes Threads und schneidet für jede Variable die bei ihren Zugriffen gehaltenen Sperrmengen. Haben mindestens zwei Threads die Variable berührt, einer sie geschrieben und ist der Schnitt leer, schützt sie keine einzelne Sperre: Man meldet ein mögliches Race. Der Zähler ohne Sperre wird markiert, der mit Sperre nicht. Die Regel ist billig und kann Fehlalarm geben. In der Übergabe unten schreibt Thread 0 x und reicht es dann über die Sperre an Thread 1 weiter. Beim Schreiben wurde keine Sperre gehalten, also beschwert sich die Regel, obwohl die Zugriffe tatsächlich geordnet sind.
def lockset_races(trace): held = {} accesses = {} for tid, kind, name in trace: locks = held.setdefault(tid, set()) if kind == "acquire": locks.add(name) elif kind == "release": locks.discard(name) else: accesses.setdefault(name, []).append((tid, kind == "write", frozenset(locks))) racy = [] for name, history in accesses.items(): threads = {tid for tid, _, _ in history} writes = any(is_write for _, is_write, _ in history) common = frozenset.intersection(*(locks for _, _, locks in history)) if len(threads) >= 2 and writes and not common: racy.append(name) return sorted(racy)locked = [[("acquire", "m"), ("read", "x"), ("write", "x"), ("release", "m")]] * 2guarded = interleave(locked, [0, 0, 0, 0, 1, 1, 1, 1])handoff = [(0, "write", "x"), (0, "acquire", "m"), (0, "release", "m"), (1, "acquire", "m"), (1, "release", "m"), (1, "read", "x")]print("unlocked:", lockset_races(trace))print("locked: ", lockset_races(guarded))print("handoff: ", lockset_races(handoff))
unlocked: ['x'] locked: [] handoff: ['x']
Eine Variable melden, wenn zwei Threads darauf zugreifen, einer schreibt und bei allen Zugriffen keine gemeinsame Sperre gehalten wird. Sie findet fehlende Sperrdisziplin aus einem Lauf, mit Fehlalarmen, wo die Ordnung von etwas anderem als einer gemeinsamen Sperre kommt.
Happens-before: Was sich wirklich überlappen könnte
Der zweite Detektor stellt die genaue Frage: Gibt es eine Kette von Ordnungen vom ersten zum zweiten Zugriff? Es gibt zwei Arten von Kanten, die Ordnung innerhalb eines Threads und das Paar Release dann Acquire derselben Sperre. Die Happens-before-Relation ist der Abschluss beider. Eine Vektoruhr pro Thread hält fest, was der Thread gesehen hat; ein Release legt die Uhr in der Sperre ab, ein Acquire nimmt das komponentenweise Maximum mit ihr. Ein Zugriff ist ein Race, wenn ein früherer konfligierender Zugriff eines anderen Threads eine Epoche hat, die die aktuelle Uhr nicht gesehen hat. Bei der Übergabe verbinden Release und Acquire das Schreiben mit dem Lesen, also kein Race. Er meldet nur echte Races, aber nur in den Zugriffen, die er beobachtet hat.
def hb_races(trace): clocks = {} lock_clocks = {} history = {} racy = set() for tid, kind, name in trace: clock = clocks.setdefault(tid, {tid: 1}) if kind == "acquire": for u, value in lock_clocks.get(name, {}).items(): clock[u] = max(clock.get(u, 0), value) elif kind == "release": lock_clocks[name] = dict(clock) clock[tid] += 1 else: is_write = kind == "write" for u, was_write, epoch in history.get(name, []): if u != tid and (is_write or was_write) and clock.get(u, 0) < epoch: racy.add(name) history.setdefault(name, []).append((tid, is_write, clock[tid])) return sorted(racy)print("unlocked:", hb_races(trace))print("locked: ", hb_races(guarded))print("handoff: ", hb_races(handoff))
unlocked: ['x'] locked: [] handoff: []
Echte Werkzeuge wie ThreadSanitizer nutzen Happens-before, weil es auf der gesehenen Spur keinen Fehlalarm gibt. Die Lockset-Regel ist der billigere Weg, eine Variable zu finden, die nie jemand schützt, und eine gute erste Prüfung. Keine ersetzt einen Model Checker für eine sperrfreie Struktur, deren Korrektheit überhaupt nicht von Sperren kommt.
Wie groß ist der Raum?
Ein Model Checker besucht dasselbe Programm, merkt sich aber Zustände. In unseren Programmen ist ein Zustand nur, wie weit jeder Thread ist, bei Threads mit n Schritten gibt es also (n1 + 1) × (n2 + 1) × ... Zustände, wie viele Schedules auch zu ihnen führen. Die Zähl-Threads unten geben die Zahlen für die echten Daten, mit Schedules und Zuständen nebeneinander.
def count_states(lengths): total = 1 for n in lengths: total *= n + 1 return totaldef counter_programs(ups, locked): programs = [] for count in ups: program = [] for _ in range(count): program += ([("acquire", "m")] if locked else []) + [("read", "x"), ("write", "x")] + ([("release", "m")] if locked else []) programs.append(program) return programsreturns = [float(r) for r in load_bars()["close"].pct_change().dropna()][:6]ups = [sum(1 for r in returns[start::2] if r > 0) for start in (0, 1)]for name, lock in (("unlocked", False), ("locked", True)): programs = counter_programs(ups, lock) lengths = [len(p) for p in programs] trace = interleave(programs, serial_schedule(lengths)) print(name, len(trace), "events", lockset_races(trace), hb_races(trace), count_schedules(lengths), "schedules,", count_states(lengths), "states")
unlocked 8 events ['x'] ['x'] 28 schedules, 21 states locked 16 events [] [] 1820 schedules, 65 states
Eine einzige serielle Spur genügt beiden Detektoren, um die fehlende Sperre zu finden, und das Programm mit Sperre ist sauber. Der Vorteil des Model Checkers gegenüber Brute Force ist der Faktor zwischen 1.820 und 65, und er wächst unbegrenzt: Bei 10 und 10 Schritten sind es 184.756 gegen 121. Darum kann Model Checking Programme abdecken, die einfache Aufzählung nie erreichen würde, während ein Race-Detektor einen Durchgang über einen Lauf kostet.
Einen Zustand beim ersten Erreichen merken und nie zweimal expandieren. Viele Schedules erreichen denselben Zustand, die Kosten sinken also von der Zahl der Schedules auf die Zahl der Zustände.
Was Sie bauen werden
Das Labor folgt der Lektion: die Spur eines Laufs, die Lockset-Regel, die Happens-before-Regel mit Vektoruhren, die Zustandszählung, die Programme der Zähl-Threads und die Studie beider Detektoren und beider Raumgrößen an den SPY-Aufwärtstagen.
- Funktion · FrageBaut auf
- interleave(programs, schedule)Was geschah in welcher Reihenfolge?Einfache Arithmetik
- lockset_races(trace)Welche Variablen haben keine gemeinsame Sperre?Einfache Arithmetik
- hb_races(trace)Welche Variablen haben ungeordnete Zugriffe?Einfache Arithmetik
- count_states(lengths)Wie viele Zustände muss man sich merken?Einfache Arithmetik
- counter_programs(ups, locked)Was tun die Zähl-Threads?Einfache Arithmetik
- study(bars)Sind sich die Detektoren bei SPY einig?counter_programsinterleavelockset_raceshb_racescount_states
Nächstes Thema: Sperrfreier Code hat noch eine Gefahr, die kein Detektor und kein Checker nachträglich beheben kann: Ein Thread gibt einen Knoten frei, den ein anderer noch liest. Hazard Pointers und Epochen-Freigabe bauen die zwei klassischen Wege, Speicher sicher freizugeben, und der Explorer zeigt unter jedem Schedule, den Sie nicht verhindert haben, einen Use-after-free.
Lab: Was bewertet wird
6 Aufgaben · 100 Pkt.- Die Spur eines Laufs10 Pkt.
- Die Lockset-Regel25 Pkt.
- Happens-before mit Vektoruhren30 Pkt.
- Die Zustände eines Model Checkers5 Pkt.
- Die Zähl-Threads5 Pkt.
- Die Studie mit der SPY-Tabelle25 Pkt.