The memory model: acquire and release

A processor is free to run two independent reads and writes in either order, and another core can see the result of that choice. Publish a SPY price and then raise a flag, and a reader that sees the flag may still read a price of 0. Of the four ways to order the writer and the reader, only one is safe: release on the writer paired with acquire on the reader.

Store buffers, caches and the compiler all let a core finish a later write or read before an earlier one, as long as a single thread cannot tell. Another thread can tell. Our machine models this directly: a thread is a list of operations, and it may run any operation whose ordering constraints are met, in any order. Operations on the same address always keep their order, otherwise a thread would not see its own writes. An acquire load blocks everything after it; a release store waits for everything before it. Two functions say it all: must_wait lists what an operation waits for, and eligible lists what may run next.

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]

The release store of the flag waits for position 0, the data store, so the writer can only run its operations in order. The acquire load of the flag blocks the data load behind it, so the reader also runs in order. With plain loads, both are eligible at once and the reader may read the data first.

outcomes is the explorer of the last topics for this new machine. A state is which operations each thread has done, the memory and the registers. From a state it tries every eligible operation of every thread, and when nothing is left to run the registers are an outcome. Because many orders reach the same state, it remembers the states it has seen. The message-passing test publishes with two stores, the data and then the flag, and consumes with two loads, the flag and then the data. The consumer is wrong when it sees r1 == 1 (the flag) and r2 == 0 (no data yet), which reads_stale checks.

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

With relaxed orders the consumer can end with all four pairs (r1, r2), including (1, 0), the stale one. With release on the flag store and acquire on the flag load, only three remain: the reader that sees the flag also sees the data, because neither side can be reordered across the flag.

Is one side enough? Try all four pairs. Release on the writer alone fails: the reader may load the data before the flag. Acquire on the reader alone fails: the writer may store the flag before the data. Only the pair works, which is what the table below shows. This is the release-acquire contract of C++ std::atomic and of Rust, and the reason a lock-free queue publishes a slot with a release store of an index and reads it with an acquire load.

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))]

With the first close of SPY, 9,369 cents, the reader can see the flag and a price of 0 in three of the four configurations. A bug of this kind passes every test on a machine that happens to keep order, and shows up on another. That is why the safe pair has to be proved over every allowed order, as the explorer does.

The lab follows the lecture: what an operation must wait for, which operations may run next, every outcome of a set of threads, the message-passing test, the check for stale data, the table of the four orderings, and the study that publishes a real SPY price.

• Function · questionBuilds on
• must_wait(ops, j)What must this operation wait for?Plain arithmetic
• eligible(ops, done)Which operations may go next?Plain arithmetic
• outcomes(programs, memory)What can the threads end with?eligible
• mp_programs(write_order, read_order)What does message passing look like?Plain arithmetic
• reads_stale(results)Can the reader see the flag without the data?Plain arithmetic
• ordering_table()Which pairs of orderings are safe?outcomesmp_programs
• study(bars)Which pairs keep a real SPY price safe?outcomesmp_programs

Next topic: you now have the tools to build a lock-free structure and a vocabulary to describe what it guarantees. Progress guarantees names the three levels, obstruction-free, lock-free and wait-free, and tests each counter you wrote against a thread that is paused forever at the worst moment.