Das Speichermodell: Acquire und Release

Ein Prozessor darf zwei unabhängige Lese- und Schreibzugriffe in beliebiger Reihenfolge ausführen, und ein anderer Kern kann das Ergebnis dieser Wahl sehen. Veröffentlichen Sie einen SPY-Preis und setzen Sie dann ein Flag: Ein Leser, der das Flag sieht, kann trotzdem einen Preis von 0 lesen. Von den vier Möglichkeiten, Schreiber und Leser zu ordnen, ist nur eine sicher: Release beim Schreiber gepaart mit Acquire beim Leser.

Store-Puffer, Caches und der Compiler lassen einen Kern einen späteren Schreib- oder Lesezugriff vor einem früheren beenden, solange ein einzelner Thread es nicht merkt. Ein anderer Thread merkt es. Unsere Maschine modelliert das direkt: Ein Thread ist eine Liste von Operationen und darf jede Operation in beliebiger Reihenfolge ausführen, deren Ordnungsbedingungen erfüllt sind. Operationen auf derselben Adresse behalten immer ihre Reihenfolge, sonst würde ein Thread seine eigenen Schreibzugriffe nicht sehen. Ein Acquire-Load blockiert alles danach; ein Release-Store wartet auf alles davor. Zwei Funktionen sagen alles: must_wait listet auf, worauf eine Operation wartet, und eligible listet auf, was als Nächstes laufen darf.

def must_wait(ops, j):    waits = []    for i in range(j):        same = ops[i][1] == ops[j][1]        after_acquire = ops[i][0] == "load" and ops[i][3] == "acquire"        release = ops[j][0] == "store" and ops[j][3] == "release"        if same or after_acquire or release:            waits.append(i)    return waitsdef eligible(ops, done):    return [j for j in range(len(ops)) if j not in done and all(i in done for i in must_wait(ops, j))]writer = [("store", "data", 1, "relaxed"), ("store", "flag", 1, "release")]reader = [("load", "flag", "r1", "acquire"), ("load", "data", "r2", "relaxed")]print(must_wait(writer, 1), eligible(writer, set()), eligible(writer, {0}))print(must_wait(reader, 1), eligible(reader, set()))print(eligible([("load", "flag", "r1", "relaxed"), ("load", "data", "r2", "relaxed")], set()))

[0] [0] [1]
[0] [0]
[0, 1]

Der Release-Store des Flags wartet auf Position 0, den Daten-Store, der Schreiber kann seine Operationen also nur der Reihe nach ausführen. Der Acquire-Load des Flags blockiert den dahinter liegenden Daten-Load, der Leser läuft also ebenfalls der Reihe nach. Bei einfachen Loads sind beide gleichzeitig zulässig, und der Leser darf die Daten zuerst lesen.

outcomes ist der Explorer der letzten Themen für diese neue Maschine. Ein Zustand ist, welche Operationen jeder Thread erledigt hat, der Speicher und die Register. Von einem Zustand aus probiert er jede zulässige Operation jedes Threads, und wenn nichts mehr zu laufen ist, sind die Register ein Ergebnis. Weil viele Reihenfolgen denselben Zustand erreichen, merkt er sich bereits gesehene Zustände. Der Message-Passing-Test veröffentlicht mit zwei Stores, erst den Daten, dann dem Flag, und konsumiert mit zwei Loads, erst dem Flag, dann den Daten. Der Konsument liegt falsch, wenn er r1 == 1 (das Flag) und r2 == 0 (noch keine Daten) sieht, was reads_stale prüft.

def outcomes(programs, memory=None):    found = set()    seen = set()    def visit(done, mem, regs):        state = (tuple(frozenset(d) for d in done), tuple(sorted(mem.items())), tuple(sorted(regs.items())))        if state in seen:            return        seen.add(state)        moved = False        for tid, ops in enumerate(programs):            for j in eligible(ops, done[tid]):                moved = True                kind, address, x, _ = ops[j]                mem2, regs2 = dict(mem), dict(regs)                if kind == "store":                    mem2[address] = x                else:                    regs2[x] = mem.get(address, 0)                done2 = [set(d) for d in done]                done2[tid].add(j)                visit(done2, mem2, regs2)        if not moved:            found.add(tuple(sorted(regs.items())))    visit([set() for _ in programs], dict(memory or {}), {})    return founddef mp_programs(write_order, read_order):    return [        [("store", "data", 1, "relaxed"), ("store", "flag", 1, write_order)],        [("load", "flag", "r1", read_order), ("load", "data", "r2", "relaxed")],    ]def reads_stale(results):    return any(dict(outcome).get("r1") == 1 and dict(outcome).get("r2") == 0 for outcome in results)for pair in (("relaxed", "relaxed"), ("release", "acquire")):    results = outcomes(mp_programs(*pair))    print(pair, sorted(results), "stale:", reads_stale(results))

('relaxed', 'relaxed') [(('r1', 0), ('r2', 0)), (('r1', 0), ('r2', 1)), (('r1', 1), ('r2', 0)), (('r1', 1), ('r2', 1))] stale: True
('release', 'acquire') [(('r1', 0), ('r2', 0)), (('r1', 0), ('r2', 1)), (('r1', 1), ('r2', 1))] stale: False

Bei Relaxed-Ordnung kann der Konsument mit allen vier Paaren (r1, r2) enden, auch (1, 0), dem veralteten. Mit Release auf dem Flag-Store und Acquire auf dem Flag-Load bleiben nur drei: Der Leser, der das Flag sieht, sieht auch die Daten, weil keine Seite über das Flag hinweg umgeordnet werden kann.

Reicht eine Seite? Probieren Sie alle vier Paare. Release allein beim Schreiber scheitert: Der Leser kann die Daten vor dem Flag laden. Acquire allein beim Leser scheitert: Der Schreiber kann das Flag vor den Daten speichern. Nur das Paar funktioniert, wie die Tabelle unten zeigt. Das ist der Release-Acquire-Vertrag von C++ std::atomic und Rust, und der Grund, warum eine sperrfreie Warteschlange einen Slot mit einem Release-Store eines Index veröffentlicht und mit einem Acquire-Load liest.

PAIRS = [("relaxed", "relaxed"), ("release", "relaxed"), ("relaxed", "acquire"), ("release", "acquire")]def ordering_table():    return {pair: reads_stale(outcomes(mp_programs(*pair))) for pair in PAIRS}for pair, stale in ordering_table().items():    print("write", pair[0], "| read", pair[1], "->", "can read stale data" if stale else "safe")

write relaxed | read relaxed -> can read stale data
write release | read relaxed -> can read stale data
write relaxed | read acquire -> can read stale data
write release | read acquire -> safe

price = int(round(float(load_bars()["close"].iloc[0]) * 100))programs = mp_programs("release", "acquire")programs[0][0] = ("store", "data", price, "relaxed")print(price, sorted(outcomes(programs)))

9369 [(('r1', 0), ('r2', 0)), (('r1', 0), ('r2', 9369)), (('r1', 1), ('r2', 9369))]

Mit dem ersten SPY-Schlusskurs, 9.369 Cent, kann der Leser in drei der vier Konfigurationen das Flag und einen Preis von 0 sehen. Ein solcher Fehler besteht alle Tests auf einer Maschine, die zufällig die Ordnung hält, und tritt auf einer anderen auf. Darum muss das sichere Paar über alle erlaubten Reihenfolgen bewiesen werden, wie es der Explorer tut.

Das Labor folgt der Lektion: worauf eine Operation warten muss, welche Operationen als Nächstes laufen dürfen, alle Ergebnisse einer Menge von Threads, der Message-Passing-Test, die Prüfung auf veraltete Daten, die Tabelle der vier Ordnungen und die Studie, die einen echten SPY-Preis veröffentlicht.

• Funktion · FrageBaut auf
• must_wait(ops, j)Worauf muss diese Operation warten?Einfache Arithmetik
• eligible(ops, done)Welche Operationen dürfen als Nächstes laufen?Einfache Arithmetik
• outcomes(programs, memory)Womit können die Threads enden?eligible
• mp_programs(write_order, read_order)Wie sieht Message Passing aus?Einfache Arithmetik
• reads_stale(results)Kann der Leser das Flag ohne die Daten sehen?Einfache Arithmetik
• ordering_table()Welche Ordnungspaare sind sicher?outcomesmp_programs
• study(bars)Welche Paare schützen einen echten SPY-Preis?outcomesmp_programs

Nächstes Thema: Sie haben jetzt die Werkzeuge, um eine sperrfreie Struktur zu bauen, und ein Vokabular, um zu beschreiben, was sie garantiert. Fortschrittsgarantien benennt die drei Stufen, obstruction-free, lock-free und wait-free, und testet jeden von Ihnen geschriebenen Zähler gegen einen Thread, der im schlimmsten Moment für immer angehalten wird.