Capstone: a lock-free market-data fan-out with proofs of its invariants

The capstone is a fan-out: one producer publishes SPY ticks and several consumers each read all of them, with no lock anywhere. Everything you built meets here. A tail that only the producer moves, a private cursor per consumer so nobody contends, a write order that decides what a reader can see, and an explorer that turns "it seems to work" into a statement about every schedule.

The feed is a log that only grows. Position p holds tick<p>, and tail says how many positions are published. Only the producer writes ticks and the tail, so there is nothing to contend over on the producer side. Each consumer owns a cursor, the next position it will read, and nobody else writes it. That is the whole trick of a fan-out: the consumers never write anything the others read, so adding a consumer costs the others nothing. The one shared fact is the tail, and the one question is in which order the producer writes the tick and moves the tail. Move it after the data and a reader that sees the new tail finds the data. Move it before, and a reader can see a position that is not written yet.

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}

A poll takes two turns. The first reads the tail. The second reads the consumer's own cursor, and if the cursor is behind the tail it reads the tick, advances the cursor and records what it got. Nothing about the position can change under it, because only this consumer writes its cursor. What can go wrong is what the tick holds: a reader that gets in after the tail moved but before the data arrived reads nothing. The poll records that as None, so the checker can see it.

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}

What does "correct" mean for the feed? Three statements about the final state. Torn: every tick a consumer received equals the tick that was put at that position (a missing tick received as None is torn). Gap: each consumer received positions 0, 1, 2, ... with no hole. Overrun: no cursor is beyond the tail. verify explores every schedule of a producer and the consumers and counts the schedules that break each one. The explorer is the proof: it cannot sample the one lucky run, it visits them all.

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}

The same program, 3,150 schedules, and a single reordering of two lines turns "none broken" into 869 broken. Most of them are schedules that a few thousand test runs would almost never hit. That is the case for exploring instead of testing, and it is the whole skill in one table: a model small enough to enumerate, a checker for the invariants, and a verdict about every schedule.

The lab follows the lecture: the empty feed, the producer in its two orders, the consumer's poll, the checker of the three invariants, the verifier that explores every schedule, a replay of a calm run in which each consumer receives the ticks in order, and the study on SPY closes.

• Function · questionBuilds on
• make_feed(consumers)What is shared?Plain arithmetic
• publish(shared, tick, safe)Data first, or tail firstPlain arithmetic
• poll(shared, c)The next tick for consumer cPlain arithmetic
• violations(final)Which invariants broke?Plain arithmetic
• verify(ticks, polls, safe)Is the feed correct under every schedule?explore_allviolations
• drain(ticks, polls)What does each consumer receive?run_prefix
• study(bars)Safe, unsafe and calm on SPYverifydrain

That completes the lock-free skill. You can now build the pieces (atomics, compare-and-swap, stacks and queues), name the hazards (races, ABA, reclamation), and above all check a design against every schedule instead of trusting a run that happened to pass. The next step is the same discipline on real hardware, in the C++ atomics topics.