Abschlussprojekt: ein sperrfreier Marktdaten-Fan-out mit Beweisen seiner Invarianten

Das Abschlussprojekt ist ein Fan-out: Ein Producer veröffentlicht SPY-Ticks, und mehrere Consumer lesen alle, ohne jede Sperre. Alles, was Sie gebaut haben, trifft hier zusammen. Ein Tail, den nur der Producer bewegt, ein privater Cursor pro Consumer, damit niemand konkurriert, eine Schreibreihenfolge, die entscheidet, was ein Leser sehen kann, und ein Explorer, der aus „es scheint zu funktionieren“ eine Aussage über jeden Schedule macht.

Der Feed ist ein Log, das nur wächst. Position p enthält tick<p>, und tail sagt, wie viele Positionen veröffentlicht sind. Nur der Producer schreibt Ticks und den Tail, auf seiner Seite gibt es also nichts zu bestreiten. Jeder Consumer besitzt einen Cursor, die nächste Position, die er liest, und niemand sonst schreibt ihn. Das ist der ganze Trick eines Fan-outs: Die Consumer schreiben nie etwas, was die anderen lesen, ein weiterer Consumer kostet die anderen also nichts. Die einzige geteilte Tatsache ist der Tail, und die einzige Frage ist, in welcher Reihenfolge der Producer den Tick schreibt und den Tail bewegt. Bewegt er ihn nach den Daten, findet ein Leser, der den neuen Tail sieht, die Daten. Bewegt er ihn davor, kann ein Leser eine noch nicht geschriebene Position sehen.

def publish(shared, tick, safe=True):    if safe:        yield        pos = shared["tail"]        shared["tick%d" % pos] = tick        shared["put%d" % pos] = tick        yield        shared["tail"] = pos + 1    else:        yield        pos = shared["tail"]        shared["tail"] = pos + 1        yield        shared["tick%d" % pos] = tick        shared["put%d" % pos] = tickfor safe in (True, False):    shared, _ = run_prefix(lambda sh: [publish(sh, 9369, safe)], [0], make_feed(1))    print("safe  " if safe else "unsafe", "after one turn:", {k: v for k, v in shared.items() if k in ("tail", "tick0")})

safe   after one turn: {'tail': 0, 'tick0': 9369}
unsafe after one turn: {'tail': 1}

Ein Poll braucht zwei Züge. Der erste liest den Tail. Der zweite liest den eigenen Cursor des Consumers und, liegt der Cursor hinter dem Tail, den Tick, rückt den Cursor vor und notiert, was er bekam. An der Position kann sich nichts ändern, denn nur dieser Consumer schreibt seinen Cursor. Schiefgehen kann der Inhalt des Ticks: Ein Leser, der nach der Bewegung des Tails, aber vor dem Eintreffen der Daten kommt, liest nichts. Der Poll notiert das als None, damit der Prüfer es sieht.

def poll(shared, c):    yield    tail = shared["tail"]    yield    pos = shared["cur%d" % c]    if pos >= tail:        return None    value = shared.get("tick%d" % pos)    shared["cur%d" % c] = pos + 1    shared["got%d_%d" % (c, pos)] = value    return valueready = dict(make_feed(1), tail=1)shared, alive = run_prefix(lambda sh: [poll(sh, 0)], [0, 0], ready)print("tail is 1 but tick0 was never written:", {k: v for k, v in shared.items() if k.startswith(("cur", "got"))})

tail is 1 but tick0 was never written: {'cur0': 1, 'got0_0': None}

Was heißt „korrekt“ für den Feed? Drei Aussagen über den Endzustand. Torn: Jeder von einem Consumer empfangene Tick ist gleich dem an dieser Position abgelegten (ein fehlender, als None empfangener Tick ist torn). Gap: Jeder Consumer empfing die Positionen 0, 1, 2, ... ohne Loch. Overrun: Kein Cursor liegt hinter dem Tail. verify erkundet jeden Schedule eines Producers und der Consumer und zählt, welche jede davon brechen. Der Explorer ist der Beweis: Er kann nicht den einen glücklichen Lauf stichprobenartig nehmen, er besucht alle.

def violations(final):    puts = {int(key[3:]): value for key, value in final.items() if key.startswith("put")}    gots = {}    for key, value in final.items():        if key.startswith("got"):            c, p = key[3:].split("_")            gots[(int(c), int(p))] = value    broken = []    if any(value != puts.get(p) for (c, p), value in gots.items()):        broken.append("torn")    for c in {c for c, _ in gots}:        if sorted(p for cc, p in gots if cc == c) != list(range(sum(1 for cc, _ in gots if cc == c))):            broken.append("gap")            break    if any(key.startswith("cur") and value > final["tail"] for key, value in final.items()):        broken.append("overrun")    return sorted(broken)def verify(ticks, polls, safe=True):    outcomes = explore_all(feed_threads(ticks, polls, safe), make_feed(len(polls)))    broken = {}    delivered = 0    for key, count in outcomes.items():        final = dict(key)        delivered = max(delivered, sum(1 for k in final if k.startswith("got")))        for name in violations(final):            broken[name] = broken.get(name, 0) + count    return {"schedules": sum(outcomes.values()), "broken": dict(sorted(broken.items())), "delivered": delivered}ticks = [9369, 9305]print("safe  ", verify(ticks, (2, 1), True))print("unsafe", verify(ticks, (2, 1), False))

safe   {'schedules': 3150, 'broken': {}, 'delivered': 3}
unsafe {'schedules': 3150, 'broken': {'torn': 869}, 'delivered': 3}

Dasselbe Programm, 3.150 Schedules, und eine einzige Vertauschung zweier Zeilen macht aus „keiner gebrochen“ 869 gebrochene. Die meisten sind Schedules, die ein paar tausend Testläufe fast nie träfen. Das ist das Argument fürs Erkunden statt Testen und die ganze Fertigkeit in einer Tabelle: ein Modell, klein genug zum Aufzählen, ein Prüfer für die Invarianten und ein Urteil über jeden Schedule.

Das Labor folgt der Lektion: der leere Feed, der Producer in seinen zwei Reihenfolgen, der Poll des Consumers, der Prüfer der drei Invarianten, der Verifizierer, der alle Schedules erkundet, eine Wiedergabe eines ruhigen Laufs, in dem jeder Consumer die Ticks der Reihe nach empfängt, und die Studie an SPY-Schlusskursen.

• Funktion · FrageBaut auf
• make_feed(consumers)Was ist geteilt?Einfache Arithmetik
• publish(shared, tick, safe)Daten zuerst oder Tail zuerstEinfache Arithmetik
• poll(shared, c)Der nächste Tick für Consumer cEinfache Arithmetik
• violations(final)Welche Invarianten brachen?Einfache Arithmetik
• verify(ticks, polls, safe)Ist der Feed unter allen Schedules korrekt?explore_allviolations
• drain(ticks, polls)Was empfängt jeder Consumer?run_prefix
• study(bars)Sicher, unsicher und ruhig an SPYverifydrain

Damit ist die sperrfreie Fertigkeit abgeschlossen. Sie können jetzt die Bausteine bauen (Atomics, Compare-and-swap, Stacks und Queues), die Gefahren benennen (Races, ABA, Freigabe) und vor allem einen Entwurf gegen jeden Schedule prüfen, statt einem zufällig bestandenen Lauf zu trauen. Der nächste Schritt ist dieselbe Disziplin auf echter Hardware, in den C++-Atomics-Themen.