A single-producer single-consumer ring buffer

The simplest lock-free queue needs no compare-and-swap at all. Give each position one writer: the producer alone writes the tail, the consumer alone writes the head. A stale read of the other side's position is always safe, so a ring buffer can pass ticks between two threads without a lock. The explorer proves it over 291 schedules, and shows it breaking in 458 of 1,072 once a second producer joins.

A ring buffer keeps two counters that only grow. The producer writes slot tail % capacity and then publishes by raising tail; the consumer reads slot head % capacity and then frees it by raising head. The ring is full when tail - head == capacity and empty when head == tail. Why is it safe without a lock? The producer is the only writer of tail, so it can keep its own copy in a local variable. It reads head to look for room, and if that value is stale the stale head is smaller than the real one, so the producer thinks the ring is fuller than it is and at worst drops an item, never overwrites an unread slot. The consumer's stale tail is smaller too, so it at worst sees the ring empty. This is the single-writer principle.

def initial_state():    return {"head": 0, "tail": 0, "pushed": (), "popped": ()}def ring_producer(items, capacity):    def thread(shared):        tail = 0        for item in items:            yield            head = shared.get("head", 0)            if tail - head < capacity:                yield                shared["slot%d" % (tail % capacity)] = item                yield                tail += 1                shared["tail"] = tail                shared["pushed"] = shared.get("pushed", ()) + (item,)    return threaddef ring_consumer(attempts, capacity):    def thread(shared):        head = 0        for _ in range(attempts):            yield            tail = shared.get("tail", 0)            if head != tail:                yield                item = shared.get("slot%d" % (head % capacity))                yield                head += 1                shared["head"] = head                shared["popped"] = shared.get("popped", ()) + (item,)    return threadtwo = lambda shared: [ring_producer((7, 8), 2)(shared), ring_consumer(2, 2)(shared)]for prefix in ([0, 0, 0], [0, 0, 0, 1, 1, 1], [0, 0, 0, 0, 0, 0, 1, 1, 1, 1]):    print(prefix, run_prefix(two, prefix, initial_state())[0])

[0, 0, 0] {'head': 0, 'tail': 1, 'pushed': (7,), 'popped': (), 'slot0': 7}
[0, 0, 0, 1, 1, 1] {'head': 1, 'tail': 1, 'pushed': (7,), 'popped': (7,), 'slot0': 7}
[0, 0, 0, 0, 0, 0, 1, 1, 1, 1] {'head': 1, 'tail': 2, 'pushed': (7, 8), 'popped': (7,), 'slot0': 7, 'slot1': 8}

Three turns of the producer push the first tick: it reads the head, stores the item in slot0, and publishes tail: 1. After three turns of the consumer, head: 1 and popped: (7,). In the last line the producer has pushed both items (slot0: 7, slot1: 8) and the consumer has taken the first one; thread 1 is still alive because it has one more attempt.

What must a queue promise? Two things. The items popped are the items pushed, in the same order and without gaps: popped is a prefix of pushed (the FIFO property). And nothing is popped that was never pushed: len(popped) <= len(pushed). The threads log what they push and pop in the very turn that finishes the operation, so violations can check both on any final state. verify then runs the whole program under every schedule with explore_all and counts the schedules that break each invariant. An empty broken dictionary over all schedules is a proof, for that size of program.

def violations(final):    pushed, popped = tuple(final.get("pushed", ())), tuple(final.get("popped", ()))    broken = []    if popped != pushed[: len(popped)]:        broken.append("order")    if len(popped) > len(pushed):        broken.append("count")    return sorted(broken)def verify(producers, attempts, capacity):    def make_threads(shared):        return [ring_producer(items, capacity)(shared) for items in producers] + [ring_consumer(attempts, capacity)(shared)]    outcomes = explore_all(make_threads, initial_state())    broken = {}    pushed = popped = 0    for key, count in outcomes.items():        final = dict(key)        pushed = max(pushed, len(final.get("pushed", ())))        popped = max(popped, len(final.get("popped", ())))        for name in violations(final):            broken[name] = broken.get(name, 0) + count    return {"schedules": sum(outcomes.values()), "broken": dict(sorted(broken.items())), "pushed": pushed, "popped": popped}print(violations({"pushed": (7, 8), "popped": (8,)}))print(verify([(7, 8)], 2, 2))print(verify([(7, 8)], 2, 1))

['order']
{'schedules': 101, 'broken': {}, 'pushed': 2, 'popped': 2}
{'schedules': 25, 'broken': {}, 'pushed': 2, 'popped': 2}

A producer with two items into a ring of two slots, read by a consumer with two attempts, has 101 schedules and none of them breaks an invariant. With a ring of a single slot the producer has to drop an item when the consumer is slow, but it is still correct: 25 schedules, no violation. The popped list (8,) after (7, 8) was pushed is, as expected, a violation of the order.

The safety argument leans on one fact: tail has one writer. Add a second producer and two threads each keep their own idea of the tail. Both read the same head, both compute the same slot, and the second write overwrites the first. The explorer finds it: 458 of the 1,072 schedules of two producers (one tick each) end with a popped that is not a prefix of pushed. The fix is not a patch to this ring but another structure, a multi-producer queue, which later topics build with compare-and-swap.

print(verify([(7,), (8,)], 2, 2))

{'schedules': 1072, 'broken': {'order': 458}, 'pushed': 2, 'popped': 1}

ticks = [int(round(float(c) * 100)) for c in load_bars()["close"].iloc[:4]]print(ticks)print("one producer: ", verify([ticks[:2]], 3, 2))print("two producers:", verify([ticks[:1], ticks[1:2]], 2, 2))

[9369, 9305, 9354, 9349]
one producer:  {'schedules': 291, 'broken': {}, 'pushed': 2, 'popped': 2}
two producers: {'schedules': 1072, 'broken': {'order': 458}, 'pushed': 2, 'popped': 1}

That is the whole lesson in two numbers: one writer per position is enough for correctness on 291 schedules, and two writers on the same position are wrong on 43% of 1,072. The explorer did not guess; it ran every interleaving.

The lab follows the lecture: the empty ring, the producer and the consumer threads, the check of the two invariants, the verifier that runs the explorer, and the study that sends SPY closes through the ring with one and with two producers.

• Function · questionBuilds on
• initial_state()What does an empty ring look like?Plain arithmetic
• ring_producer(items, capacity)How does the producer push?Plain arithmetic
• ring_consumer(attempts, capacity)How does the consumer pop?Plain arithmetic
• violations(final)Which invariants does this state break?Plain arithmetic
• verify(producers, attempts, capacity)Is the ring right under every schedule?explore_allviolations
• study(bars)What breaks with a second producer?verify

Next topic: the single-writer trick has a limit, and so does compare-and-swap. The ABA problem and tagged pointers builds a lock-free stack on compare-and-swap, shows a schedule in which the swap succeeds although the stack has changed underneath it, and repairs it with a version tag.