Hazard pointers and epoch reclamation

A lock-free stack never blocks, but it cannot simply free a node it has popped: another thread may have read the head a moment ago and be about to read that node's next. Freed memory can be reused or unmapped, so that read is a use-after-free. Two classic cures exist. Hazard pointers let a thread announce the node it is using. Epochs let it announce when it entered. In both, an unlinked node is freed only when nobody can still hold it.

The model is the stack of the ABA topic. A thread reads the head, reads the node, then swaps the head in one compare-and-swap. The unsafe pop frees the node in the same turn the swap succeeds. A node freed is a node nobody may touch, and read_node records a use-after-free whenever a thread reads one. Two threads that pop once each give only 20 schedules, and the explorer finds the bad ones at once: the schedules where one thread read the head, the other popped and freed that node, and the first then reads it.

def pop_unsafe(shared, tid):    while True:        yield        idx = shared["head"]        if idx == -1:            return None        yield        nxt, value = read_node(shared, idx)        yield        if compare_and_swap(shared, "head", idx, nxt):            shared["popped"] = shared["popped"] + (value,)            free_node(shared, idx)            return valuedef two_pops(shared):    return [pop_unsafe(shared, 0), pop_unsafe(shared, 1)]outcomes = explore_all(two_pops, make_heap([9369, 9305]))hits = sum(n for key, n in outcomes.items() if dict(key)["uaf"])print(sum(outcomes.values()), "schedules,", hits, "of them read a freed node")

20 schedules, 6 of them read a freed node

A hazard pointer turns the free into a conversation. Before reading a node the thread writes its number into its slot. That alone is not enough, because the node may have been popped and freed between reading the head and writing the slot, so the thread validates: it reads the head again and starts over if it moved. After a successful pop the thread does not free the node, it puts it on its own retired list and scans: it reads every thread's slot once and frees only the retired nodes that no slot names. The nodes left on the list wait for a later scan.

def pop_hazard(shared, tid):    while True:        yield        idx = shared["head"]        if idx == -1:            shared["hp%d" % tid] = -1            return None        yield        shared["hp%d" % tid] = idx        yield        if shared["head"] != idx:            continue        yield        nxt, value = read_node(shared, idx)        yield        if compare_and_swap(shared, "head", idx, nxt):            shared["popped"] = shared["popped"] + (value,)            shared["hp%d" % tid] = -1            shared["retired%d" % tid] = shared["retired%d" % tid] + (idx,)            break    yield    hazards = tuple(shared["hp%d" % t] for t in range(shared["threads"]))    yield    keep = []    for node in shared["retired%d" % tid]:        if node in hazards:            keep.append(node)        else:            free_node(shared, node)    shared["retired%d" % tid] = tuple(keep)    return valuedef two_pops(shared):    return [pop_hazard(shared, 0), pop_hazard(shared, 1)]outcomes = explore_all(two_pops, make_heap([9369, 9305]))hits = sum(n for key, n in outcomes.items() if dict(key)["uaf"])waiting = max(sum(len(dict(key)["retired%d" % t]) for t in (0, 1)) for key in outcomes)print(sum(outcomes.values()), "schedules,", hits, "read a freed node, up to", waiting, "node waiting at the end")

12122 schedules, 0 read a freed node, up to 1 node waiting at the end

Epoch-based reclamation announces much less. There is one global epoch counter. A thread writes the current epoch into its slot when it enters an operation and writes -1 when it leaves, and it never announces individual nodes. A node retired in epoch e can only be held by a thread that entered at epoch e or before, so it is safe to free when every thread inside an operation announced an epoch greater than e. The price is that one thread that stays inside for a long time holds back every node retired after it entered, while a hazard pointer holds back only the one node it names.

def pop_epoch(shared, tid):    yield    shared["ep%d" % tid] = shared["epoch"]    while True:        yield        idx = shared["head"]        if idx == -1:            shared["ep%d" % tid] = -1            return None        yield        nxt, value = read_node(shared, idx)        yield        if compare_and_swap(shared, "head", idx, nxt):            shared["popped"] = shared["popped"] + (value,)            shared["ep%d" % tid] = -1            shared["retired%d" % tid] = shared["retired%d" % tid] + ((idx, shared["epoch"]),)            shared["epoch"] = shared["epoch"] + 1            break    announced = []    for t in range(shared["threads"]):        yield        if shared["ep%d" % t] != -1:            announced.append(shared["ep%d" % t])    yield    keep = []    for node, epoch in shared["retired%d" % tid]:        if announced and epoch >= min(announced):            keep.append((node, epoch))        else:            free_node(shared, node)    shared["retired%d" % tid] = tuple(keep)    return valuedef two_pops(shared):    return [pop_epoch(shared, 0), pop_epoch(shared, 1)]outcomes = explore_all(two_pops, make_heap([9369, 9305]))hits = sum(n for key, n in outcomes.items() if dict(key)["uaf"])waiting = max(sum(len(dict(key)["retired%d" % t]) for t in (0, 1)) for key in outcomes)print(sum(outcomes.values()), "schedules,", hits, "read a freed node, up to", waiting, "node waiting at the end")

9012 schedules, 0 read a freed node, up to 1 node waiting at the end

Safety costs schedules, because every announcement, validation and scan is another step the other thread can slip into: 20 became 12,122 and 9,012. That is exactly why the explorer is useful here. It does not need to know why the scheme is right, it checks every one of those schedules.

The lab follows the lecture: the shared state with one slot set per thread, the unsafe pop, the hazard-pointer pop, the epoch pop, the check of the two invariants (no use-after-free, nothing lost), the verifier that explores every schedule of a scheme, and the study of all three schemes on SPY closes.

• Function · questionBuilds on
• make_heap(values, threads)What is shared?Plain arithmetic
• pop_unsafe(shared, tid)Pop and free at oncePlain arithmetic
• pop_hazard(shared, tid)Announce, validate, retire, scanPlain arithmetic
• pop_epoch(shared, tid)Enter, retire with the epoch, reclaimPlain arithmetic
• violations(final)Which invariants broke?Plain arithmetic
• verify(scheme, values, pops)Is a scheme safe under every schedule?explore_allviolations
• study(bars)Which scheme survives SPY's stack?verify

Next topic: this was a stack, and a toy one. The capstone a lock-free market-data fan-out puts the whole skill to work: SPY ticks flow from one producer to several consumers through a lock-free structure, and the explorer proves its invariants over every schedule.