shm_gen_cache: algorithm invariants and proofs

This document states and proves the concurrency invariants of shm_gen_cache, the lock-free shared-memory generational cache, at shared layout version 12 (LAYOUT_VERSION, lib.rs:89).

Two artefacts back the claims made here:

• This document: pen-and-paper proofs against the source.
• verification: GenMC model-checks the production code itself, under RC11, on small configurations (section 15).

A Lean 4 model of these events, in lean_model, machine-checks most of the proofs.

File and line references (store.rs:264) are to src/ and link to it at commit 920285f3b6.

Contents

1. Scope
2. Model and notation
3. The algorithm (overview, terms)
4. Shared words and events
5. Assumptions and code facts
6. Invariants overview
7. Informal proof outline
8. Proofs: slots and ownership (SL1, OW1, OW2)
9. Proofs: epochs and seals (EP1-EP4)
10. Proofs: pins and quiescence (PN1-PN3, QU1, QU2)
11. Proofs: record space (SP1-SP5)
12. Proofs: index and hits (IX1, HT1-HT3)
13. Proofs: bounds, robustness and recency (BD1, BD2, RB1-RB5, RD1, RD2, FR1-FR5)
14. Orderings audit
15. GenMC cross-reference
16. Gaps and risks

1. Scope

Not covered:

• The C API (ffi.rs), except as the place that enforces A2.
• The benchmarks, and the configuration arithmetic beyond A5.
• The liveness backends (linux_pid.rs, windows_pid.rs). Their contract is assumed: A3 for safety, A9 for robustness.
• wait.rs and futex wake-up delivery. Its loads only decide whether to sleep; they are liveness, outside the safety model.
• The staging writes of test_access::stage_interrupted_reap (test_access.rs:188-210): test-only, not modelled.
• The six GetPid test hooks (reservation_epoch_hook, reservation_retry_hook, after_epoch_publication, after_arena_reset, after_record_publication, promotion_hook; pid.rs:30-58). They are called only under feature verify, default to empty functions and make no shared-memory access of their own; promotion_hook tells a GenMC program which way a lookup came to promote (section 15).
• PromotionSampler (cache/promotion.rs:13-38), which decides whether a lookup rechecks readiness. Every proof quantifies over both of its answers; it affects hit rate and liveness only.

Guarantees

• G1, hit integrity and provenance. A lookup hit returns exactly the value one store attempt wrote for that key, never a torn, mixed or recycled value. Every published key/value pair was passed together to some insert(). (HT2, HT3.)
• G2, memory safety. Every shared load and store addresses a word inside the mapping, whatever earlier loads returned. (BD1, BD2, SP4.)
• G3, no write into a reused incarnation; serial rotation. An arena is reset for its next incarnation only after every store attempt of the previous one has finished, or has been reaped. Rotations behave as if they ran one at a time, and the epoch climbs by one per publication. (QU1, QU2, OW2, EP1-EP4.)
• G4, promotions cannot resurrect a superseded insert. Let insert $I$ of key $k$ return Ok after publishing in epoch $\phi$. A lookup of $k$ whose final pass's V1 happens after that return may miss. Any hit originates in $I$ or a same-key insert later than or concurrent with $I$, never one that precedes $I$ (its return happens before $I$'s call), regardless of promotions or rotations (FR3). The supporting property is that a promotion copies the last publication of its key in the source generation (FR2). If, besides, the lookup's final pass reads epoch $\phi$ or $\phi +1$ and reads no store of incarnation $\phi +3$ or later, it does not miss: it returns a hit, InsufficientCapacity or Corrupt, never Ok(None) (FR4). (RD1, RD2, FR1-FR4.)
• G5, failed inserts are invisible. An insert() that returns an error other than Corrupt makes no I2: no index entry is a publication of any of its records. So no lookup ever returns a record written by a store attempt that descends from it, directly or as a promoted copy, in any generation. Corrupt returns are outside this guarantee. Limits: a failed insert can still have side effects: the rotations it performs or triggers, which evict the oldest generation, so an older value of the key may stop being returned; slot reaping; and record-area space consumed by bytes reserved, or written but never indexed. So a lookup after a failed insert is not guaranteed to return the previous value, only not to return the failed insert's. (FR5.)

Non-goals:

• Recency beyond G4. G4 orders by happens-before, not by real time. A lookup that does not happen after an insert may still return an older value, but its promotions cannot make a later lookup covered by G4 return a superseded insert's record. Inserts of one key that are not ordered by happens-before are not ordered against each other, and one that lands in a later generation can win. A failed insert is invisible (G5) but not undone: its rotations may evict the key's older value, so a lookup after it need not return the previous value. A lookup whose retries take it to epoch $\phi +2$ or later may miss the key (FR4).
• Liveness. Wake-ups, wait budgets and timeouts are not treated. RB5 is the only liveness-flavoured property stated. Nor is the promotion sampler: no fairness, and no eventual promotion, is assumed. Section 16 lists the known holes.

Section 6 ends with the converse: which invariants and assumptions are necessary, and what goes wrong without each.

2. Model and notation

The proofs use the C++20 memory model that Rust atomics adopt ([intro.races], [atomics.order], [atomics.fences]). Read in RC11 terms, each argument is the acyclicity of $\mathrm{hb}$ or of $\mathrm{psc}$. GenMC checks the code under RC11.

Threads are written θ, fences $f$, a particular O3 event $o_3$, and the epoch in which a returning insert published $\phi$ (G4, FR3, FR4). F1-F15 always denote code facts, never fences. $S$ is the single total order of SeqCst operations; to avoid a clash, the scan load is written $\mathrm{Sc}$ and the liveness verdict $\mathrm{vd}$. Like Z$\left(e\right)$ for the seal of $e$, Cert$\left(n\right)$ denotes any readiness certificate for $n$ (section 4.2).

The rules cited by name:

The remaining rule of [atomics.fences] (a release fence $\mathrm{sw}$ an acquire load that reads a write $\mathrm{sb}$-after it) is not used by any proof here.

A0 (memory model). Executions are RC11-consistent, with $\mathrm{hb}$ the transitive closure of $\mathrm{sb}$, $\mathrm{sw}$ and $\mathrm{asw}$. $\mathrm{mo}$ is well-founded (has no infinite descending chain), and every read reads exactly one write. SeqCst fences are ordered by an acyclic $\mathrm{psc}$. The proofs use only the C++20 release sequence, continued by RMWs only. That definition is contained in C++11's, so the proofs hold under both. With the A3 edge in $\mathrm{hb}$, the model is RC11 plus $\mathrm{asw}$, not pure RC11: without it, the steal cases of SL1 and OW1 would have no $\mathrm{hb}$ edge.

A set of actions is serial when $\mathrm{hb}$ totally orders it.

Serial-reads lemma. On a serial set of writes to one word, $\mathrm{mo}$ agrees with $\mathrm{hb}$ (COH-WW). A load that is $\mathrm{hb}$-ordered against every write to the word reads exactly the latest write that happens before it (COH-WR, COH-RW).

Chains such as O4 $\mathrm{sb}$ P3 $\mathrm{sw}$ P1 read left to right and compose into $\mathrm{hb}$.

3. The algorithm

3.1 Overview

The mapping holds a header, one cache-line slot per participant, and three arenas. Each arena has a control word $\mathrm{ctl}$, a readiness word (the last epoch certified as a promotion source), an occupancy counter (exact mode only), an index of stamp:32, ref:32 entries and a record area. Incarnation $e$ lives in arena $emod3$; while the global epoch is $e$, lookups probe incarnations $e$ and $e-1$, inserts write into $e$, and the third arena waits to be reused as $e+1$.

Registration. A thread claims a FREE slot (P1, P2) with a fresh registration id, and releases it at the end (P3). When every slot is taken, it may steal the slot of a dead participant (P0-P6). The steal asks the liveness backend for a verdict about the claim it replaces.

Insert. A pass of reserve() loads the epoch (W1), pins it (W2), fences (W3) and prechecks the arena (B0). It then cuts the record from its private chunk (H1), or reserves with a fetch_add on the bump (B1), possibly claiming a new chunk (H2). The insert then stores the payload and the header (W4, W5), publishes the index entry (I0, I2), updates the occupancy (W6) and unpins (W7). A pass that finds the arena sealed or full unpins and rotates instead.

Rotation. The rotator takes ownership of the rotation-owner word (O1, O2), rechecks the epoch (R0) and seals the current arena (R1). Right after the seal loop it runs a SeqCst fence (R1F). It then scans every pin (R3). An observation at least two epochs old enters the wait and possible slot-reaping path (R3A, reap_pinner). An observation of the epoch $e$ it has just sealed disables readiness and takes neither path. A reap triggered by an older observation may clear a pin that changed meanwhile (RD1). If the scan observed no pin of $e$, it certifies $e$ as a promotion source (R3C). It then resets the arena to be reused (R4), publishes the next epoch (R5) and releases ownership (O4).

Takeover. A rotator that finds a dead owner examines the owner's slot (reap_owner()) and, unless the owner is live, takes ownership over with a CAS (O3).

Lookup. A lookup loads the epoch (V1) and probes $e$, then $e-1$. It loads index entries (I1), fences (I1F), loads the record (D4, D5), fences again (D6) and reloads the epoch (V2), returning Retry when the probed incarnation is two or more epochs old. Before probing $e-1$ it loads that arena's readiness word (C0). Probes do not pin and write nothing, except a recheck's certificate (C4, a fetch_max made unpinned); a promotion pins and writes through store().

Promotion. Copying a hit from $e-1$ into $e$ is hazardous while a writer of $e-1$ is still in flight: an insert of $v_2$ pinned to $e-1$ may publish after a lookup has already read the older $v_1$ there and return, and the promotion would then republish $v_1$ in $e$, shadowing the completed insert for every later lookup (section 16, item 2). A certificate for $n$ says that every store attempt for $n$ has finished, and makes their writes visible to whoever reads the certificate (RD1, RD2). A probe ordered after it therefore reads the key's last publication in $n$ (FR1, FR2). The order matters: a certificate learned after the probe's loads does not order them, hence C0 precedes the first I1, and a certificate obtained later leads to a fresh probe. The mechanism: a hit in $e-1$ after a miss in $e$ is stored again, into $e$ only (only_epoch), through the same insert path, but only if $e-1$ is certified: either C0 read the certificate for $e-1$ before the probe read anything, or a sampled recheck (C1-C4) certifies it now and a fresh probe of $e-1$ (the reprobe) supplies the copy that is promoted. Otherwise the hit is returned unpromoted. The recheck neither waits nor reaps. The sampler rechecks with probability min(1, 8 / bucket_count), drawn from a per-registration SplitMix64 stream. A promotion is also dropped if the epoch moved on or the arena has no room, and when no index slot accepts it, without rotating. Once published, it triggers the same maintenance as an insert: a rotation at the occupancy target. The C API's lookup documentation (ffi.rs:496-504, and the generated shm_gen_cache.h) states the same contract, including that the reprobe's result, possibly a miss or InsufficientCapacity, replaces the hit.

3.2 Terms

Event labels are those of section 3.1; section 4.2 tabulates them.

• A claim $c$ of a slot is a successful P1 or P4; the registration it starts lasts from that CAS until its P3, a P4 stealing it, or the end of the execution. The registrant of a slot is the thread holding its current registration. Actions on behalf of $c$ are those its thread makes for it from the claim to its P3 (A2). A rotator that steals a slot in reap_pinner() briefly holds a second registration: its events from that P4 to the P3 that releases it (T2, P5, P6, H0) are on behalf of the second registration, not of the rotator's own $c$; being made by the rotator's thread between $c$'s claim and P3, they are also $\mathrm{sb}$-ordered with $c$'s actions. The register of $c$ is its P2 or P5. The ender of $c$ is the state write that ends it: its own P3, or a P4 stealing it.
• A tenure $t$ is one hold of rotation ownership, from its acquiring CAS $A_t$ (a successful O2 or O3) until its O4 or the holder's death. Actions under $t$ are those its holder makes from $A_t$ to its O4. R0$\left(t\right)$ is the value its R0 read. A publishing tenure is one that executes R5.
• Incarnation $e$ is arena $emod3$ while it serves epoch $e$. The base of incarnation $e$ is a $\mathrm{ctl}$ write that starts it: an R4 stamping $e$, or the initial value for $e=2$.
• A pass is one iteration of reserve()'s loop, from W1 to the return of a reservation or to W7. A store attempt $w$ is a pass whose B0 saw $(\mathrm{stamp}{e}_w,\mathrm{unsealed})$, extended through its record stores, I2 and W6 to its W7 (store.rs:175, or store.rs:352 for an attempt that stops). Its actions from W2 to W7 are the events of the pass from W2 on, and of the store that follows it, up to that W7 (or to the end, if the thread dies). An attempt may stop at the target check or fail at B1; if it succeeds, it writes and publishes one record.
• A chunk is the unused tail $[\mathrm{cursor},\mathrm{end})$ of a B1 claim larger than its record, kept in the slot's chunk words for later cuts in the same epoch.
• An announce is the scan's R3A, a CAS that sets the ROTATION_WAITING flag in a pin it waits on. The head of a pin write $w$ is the last non-announce write at or before $w$ in $\mathrm{mo}\left(\mathrm{pin}\right)$ (or $\mathrm{init}$): $w$ lies in its release sequence (PN1).
• An insert operation $I$ is one call of insert(), from its call to its return; its store attempts lie in between (F15). Insert $J$ precedes insert $I$ when $J$'s return happens before $I$'s call. A store attempt descends from insert $J$ if it is an attempt of $J$, or a promotion attempt whose promoted hit's I1 read an entry published by an attempt that descends from $J$. Each attempt descends from exactly one insert, its root. By induction on the attempt's epoch: an insert attempt belongs to one insert, and a promotion attempt to none (F15); a promotion attempt copies one hit (F10), whose I1 reads one entry, whose publication belongs to one attempt (F2) of the epoch before.
• A certificate for $n$ is a release fetch_max with argument $n$ on the readiness word of arena $nmod3$: the R3C of a tenure with R0 $=n$, or the C4 of a recheck whose C1 read $n+1$ (Cert$\left(n\right)$).

4. Shared words and events

4.1 Shared words

4.2 Events

Labels are those of the source comments, except C0, the readiness load in probe(), which the source does not label. The readiness labels R1F and R3C are in rotation.rs (rotate_owned()), and C1-C4 in promotion.rs (recheck_promotion_ready()). Section 4.3 gives the conventions and the renames.

Insert (store(), reserve(), publish(), table_put()):

Registration (register_participant(), claim(), release_claim()):

Steal (steal(); used by reap_dead_participant(), reap_pinner() and reap_owner()):

Ownership (acquire_rotation(), release_rotation()):

Rotation (rotate(), rotate_owned(), reap_pinner()):

Takeover: reap_owner() (rotation.rs:234-247) is a procedure, not a label. It runs steal() restricted to the owner's registration id (P0, T0, $\mathrm{vd}$, P4, T2, P5, P6, H0), then P3 of a stolen slot; O3 follows unless the outcome is Live.

Lookup (lookup(), probe(), reprobe_for_promotion(), recheck_promotion_ready()):

Initialisation ($\mathrm{init}$, notation): Cache::initialize and initialize_storage (cache/mod.rs:172-258). Magic CAS, plain header parameters, registration_counter := 1, global_epoch := 0, rotation_owner := 0, slots (FREE, UNPINNED, start time 0, H0; participant.rs:178-183), $\mathrm{ctl}$ words (arena 2: $(2,\mathrm{unsealed},0)$; the others $(0,\mathrm{sealed},0)$), promotion_ready_epoch := 0 for each arena (relaxed; cache/mod.rs:246; never reset afterwards, as R4 does not write it), exact_occupancy := 0, zero fill of index and records, global_epoch := 2 (release, cache/mod.rs:256), magic (release, cache/mod.rs:257). By A1 it is abstracted as one write per word.

Accesses omitted from the concurrency event graph. The production-assertion loads of the caller's own pin (participant.rs:212, 238; rotation.rs:76; lock.rs:150-155) and the unconditional own-pin load in UnpinOnExit::drop (lock.rs:175), and registration_id() building the owner word (participant.rs:360, via rotation.rs:280) read words that only the caller writes: they are sequential. The WordHalf::read loads of BoundedWait (wait.rs:81) only decide whether to sleep. Their addresses, and those of the own-slot loads above (the claim assertion uses the registration scan index), are nevertheless covered by BD2: the wait watches a range-loop participant pin or the header rotation-owner word, and own-slot loads use the slot retained from registration, a scan slot, or the slot decoded from a nonempty owner word when a reaper releases its temporary registration. The omitted is_free precheck also uses the registration scan slot. The initialization magic CAS reads the header word at byte 0 before the A1 abstraction. On AArch64, arm_wfet's ldxr reads the low half of a scan pin or the high half of the header rotation-owner word at byte 60 (wait.rs:1045-1057). O0 and the is_free precheck only short-cut: R0 and P1 are the accesses that decide. Besides C0, only test code reads the readiness word: the unit tests in cache/promotion.rs and test_access::promotion_ready_epoch (feature verify).

4.3 Label conventions

• One letter per operation family, numbered in program order: W (insert), B (reservation), H (chunk), I (index), D (record loads), V (lookup epoch), O (ownership), R (rotation), P (slot state), T (start time), C (promotion certificate: a probe's readiness load and the recheck). Two exceptions. The D family starts at D4: D4-D6 are the labels of the source comments, and there are no D1-D3. The I family spans two operations: I0 and I2 belong to table_put() (insert), I1 and I1F to probe() (lookup), so its numbers are not one program order.
• $0$ marks an access before the family's numbered sequence: the load that an RMW or a decision is predicated on (B0, I0, O0, P0, T0, R0; C0, on which the decision to promote is predicated), or the chunk reset (H0).
• A letter suffix marks an auxiliary access attached to a numbered event: I1F (the fence after I1), R3A (the announce inside R3), R1F (the fence after the seal loop of R1), R3C (the certificate earned by the scan R3).
• Z$\left(e\right)$ is notation, not a label; so are $\mathrm{vd}$, $\mathrm{init}$, reap_owner() and reap_pinner(); so are Cert$\left(n\right)$ and reprobe_for_promotion().

5. Assumptions and code facts

Assumptions are environmental or contractual; code facts are properties of the source, checked by reading (and, where noted, by GenMC).

No assumption covers fairness or eventual promotion. PromotionSampler::should_recheck may return anything, every proof quantifies over both answers, and the sampler is outside the model (section 1). RD1-FR4 need no new axiom either: only the rules of section 2 under A0.

Record headers need no lifetime clause: no safety proof uses their stamps (D4's stamp check is redundant with the entry stamp, A6 and V2).

6. Invariants overview

Invariants are grouped in layers; each rests only on earlier layers and on the assumptions and code facts:

SL slots -> OW ownership -> EP epochs/seals -> PN pins -> QU quiescence
         -> SP record space -> IX index -> HT hits -> BD bounds
         -> RB robustness, index shape -> RD readiness -> FR freshness

layer  invariants          rests on (besides A0-A9, F1-F15)
SL     SL1                 -
OW     OW1 OW2             SL
EP     EP1 EP2 EP3 EP4     OW
PN     PN1 PN2 PN3         SL, EP
QU     QU1 QU2             PN, EP, OW
SP     SP1 SP2 SP3 SP4 SP5 QU, PN, EP, OW, SL
IX     IX1                 -
HT     HT1 HT2 HT3         IX, SP, QU, EP
BD     BD1 BD2             IX, SP
RB     RB1-RB5             SL, OW, IX, SP, QU (RB3, RB4: needed by G4 only;
                                                RB1, RB2, RB5: no guarantee)
RD     RD1 RD2             PN, QU, EP, OW
FR     FR1-FR5             RD, HT, RB3, RB4, SP, QU

Slots and ownership.

Epochs and seals.

Pins and quiescence.

Record space.

Index, hits and bounds.

Robustness and index shape. No guarantee G1-G3 needs these; they are separated so that the safety argument visibly does not depend on them. G4 needs RB3 and RB4.

Readiness and recency. These carry G4; FR5 carries G5.

Necessity. The "Rests on" columns give sufficiency. Conversely, each of the following is necessary: dropping it admits the bad execution shown. The evidence column says where a mutant was actually built. Without such evidence, the row is an argument only. Section 14 gives the same analysis for each atomic ordering.

Not needed for G1-G3: RB1-RB5, A8, A9, I0's acquire. Of these, G4 needs RB3, RB4, A8 and I0's acquire (through RB3).

Needed by no guarantee: RB1, RB2 and RB5; the C1's acquire and C2, redundant on the reachable path (the remark after RD1); the acquire half of O2 when it reads $\mathrm{init}$; any acquire on O3; record-header stamps (D4's stamp check); W7's swap, as opposed to a store. Section 14 lists the orderings that are stronger than needed.

7. Informal proof outline

This section tells the whole story without citing rules; sections 8-13 make each step precise. There, each invariant has an Outline before its Proof; where the proof is itself one or two sentences, the two are merged as Outline and proof.

Slots behave sequentially. A slot's state word changes only by compare-and-swap, so its history is a chain: a claim, its register, then the write that ends it, and the next claim. A normal hand-over goes through a release (P3) that the next claim (P1) acquires. A steal goes through the liveness verdict: a "dead" answer orders everything the dead thread did before it, and the steal's CAS confirms that the verdict was about the claim being replaced. So everything one registration does happens before the next registration of the slot starts. Its pin and its chunk words then behave like private variables passed down a chain of owners.

Ownership is a lock, takeovers included. The rotation-owner word works as a lock: O4 releases, O2 acquires. A takeover O3 does not read the owner's release. Instead the taker learns from the owner's slot, with acquire loads, that the owner's registration is over: either it stole that registration itself after a dead verdict, or it saw a later state of the slot, which carries the release of whatever ended the owner. Either way, everything the old owner did happens before the takeover. So rotations run one after another, each starting from the epoch its predecessor published: the epoch climbs 2, 3, 4, ... and every rotation seals its arena before publishing.

Writers are seen by the rotation that reuses their arena. A writer pins its epoch, fences, and only then checks that its incarnation is unsealed. The rotation that will reuse that arena, two epochs later, fences right after its own sealing step, under ownership, and that fence comes after the seal of the writer's incarnation through the chain of ownership handoffs. Two SeqCst fences on opposite sides of the seal cannot both miss each other: either the writer saw the seal, and stops, or the rotation's scan sees the pin. The rotation then waits until the pin moves on (an unpin, a new pin, or a reaper's clear). Each of those is a release made after the writer's last write, so the reset of the arena happens after everything the writer did there. Incarnations of an arena are therefore serial, and a pinned writer never sees a later incarnation.

Within an incarnation, space is handed out once. The bump is a fetch_add that lands inside its incarnation, so successful reservations are disjoint intervals. A slot fails at most one add per incarnation, so the bump stays below 2^31. Chunks are private to their registration and are reset on every claim, so cuts are disjoint too. Each attempt writes each word of its own reservation once.

A reader that follows a publication reads that record. The index publication is a release after the record stores, and the reader fences with acquire after loading the entry. Every record word it then loads holds that attempt's store, unless the arena was reused meanwhile. In that case the reader read a store made after some writer's SeqCst fence, its acquire fence D6 synchronises with that fence, and the epoch reload V2 sees the newer epoch and makes the lookup retry. The 32-bit stamps do not alias because no entry or lookup lives for 2^32 epochs.

Every published pair comes from an insert. An insert stores the pair its caller passed. A promotion stores its caller's key and the value of a validated hit in epoch $e-1$, which, by the previous paragraph, is exactly the pair some earlier attempt of $e-1$ wrote for that key. That attempt is an insert or, again, a promotion from an even older epoch, so an induction on the epoch traces every pair back to an insert().

A promotion copies a finished generation. The rotation that seals $e$ fences right after sealing and then sees every writer still pinned to $e$: a writer whose fence came first in the SeqCst order is in the scan, and one whose fence came later sees the seal and writes nothing. If no slot is pinned to $e$, every writer of $e$ has unpinned, each unpin is a release made after all its writes, and the scan acquires it; the rotation then publishes a certificate for $e$ with a release. A lookup acquires that certificate before reading anything in $e$, or rechecks the pins itself and then reads $e$ again. Either way every write of $e$ happens before the reads that supply the promoted copy, so each index load sees the last entry of its slot, and the promotion copies the key's last publication in $e$. A copy read before the certificate was learned may be stale; it is returned but never promoted.

Promotions cannot resurrect a superseded insert. Suppose insert(k, v) returned Ok after publishing in epoch $\phi$, and a lookup's final pass starts happens-after that return. It reads an epoch $g\ge \phi$. In incarnation $\phi$, any probe reads the insert's entry in the key's slot, or a later entry for $k$ from an insert that did not come before. Later incarnations hold only inserts that did not come before, and promotions, which copy the last value of the generation before theirs. If $g=\phi$ and the lookup falls back to $\phi -1$, its probe of $\phi$ missed although the key's chain in $\phi$ happened before it; that requires reading a store of incarnation $\phi +3$ or later, and the validation of whatever the lookup then hits forces a retry. So the lookup never returns a value whose origin is an insert that came before, regardless of promotions or rotations. It may miss; no retention is assumed. If, besides, its final pass reads $\phi$ or $\phi +1$ and nothing of incarnation $\phi +3$ or later, it does not miss: it hits, or fails with InsufficientCapacity or Corrupt.

A failed insert leaves nothing to find. An insert that returns an error other than Corrupt publishes nothing: its input was too large, its reservation or rotation failed, or its record found no bucket and the rotation that should make room failed. Corrupt returns are outside this guarantee. A promotion copies a hit, and a hit is always a publication, so nothing copied from the failed insert can exist either. Its side effects remain: its rotations may evict the key's older value.

Bounds checks hold whatever was read. Every index value, however stale, encodes an offset inside the record area. The readers bound the header's length against the area before loading anything else, and derive every further address from values that passed those checks.

8. Proofs: slots and ownership

SL1. Slot serialisation

Statement. For one slot:

• (a) After $\mathrm{init}$ (FREE), $\mathrm{mo}\left(\mathrm{state}\right)$ is a sequence of claim blocks. Each claim $c$ (a P1 or P4) is followed by at most its register (P2 or P5), then by at most one write ending $c$: its own P3, or a P4 stealing $c$. A P4 may follow INITIALIZING($c$) directly.
• (b) If claim $c$ precedes claim $c^{\prime }$ in $\mathrm{mo}\left(\mathrm{state}\right)$, every action on behalf of $c$ happens before the claiming CAS of $c^{\prime }$, and hence before every action of $c^{\prime }$.
• (c) Every state write $\mathrm{mo}$-after $c$'s register is the write that ended $c$ or comes after it.

Outline. All writes after $\mathrm{init}$ are RMWs, so $\mathrm{mo}\left(\mathrm{state}\right)$ is a chain in which each write reads its predecessor; unique claim words (A4) leave room for only the shape in (a). Ownership passes either by release and acquire (P3 then P1) or through the verdict (A3), which orders a dead thread's actions before $\mathrm{vd}$, and $\mathrm{vd}$ is $\mathrm{sb}$-before P4. The start time is loaded relaxed; P4's success is what proves that it belonged to the claim being replaced. Ruling out an earlier claim's start time uses (b) for earlier claims, hence an induction on $\mathrm{mo}\left(\mathrm{state}\right)$.

Proof. By well-founded induction on the position of $c^{\prime }$ in $\mathrm{mo}\left(\mathrm{state}\right)$ (A0).

1. Shape (a). After $\mathrm{init}$ every state write is a CAS (F7 and participant.rs:201-241). A successful CAS reads its expected value and immediately follows that write (RMW). P1 expects FREE; P2 and P5 expect their own claim's INITIALIZING word; P3 expects its own REGISTERED word; P4 expects the word its P0 loaded, which is never FREE (steal() returns Free first, participant.rs:282). By A4 each value INITIALIZING($c$) and REGISTERED($c$) is written once in the slot, by $c$ and by its register. So after INITIALIZING($c$) comes $c$'s register or a P4 stealing $c$; after REGISTERED($c$) comes $c$'s P3 or a P4 stealing $c$; after FREE only a P1. A block may be the last one, so each part is "at most".
2. (c) follows from (a): the write right after $c$'s register, if any, ends $c$.
3. (b) for consecutive claims. Let $c^{\prime }$ be the next claim after $c$, and $E$ the ender of $c$.
   • $E$ is $c$'s P3, and $c^{\prime }$ a P1 reading FREE from it. By A2 every action of $c$ is $\mathrm{sb}$-before P3. P3 is a release CAS and P1 an acquire CAS that reads it: P3 $\mathrm{sw}$ P1 (REL-ACQ).
   • $E=c^{\prime }$, a P4 stealing INITIALIZING($c$). The verdict was is_live(pid_c) = Ok(false) (F7). The opening P0 read $c$ before the verdict, identifying an already existing incarnation. By A3 with $\mathrm{st}=0$, every action of $c$'s thread, which has pid_c, happens before $\mathrm{vd}sb$ P4.
   • $E=c^{\prime }$, a P4 stealing REGISTERED($c$). The verdict was is_live_since(pid_c, st), with $\mathrm{st}$ loaded at T0. We show that T0 read $c$'s own start-time store $T_c$ (T1 or T2). The register CAS reads $c$, and P0 reads that register before the verdict, so the incarnation was already observed. Then A3 applies as above (or with $\mathrm{st}=0$).
     • P0 read the write that P4 replaced (A4), which is $c$'s register $g$, a release CAS. $T_{c}sbgsw$ P0 $\mathrm{sb}$ T0, so T0 reads $T_c$ or a later store (COH-WR).
     • Not an earlier claim's store, nor $\mathrm{init}$'s. For a claim $c_0$ before $c$, the induction hypothesis gives $T_{\mathrm{c0}}hbcsb{T}_c$, so $T_{\mathrm{c0}}mo{T}_c$ (COH-WW); $\mathrm{init}$ precedes everything (A1).
     • Not a later claim's store. Every state write after $c^{\prime }$ is an RMW, so it lies in $\mathrm{rs}\left(c^{\prime }\right)$, and $c^{\prime }$ is a release. A later claim $c^{\prime \prime }$ either is a P1, an acquire reading a write in $\mathrm{rs}\left(c^{\prime }\right)$, or is a P4 whose own P0 is an acquire reading such a write. Either way $c^{\prime }sw$ an event $\mathrm{sb}$-before $T_{c\prime \prime }$, so T0 $sb{c}^{\prime }hb{T}_{c\prime \prime }$, and T0 reads a write $\mathrm{mo}$-before $T_{c\prime \prime }$ (COH-RW). The stealer's own T2 is $\mathrm{sb}$-after T0 (COH-RW again).
4. (b) in general. The claiming CAS of a claim is an action on its behalf, and every action of $c^{\prime }$ is $\mathrm{sb}$-after its claim (A2). Transitivity along the consecutive claims between $c$ and $c^{\prime }$ gives (b).

A reaper that dies between P4 and P6 leaves an ordinary claim of its own, which the next reaper steals under the same rules: the chain of claims in (a) covers it.

OW1. Takeover handoff

Statement. Let a successful O3 $o_3$ by thread θ read the acquiring CAS $A_t$ of tenure $t$, held by registration $G$. Then every action on behalf of $G$, and every action under $t$, happens before $o_3$. Consequently $t$ has no O4.

Outline. O3 is a Release CAS: the taker does not synchronise through the owner word. It synchronises through $G$'s slot instead. O1's acquire load of an owner word naming $G$ imports $G$'s register, so the steal's first acquire load P0 sees REGISTERED($G$) or a later state. Then either θ steals $G$ itself after a dead verdict, and SL1 gives the order, or it reads a later state. That later state lies in the release sequence of the write that ended $G$: $G$'s P3, after all of $G$'s actions, or a reaper's P4, after $G$'s death. Without this handoff, an O3 ordered before the owner's O4 in $\mathrm{mo}$ would let a second rotator acquire ownership; and the new owner, which builds on the dead owner's R1 and R5, would not see them.

Proof.

1. θ read the owner word value ω = (slot_G, id_G) at O1 (acquire, rotation.rs:307), and O3 expects $\omega$ (rotation.rs:336-338). O1 read some acquiring CAS $A^{\prime }$ writing $\omega$. By A4, $\omega$ names one registration, $G$; but $A^{\prime }$ may be $A_t$ or an earlier tenure of $G$ (owner-word ABA: $G$ released and reacquired), so the evidence is about $G$, not about $t$. $A^{\prime }$ is made by $G$'s thread, after $G$'s register $g$ (only a registered participant rotates: ParticipantLock is constructed after a successful P2/P5 and retains that registration until drop; its methods forward the slot and index into rotation. registration_id() reads that registration, participant.rs:359-364). $A^{\prime }$ is a release (O2 is AcqRel, O3 Release), so $gsb{A}^{\prime }sw$ O1 $\mathrm{sb}$ P0, and P0 reads $g$ or a later state (COH-WR).
2. Derive handoff evidence from the return paths (F6) and step 1:
   • Live: no O3 follows.
   • Stolen, when P0 read $g$: θ's successful P4 read the same full word. Init and P3 write zero; P1/P4 set INITIALIZING. Thus its source is a register with id_G; A4 identifies the claim and SL1 identifies its unique register $g$. This proves that P4 steals $G$. SL1(b): every action of $G$ happens before that P4, which is $\mathrm{sb}$-before $o_3$. The dead verdict also orders every action of $G$'s thread, including work for a second registration during reap_pinner(), before P4 (A3).
   • Whenever P0 read a write $w\ne g$, step 1 puts it $\mathrm{mo}$-after $g$. This includes every Free and Other return, since their guards exclude $g$'s nonzero word with id_G, and also covers Stolen and Lost when their P0 source differs from $g$. For Lost when P0 read $g$, P4 failed; a failed CAS reads a value other than its expected one, and COH-RR (P0 $\mathrm{sb}$ P4) puts that write $w$ after $g$; P4's failure ordering is acquire. Each of these cases supplies an acquire read $q$ of a write $w$ $\mathrm{mo}$-after $g$, with $qsb{o}_3$. By SL1(c), $w$ is at or after the ender $E$ of $G$. All state writes after $E$ are RMWs, so $w$ lies in $\mathrm{rs}\left(E\right)$, and $E$ is a release: $Eswq$. If $E$ is $G$'s P3, every action of $G$ is $\mathrm{sb}$-before it (A2), as is every action under $t$: the holder releases its original registration only after its tenure. If $E$ is a reaper's P4, SL1(b) orders every action of $G$ before it, and the thread-wide dead verdict orders every action under $t$ before it (A3).
3. No O4. An O4 of $t$ would be under $t$, so O4 $hb{o}_3$, hence O4 $mo{o}_3$ (COH-WW). But $o_3$ immediately follows $A_t$ (RMW), and O4 is $\mathrm{mo}$-after $A_t$ (COH-WW, $A_{t}sb$ O4): O4 would lie between them. Contradiction.

In the code the P3 case cannot precede a successful O3: rotate() installs a release guard immediately after acquiring ownership (rotation.rs:78). Its destructor runs O4 on ordinary return and unwinding before the registration can execute P3, so O4 $\mathrm{sb}$ P3, and step 3 makes O3 fail. The proof does not need this. Nor does it use any acquire on O3: the taker's edges come from O1, from reap_owner()'s acquire reads and from A3. O3's release serves the next taker's O1 (step 1 for a later takeover).

OW2. Ownership is a lock under hb

Statement.

• (a) mo(rotation_owner) is $\mathrm{init}$ followed by blocks, each an acquiring CAS (O2 or O3), optionally followed immediately by the same tenure's O4. An O2 reads $\mathrm{init}$ or the O4 closing the previous block; an O3 reads the acquiring CAS just before it.
• (b) For tenures $t$ before $t^{\prime }$ (by $\mathrm{mo}$ of their acquiring CASes), every action under $t$ happens before $A_{t\prime }$, and before every action under $t^{\prime }$.
• (c) Tenures are totally ordered.

Outline. Once we know that an O4 always sits right after its own tenure's acquiring CAS, every block looks like a lock acquisition and release. The normal handoff is O4's release read by O2's acquire; the takeover handoff is OW1. O3 needs no acquire: it reads an acquiring CAS, and OW1 supplies the order.

Proof.

1. The writes are $\mathrm{init}$ (NONE), O2 CAS(NONE -> me) (AcqRel), O3 CAS(ω -> me) (Release) and O4 store(NONE) (release), one O4 per tenure, $\mathrm{sb}$-after its acquiring CAS.
2. Adjacency: if O4_t exists, it immediately follows $A_t$. By induction on the position of $A_t$ (A0). Let $X_1$ be the write right after $A_t$, and suppose $X_1\ne$ O4_t. If $X_1$ is a CAS, it read $A_t$'s non-NONE value (RMW), so it is an O3, and OW1 says $t$ has no O4. If $X_1$ is the O4 of another tenure $t_0$, then $A_{\mathrm{t0}}$ is before $A_t$ ($A_{\mathrm{t0}}sb$ O4_t0, COH-WW), and by the induction hypothesis O4_t0 immediately follows $A_{\mathrm{t0}}$, not $A_t$: contradiction.
3. (a). By step 2 and RMW, an O2 reads NONE from $\mathrm{init}$ or from an O4, which closes the previous block; an O3 reads a non-NONE value, which is an acquiring CAS, immediately before it.
4. (b) for consecutive tenures. If $A_{t\prime }$ is an O2, it read O4_t: every action under $t$ is $\mathrm{sb}$-before O4_t (release), and O2 acquires, so O4_t $sw{A}_{t\prime }$. If $A_{t\prime }$ is an O3, it read $A_t$, and OW1 applies. Actions under $t^{\prime }$ are $\mathrm{sb}$-after $A_{t\prime }$. Transitivity extends (b) to any $t$ before $t^{\prime }$; (c) is the totality of $\mathrm{mo}$.

O2 must acquire exactly when it reads an O4; O2 and O3 must release (for O1 in OW1 step 1); O4 must release.

9. Proofs: epochs and seals

EP1. Epoch sequence

Statement. The writes to global_epoch are $\mathrm{init}$ (abstracted as one write of 2, A1) and R5s; an R5 of tenure $t$ writes R0$\left(t\right)+1$. Along $\mathrm{mo}$ the values are 2, 3, 4, ..., each exactly once. If $t$ precedes $t^{\prime }$ and $t$ has an R5, then R0$\left(t^{\prime }\right)\ge$ R0$\left(t\right)+1$; hence R0$\left(t\right)<$ R0$\left(t^{\prime }\right)$ implies that $t$ precedes $t^{\prime }$. Every thread's successive loads of the epoch are non-decreasing.

Outline. R0 and R5 run only under ownership, so OW2 makes them serial; each R0 then reads the latest earlier R5, and each R5 adds one.

Proof.

1. Epoch writes: $\mathrm{init}$ (the store of 0 at cache/mod.rs:216 and of 2 at $254$, one write by A1) and R5 (rotation.rs:199), which writes $e+1$ after R0 read $e$ (rotation.rs:89) (F5). R0 and R5 are under ownership, at most one each per tenure.
2. By OW2(b) every R5 of a tenure before $t^{\prime }$ happens before R0$\left(t^{\prime }\right)$, and R0$\left(t^{\prime }\right)$ happens before every R5 of a later tenure and its own R5. With $\mathrm{init}$ first (A1), the serial-reads lemma says that R0$\left(t^{\prime }\right)$ reads the $\mathrm{mo}$-latest epoch write of an earlier tenure, or $\mathrm{init}$. So each R5 writes one more than the $\mathrm{mo}$-latest epoch write before it: the values along $\mathrm{mo}$ are 2, 3, 4, ..., each once (no gaps).
3. If $t$ precedes $t^{\prime }$, R0$\left(t\right)hb$ R0$\left(t^{\prime }\right)$ (OW2(b)), so R0$\left(t^{\prime }\right)$ reads the write R0$\left(t\right)$ read or a later one (COH-RR), and if $t$ has an R5, R0$\left(t^{\prime }\right)\ge$ R0$\left(t\right)+1$ (step 2). The contrapositive, with OW2(c), gives "R0$\left(t\right)<$ R0$\left(t^{\prime }\right)$ implies $t$ before $t^{\prime }$".
4. COH-RR and step 2 make each thread's loads non-decreasing.

EP2. Seal persistence

Statement. For stamp $e$ (arena $emod3$):

• (i) Every R4 writing stamp $e$ is made by a tenure with R0 $=e-1$. There may be several, when an owner dies between R4 and R5 and its taker resets again. All of them precede every tenure with R0 $\ge e$.
• (ii) Once Z$\left(e\right)$ exists, every $\mathrm{ctl}$ write $mo$-after Z$\left(e\right)$ with stamp $e$ is sealed, and every sealed value with a non-zero stamp $e$ is Z$\left(e\right)$ itself or $mo$-after Z$\left(e\right)$, on the same word; so Z$\left(e\right)$ is unique. It is made by a tenure with R0 $=e$.
• (iii) Hence an ordinary (non-RMW) load of the $\mathrm{ctl}$ word of arena $emod3$ returning $(\mathrm{stamp}e,\mathrm{unsealed})$ reads a write $\mathrm{mo}$-before Z$\left(e\right)$: it is $\mathrm{cob}$-before Z$\left(e\right)$.

No exact shape of $\mathrm{mo}\left(\mathrm{ctl}\right)$ is claimed: a taker may repeat R4, and after a death between R4 and R5 the reset has left arena $e+1$ unsealed while the epoch is still $e$.

Outline. Only R4 changes a $\mathrm{ctl}$ word's stamp. B1 adds a multiple of 2^33 (a carry out of bit 63 is discarded, so bits 0-32 never change), and R1 sets the sealed bit keeping stamp and bump. So after the seal of stamp $e$, the stamp-$e$ values form an RMW chain that keeps the bit, until an R4 writes another stamp. An R4 stamping $e$ again would need a tenure with R0 $=e-1$ after the sealing tenure (R0 $=e$), which EP1 rules out.

Proof.

1. $\mathrm{ctl}$ writes (F5): $\mathrm{init}$ (stamp 2 unsealed, or stamp 0 sealed); B1 (keeps stamp and sealed bit); R1 (sets sealed, keeps stamp and bump); R4 of a tenure $t$ (writes $($R0$\left(t\right)+1,\mathrm{unsealed},0)$ into arena $($R0$\left(t\right)+1)mod3$). Stamps are read as full epochs within an operation (A4).
2. (i). An R4 stamping $e$ is by a tenure with R0 $=e-1$ (step 1). For any tenure $t^{\prime }$ with R0$\left(t^{\prime }\right)\ge e>e-1$, EP1 puts the R4's tenure before $t^{\prime }$.
3. (ii). Z$\left(e\right)$ is made by a tenure $t_Z$ with R0 $=e$ (R1 seals only a word of stamp R0, rotation.rs:97, 114-119). By (i) and OW2(b), every R4 stamping $e$ happens before Z$\left(e\right)$, so it precedes Z$\left(e\right)$ in $\mathrm{mo}$ (COH-WW); so does $\mathrm{init}$ (A1). Walk along $\mathrm{mo}$ from Z$\left(e\right)$: each later write with stamp $e$ is a B1 or an R1, an RMW reading its immediate predecessor; the stamp of the predecessor is then $e$ as well, so by induction it descends from Z$\left(e\right)$ through writes that keep the bit. Each step of that walk goes back along $mo$ (RMW), so the value is Z$\left(e\right)$ or $mo$-after it (transitivity); EP3(ii) needs this order. Likewise every sealed value with a non-zero stamp is a successful R1 or $mo$-after one, on the same word and with the same stamp (the sealed $\mathrm{init}$ values have stamp 0; R4 writes unsealed). Two successful R1s on stamp $e$ are impossible: the later one in $\mathrm{mo}$ would read a sealed value, but a successful R1 reads the unsealed value it expects.
4. (iii). An ordinary load of that control word returning $(\mathrm{stamp}e,\mathrm{unsealed})$ reads a write $x$ that is neither Z$\left(e\right)$ nor after it (it would be sealed), so $x$ is before Z$\left(e\right)$ ($\mathrm{mo}$ is total): the load is $\mathrm{cob}$-before Z$\left(e\right)$.

EP3. Seal before reuse

Statement. A successful Z$\left(e\right)$ has $e\ge 2$ and happens before:

• (i) the R4 and R5 of every publishing tenure with R0 $=e$;
• (ii) the R1F of every tenure $t$ with R0$\left(t\right)=e$ that reaches R1F, whether or not $t$ later publishes;
• (iii) every event under any tenure with R0 $=e+2$, its R1F included, which is the fence of the reuse scan;
• (iv) for $e\ge 2$, every event sequenced after an acquire load of the epoch that returns $e+1$; in particular the C2 and C3 of a recheck whose C1 read $e+1$.

Form (iii), at R1F, is what the reuse scan relies on; forms (ii) and (iv) are what the readiness scans rely on (PN3).

Outline. A tenure leaves the seal loop only after the seal: its own R1, or a sealed word it loaded, which an earlier tenure sealed (OW2). That holds whether or not the tenure publishes, so the fence it runs right after the loop follows the seal. Two publications later, the seal precedes everything the next-but-one tenure does under ownership. A load that acquires $e+1$ acquires an R5 that followed the seal.

Proof.

1. (ii). Let $t$ reach R1F, with R0$\left(t\right)=e$. It left the seal loop (rotation.rs:96-123) either on its own successful R1, which is Z$\left(e\right)$ and sequenced before R1F, or on a load $l$ under $t$, the initial load or a failed CAS, returning $u=(\mathrm{stamp}e,\mathrm{sealed})$, with $lsb$ R1F (F5). In the second case $u$ is Z$\left(e\right)$ or $mo$-after it (EP2(ii)), where Z$\left(e\right)$ is made by a tenure $t_Z$ with R0 $=e$. If $t$ preceded $t_Z$, $l$ would happen before Z$\left(e\right)$ (OW2(b)) and would read a write $mo$-before it (COH-RW): a contradiction. If $t_Z=t$, Z$\left(e\right)$ is sequenced before R1F. Otherwise $t_Z$ precedes $t$ (OW2(c)), and Z$\left(e\right)$ happens before everything under $t$, R1F included (OW2(b)).
2. (i). A publishing tenure's R4 and R5 are sequenced after its R1F (F5); apply (ii).
3. (iii). Let $t_2$ have R0$\left(t_2\right)=e+2$. By EP1 it read the R5 of a tenure $t_1$ with R0 $=e+1$, whose R0 read the R5 of a tenure $t_0$ with R0 $=e$. By (i), Z$\left(e\right)hb$ R5$\left(t_0\right)$. $t_0$ precedes $t_1$ precedes $t_2$ (EP1), so OW2(b) carries this to everything under $t_2$.
4. (iv). The load returns $e+1\ge 3$, not $\mathrm{init}$'s value 2, so it read the R5 of a tenure $t_0$ with R0 $=e$ (EP1), a release: R5$\left(t_0\right)sw$ the load (REL-ACQ). By (i), Z$\left(e\right)hb$ R5$\left(t_0\right)$. Then follow $sb$.

Form (ii) does not assume publication because a tenure may certify (R3C) and then die before R5. Form (i) stays limited to publishing tenures: QU1 and SP1 cover every R4 directly.

EP4. Reset before use

Statement. The R4 of a publishing tenure happens before every acquire load (W1) that reads the epoch its R5 wrote.

Outline and proof. R4 $\mathrm{sb}$ R5 (F5, one R4 per tenure), R5 is a release and W1 an acquire reading it: R4 $\mathrm{sb}$ R5 $\mathrm{sw}$ W1 (REL-ACQ).

10. Proofs: pins and quiescence

PN1. Pin writes are release-serial

Statement. The non-announce writes to a pin (W2, W7, P6) are release writes, each made on behalf of a claim, and they are serial ($\mathrm{hb}$ totally orders them; $\mathrm{mo}$ agrees by COH-WW). Every pin write lies in the release sequence of its head, and has the head's pinned epoch. Hence if an acquire load $r$ of the pin reads a non-announce write $N$ or any write $\mathrm{mo}$-after $N$, then $Nhbr$.

Outline. W2 and W7 are the registrant's; P6 is a stealer's, made as the new registrant. So SL1 orders them all. R3A is the only other writer, and it is an RMW keeping the pinned epoch, so it never breaks a release sequence.

Proof.

1. Pin writes: $\mathrm{init}$ (UNPINNED, A1), W2 (release store), W7 (release swap), P6 (release store), R3A (relaxed CAS adding ROTATION_WAITING, F5).
2. W2 and W7 are made by the registrant (A2); P6 by a stealer after its P5, on behalf of the stealing claim. Actions of one claim are $\mathrm{sb}$-ordered (A2), those of different claims $\mathrm{hb}$-ordered (SL1(b)): the non-announce writes are serial.
3. Head. Walk back along $\mathrm{mo}$ from any pin write $w$: each R3A is an RMW reading its immediate predecessor (RMW), so $w$ lies in the release sequence of the last non-announce write at or before it (or $\mathrm{init}$), with the same pinned epoch.
4. Let $r$ (acquire) read $w$, at or after $N$. The head $H$ of $w$ is $N$ or after it. $H$ is a release, so $Hswr$ (REL-ACQ); if $H$ is $\mathrm{init}$, then $N=\mathrm{init}$ and A1 applies. If $NmoH$, step 2 and COH-WW give $NhbH$.

W2's release is essential: a scan may read the registrant's next W2, which must carry the previous attempt's record writes.

PN2. Attempt closure

Statement. Let W2 be the pin store of a store attempt $w$ of registration $G$. Every action of $w$ from W2 to W7 is, or happens before, every non-announce write $N$ to that pin that is $\mathrm{mo}$-after W2.

The next non-announce write after W2 need not be $w$'s W7 or the P6 of $G$'s own reaper. If $w$ never executes its W7 and that reaper dies after its P4 but before its P6, any next non-announce write is the P6 of a later descendant in the steal chain. A consistent schedule can have two successive reapers die before clearing and a third reaper execute that P6.

Outline. If $N$ is $G$'s own, F1 makes the attempt's W7 come first. If $N$ belongs to a later claim, SL1(b) orders all of $G$ before it. An earlier claim cannot write after W2.

Proof. $N$ is made on behalf of a claim $c_N$ (PN1).

• $c_N=G$. W2 and $N$ are $\mathrm{sb}$-ordered (A2), and $Nmo$-after W2 rules out $Nsb$ W2 (COH-WW). By F1 (exit) the attempt's W7 is $N$ or $\mathrm{sb}$-before it. Every action of $w$ from W2 to W7 is $\mathrm{sb}$-before or at W7.
• $c_N$ before $G$ in $\mathrm{mo}\left(\mathrm{state}\right)$. SL1(b) gives $Nhb$ W2, hence $Nmo$ W2 (COH-WW): impossible.
• $c_N$ after $G$. SL1(b): every action of $G$, those of $w$ included, happens before $c_N$'s claim, which is $\mathrm{sb}$-before $N$.

As a corollary, two store attempts in one slot are $\mathrm{hb}$-ordered (att_order).

PN3. Pin visibility

Statement. Let $w$ be a store attempt in slot $i$ for epoch $e_w$: W2 $\mathrm{sb}$ W3 $\mathrm{sb}$ B0, and B0 read $(\mathrm{stamp}{e}_w,\mathrm{unsealed})$. Let $f$ be a SeqCst fence with Z$\left(e_w\right)hbf$, and $\mathrm{Sc}$ any load of slot $i$'s pin with $fsb\mathrm{Sc}$. Then $\mathrm{Sc}$ reads W2 or a write $\mathrm{mo}$-after it.

No ordering is needed on W2, B0 or $\mathrm{Sc}$. The production instances are:

• (a) $f$ is the R1F of the tenure with R0 $=e_w+2$, and $\mathrm{Sc}$ its R3 load of slot $i$ (reuse, QU1; EP3(iii));
• (b) $f$ is the R1F of a tenure with R0 $=e_w$, and $\mathrm{Sc}$ its R3 load of slot $i$ (readiness, RD1; EP3(ii));
• (c) $f$ is the C2 of a recheck whose C1 read $e_w+1$, and $\mathrm{Sc}$ its C3 load of slot $i$ (readiness, RD1; EP3(iv)).

The attempt $w$ ranges over every store attempt, those of a participant that has just rotated included: W3 is the writer side of every pass. The scan side is $f$, R1F or C2, never a W3.

Outline. Store buffering: two SeqCst fences, one on each side. The writer's B0 saw the arena unsealed, so it is coherence-before the seal, and the seal happens before $f$: the writer's W3 comes before $f$ in $S$. A scan missing W2 would put $f$ before the writer's W3. A writer cutting from its chunk does no RMW on $\mathrm{ctl}$, so only these fences relate it to the rotation.

Proof.

1. B0 read $(\mathrm{stamp}{e}_w,\mathrm{unsealed})$, so B0 $\mathrm{cob}$ Z$\left(e_w\right)$ (EP2(iii)). With W3 $\mathrm{sb}$ B0 and Z$\left(e_w\right)hbf$, SC-4.4 ($X=$ W3, $a=$ B0, $b=$ Z$\left(e_w\right)$, $Y=f$) puts W3 before $f$ in $S$.
2. Suppose $\mathrm{Sc}$ read a write $\mathrm{mo}$-before W2. Then $\mathrm{Sc}cob$ W2, and SC-4.4 ($X=f$, $a=\mathrm{Sc}$, $b=$ W2, $Y=$ W3, using $fsb\mathrm{Sc}$ and W2 $\mathrm{sb}$ W3) puts $f$ before W3: contradiction ($\mathrm{psc}$ is acyclic, A0).
3. $\mathrm{mo}\left(\mathrm{pin}\right)$ is total, so $\mathrm{Sc}$ read W2 or a later write.

QU1. Quiescence before reuse

Statement. Let $w$ be a store attempt for $e_w$. For every tenure $t$ with R0$\left(t\right)\ge e_w+2$ that executes R4, every action of $w$ from W2 to W7 happens before R4$\left(t\right)$.

This covers every R4, a repeated one too. If no tenure with R0 $\ge e_w+2$ executes R4, the statement is vacuous.

Outline. The tenure with R0 $=e_w+2$ scans $w$'s slot after its own R1F, which follows Z$\left(e_w\right)$ (EP3(iii)). So the scan sees W2 or later (PN3). It passes only on a different pinned epoch, so it read a write whose head is a later non-announce write $N$: $w$'s W7, a later W2, or a reaper's P6. PN2 puts $w$ before $N$, PN1 puts $N$ before the scan, and the scan is before R4. Later tenures inherit the order through ownership.

Proof.

Case R0$\left(t\right)=e_w+2$.

1. Before R4, $t$'s holder loaded every slot's pin (A7: all participant_capacity slots) with an acquire load $\mathrm{Sc}$ after its R1F $f$, and the final load passed: pinned epoch UNPINNED or at least R0$\left(t\right)-1=e_w+1$ (flag masked) (F5; rotation.rs: load 141, pass test 148). After a reap, the loop reloads, so the final load is the one that passed.
2. EP3(iii) gives Z$\left(e_w\right)hbf$, so $\mathrm{Sc}$ read W2 or a later write $p$ (PN3(a)).
3. The head $H$ of $p$ has $p$'s pinned epoch, which passed, so it is not $e_w$; W2 has pin $e_w$, so $H\ne$ W2. W2 is a non-announce write at or before $p$, hence W2 $moH$.
4. PN2: every action $a$ of $w$ from W2 to W7 is $H$ or $ahbH$. PN1: $Hhb\mathrm{Sc}$. And $\mathrm{Sc}sb$ R4$\left(t\right)$.

Case R0$\left(t\right)>e_w+2$. R0$\left(t\right)$ read a value at least $e_w+3$, so by EP1 (no gaps) some tenure $t_1$ published $e_w+3$, with R0$\left(t_1\right)=e_w+2$; it has an R4 (F5). The first case gives $ahb$ R4$\left(t_1\right)$. R0$\left(t_1\right)<$ R0$\left(t\right)$, so $t_1$ precedes $t$ (EP1), and R4$\left(t_1\right)hb$ R4$\left(t\right)$ (OW2(b)).

For a writer that died pinned, the only route from its record writes to the reuse is: its writes, the verdict (A3), the reaper's P6 (release), R3's acquire of the cleared pin, R4. The release sequence of W2 does not cover the record writes, which follow W2. W6 lies between W2 and W7, so the counter reset at R4 also follows every count of the previous incarnation; GenMC's chunked_insert_blocks_reuse checks exactly that pair.

QU2. Incarnations are serial blocks

Statement.

• (a) If attempts $w$ (epoch $e$) and $w^{\prime }$ (epoch $e^{\prime }\ge e+3$) exist, every action of $w$ from W2 to W7 happens before every action of $w^{\prime }$ from W2 to W7. So the writes that different incarnations make to any arena word are ordered in $\mathrm{mo}$ by epoch.
• (b) No load of $w$ between W2 and W7 reads a write of an attempt for an epoch $\ge e+3$.

Outline. Through the tenure that published $e^{\prime }$: QU1 for its R4, then EP4 to $w^{\prime }$'s W1. Going through tenures, not through an induction over incarnations, also handles incarnations with no attempts.

Proof.

1. $w^{\prime }$'s W1 read $e^{\prime }$ (F2), not $\mathrm{init}$'s 2, so it read the R5 of a tenure $t^{\prime }$ with R0$\left(t^{\prime }\right)=e^{\prime }-1\ge e+2$ (EP1).
2. QU1: every action of $w$ from W2 to W7 happens before R4$\left(t^{\prime }\right)$. EP4: R4$\left(t^{\prime }\right)hb$ W1 of $w^{\prime }$, which is $\mathrm{sb}$-before its W2 and later actions. That is (a); COH-WW turns it into $\mathrm{mo}$ order.
3. (b): a load of $w$ happens before any such write (a), so it cannot read it (COH-RW).

11. Proofs: record space

SP1. B1 lands in its incarnation

Statement. Every B1 of a store attempt for $E$:

• (a) reads a $\mathrm{ctl}$ value with stamp $E$, and happens after every R4 that stamps $E$, repeated resets included;
• (b) lies in $\mathrm{mo}\left(\mathrm{ctl}\right)$ after the base that its B0's value descends from, and before every R4 stamping $E+3$.

Outline. Every R4 stamping $E$ belongs to a tenure at or before the one that published $E$, so it happens before the attempt's W1 (EP4, OW2). Every R4 stamping $E+3$ comes after the attempt (QU1). Between them, only RMWs that keep the stamp touch the word.

Proof.

1. Every R4 stamping $E$ is by a tenure with R0 $=E-1$ (EP2(i)). The attempt's W1 read $E$ from the R5 of a publishing tenure $t_p$ with R0 $=E-1$. A tenure with R0 $=E-1$ cannot come after $t_p$ (its R0 would read at least $E$, EP1), so every such R4 is at or before $t_p$'s and happens before R5$\left(t_p\right)$ (OW2(b)), hence before W1 (REL-ACQ) and B1. By COH-WW it precedes B1 in $\mathrm{mo}$.
2. B0 read a value $u$ of stamp $E$, which is at or after every such R4 (COH-WR from step 1) and descends from a base of $E$ (EP2's ${\mathrm{ctl}}_{\mathrm{base}}$). B0 $\mathrm{sb}$ B1, so B1 reads $u$ or a later write.
3. B1 is between W2 and W7, so it happens before every R4 stamping $E+3$ (QU1; that tenure has R0 $=E+2$), and precedes it in $\mathrm{mo}$ (COH-WW).
4. Between $u$ and B1 lie no R4 stamping $E$ (step 2), no R4 stamping $E+3$ (step 3), and no other R4 on this arena (they stamp $E+3k$). So all writes there are B1s and R1s, which keep stamp $E$.

SP2. Bounded bump, one failure per slot

Statement. Within incarnation $E$:

• (a) After a failed B1 by a slot, every later B0 of that slot sees the arena sealed, or its bump past capacity, or another stamp, and stops before B1. So each slot fails at most one B1 per incarnation.
• (b) Along $\mathrm{mo}\left(\mathrm{ctl}\right)$ the bump is exactly the sum of the claims of the B1s so far. It never exceeds $\mathrm{capacity}+P·C-n_{\min }$, where $P$ is the participant capacity, $C$ the largest claim (chunk or maximal record; every record is at most the maximal record, F3) and $n_{\min }$ (16 bytes, an empty key and value) the smallest record. As a bound on the B1 update and success arithmetic, it is sharp: a 32-byte arena, one participant, and two successful 16-byte claims reach bump 32, with $C=n_{\min }=16$. This arithmetic trace is not a full concurrent execution witness. So every B1 has $\mathrm{bump}+\mathrm{claim}<2^{31}$ by A5: no B1 carries out of the bump field.

Outline. A failure leaves the arena sealed or the bump above capacity, and both persist for the rest of the incarnation, so no success follows a failure and the failing slot stops at its next B0. The last success leaves the bump at most $\mathrm{capacity}-n+C$, and at most one failure per slot follows it.

Proof. By induction along $\mathrm{mo}\left(\mathrm{ctl}\right)$ from the base of $E$ (A0), for both parts together: a failure's new bump exceeds capacity only because the bump did not wrap.

0. Every claim is at most $C$: a chunk is $C$ or less by definition, and a record claim $n$ is at most max_record_size (F3).

1. By SP1, B1 reads a value of stamp $E$. It succeeds iff that value is unsealed with $\mathrm{bump}+n\le \mathrm{capacity}$ (store.rs:332); otherwise it fails, leaving the value sealed, or with bump $\mathrm{bump}+\mathrm{claim}\ge \mathrm{bump}+n>\mathrm{capacity}$ (no wrap, by the induction hypothesis for (b)).

2. Later writes in $E$ are B1s (bump never decreases) and R1s (set the seal), so "sealed or bump > capacity" persists to the next R4. No success follows a failure.

3. (a). A later attempt of the same slot happens after the failed B1 (att_order, from PN2), so its B0 reads that B1 or a later write (COH-WR). Seeing another stamp, or sealed, it stops before H1 and B1; seeing $\mathrm{bump}>\mathrm{capacity}$, it may still cut from its chunk at H1, but stops at store.rs:311-313, before B1.

4. (b). The base has bump 0; R1 keeps the bump (seal_bump); B1 adds its claim, so the bump is the sum of the claims. A success needs $\mathrm{bump}+n\le \mathrm{capacity}$ and adds at most $C$; let the last success, by slot $X$, leave the bump at most $\mathrm{capacity}-n+C$. Every failure comes after it, at most one per slot (a).

   • If $X$ does not fail afterwards, at most $P-1$ failures follow: the bump stays at most $\mathrm{capacity}+P·C-n$.
   • If $X$ fails afterwards with claim $c$, the B0 of that attempt happens after $X$'s success and found room for $c$, so the success left the bump at most $\mathrm{capacity}-c$: the bump stays at most $\mathrm{capacity}+(P-1)·C$.

   Either way it stays at most $\mathrm{capacity}+P·C-n_{\min }$. A5 checks $\mathrm{capacity}+P·C<2^{31}$ (omitting the $n_{\min }$ slack, config.rs:241-256), so every B1 has $\mathrm{bump}+\mathrm{claim}<2^{31}$.

A failed B1's bytes are lost (an unindexed hole beyond capacity or in a sealed arena); nothing rolls them back.

SP3. Chunk words are sequential

Statement. Every H1 load of chunk_epoch, chunk_cursor or chunk_end reads the latest store to that word by its own registration. The epoch load may read this registration's H0 reset (zero), or an H2 from an earlier attempt. If its epoch matches the current attempt, the epoch and end loads read the H2 stores of that chunk's claim; the cursor load reads that H2's store or the last H1 cut since. For these matching probes, the cursor stays within [bump + n_0, min(bump + claim, capacity)], where $\mathrm{bump}$, $n_0$ and $\mathrm{claim}$ are those of the claiming B1. Only the chunk_epoch reset (H0) before a registration's first W2 is needed: these guarantees also hold if registration and steal omit the cursor and end reset stores while retaining the epoch store in the same position. Thus a chunk left by an earlier registration, or in a stolen slot, is never used.

Outline. The chunk words are touched only by the slot's current registrant, so SL1 makes them sequential. H0 runs before the first pin of every registration and stores epoch 0, which no epoch equals, so a matching chunk_epoch can only come from this registration's own H2. The epoch stored is the full 64-bit epoch: no stamp aliasing.

Proof.

1. The chunk words are written only by $\mathrm{init}$, H0, H1 (cursor) and H2 (F4), all by the slot's current registrant (in claim() and steal() after the claim; in attempts), and loaded only by H1. By SL1 and A2 they are serial, and every H1 load is $\mathrm{hb}$-ordered against every store: it reads the latest one before it (serial-reads lemma).
2. The latest chunk_epoch store before an H1 of registration $G$ is $G$'s H0 (value 0, which differs from any $e\ge 2$) or an H2 of $G$ in an earlier attempt (F4: $G$'s H0 precedes its first W2). If H1 found chunk_epoch == e, it is an H2 of an earlier attempt $w_0$ of $G$ for the same epoch $e$ (att_order orders the attempts). chunk_end's latest store is the same H2: any later H0 or H2 would also be the latest chunk_epoch store.
3. The cursor's latest store is that H2's ($\mathrm{bump}+n_0$) or an H1 cut since (each advancing by its own $n$ after a room check). The room check $\mathrm{end}-\mathrm{cursor}\ge n$ in u32 is exact, because $\mathrm{cursor}\le \mathrm{end}\le \mathrm{capacity}<2^{31}$ (A5), so $\mathrm{cursor}+n\le \mathrm{end}$.

SP4. Disjoint, in-area reservations

Statement. In incarnation $E$ the byte ranges of successful reservations, whether won at B1 or cut from a chunk at H1, are pairwise disjoint and lie in [0, record_area_size). The u32 room check of H1 is exact.

Outline. Successful B1s are RMWs on a bump that never wraps, so their claims $[\mathrm{bump},\mathrm{bump}+\mathrm{claim})$ are disjoint intervals. A record takes the first $n$ bytes of its claim; a chunk is the rest, clipped to capacity, and is cut by one registration with an advancing cursor.

Proof.

1. Successful B1s on $\mathrm{ctl}$ of $E$ read their immediate predecessors (RMW) and the bump is exactly the claims so far, with no wrap (SP2): the claims $[\mathrm{bump},\mathrm{bump}+\mathrm{claim})$ are pairwise disjoint.
2. A B1 reservation is $[\mathrm{bump},\mathrm{bump}+n)$ with $\mathrm{bump}+n\le \mathrm{capacity}$ (the success check).
3. A cut is $[\mathrm{cursor},\mathrm{cursor}+n)$ inside [bump + n_0, min(bump + claim, capacity)) of the B1 claim that made the chunk (SP3), so inside that claim, after its own record, and below capacity.
4. Two cuts of one chunk are disjoint because the cursor only advances (SP3); cuts of different chunks, and a cut against a B1 reservation, lie in different claims (step 1).

SP5. Write-once records

Statement. Each record word is written at most once per incarnation, by the attempt that reserved it (W4 or W5). In the $\mathrm{mo}$ of a record word, the writes of different incarnations appear in epoch order.

Outline and proof. An attempt stores each word of its reservation once, inside its reservation (F3); reservations of one incarnation are disjoint (SP4). Across incarnations, QU2(a) orders the writes.

12. Proofs: index and hits

IX1. Publication follows the record

Statement (code-level). Only $\mathrm{init}$ (zero fill: stamp 0, offset 0) and I2 write index slots. An I2 of attempt $w$ lies in an index slot of $w$'s arena and writes an entry whose stamp is $e_{w}mod{2}^{32}$ and whose offset is $w$'s own reservation offset, a multiple of 8. Every word of $w$'s record, the lengths word holding $w$'s lengths included, is stored by $w$ $\mathrm{sb}$-before the I2.

Outline. A writer stores its whole record, then publishes an entry naming it; nothing else writes the index. There is no concurrency argument: this restates F3 and F8 as the one index fact that hit integrity needs. The shape of the index (one slot per key, no gap) is not needed for G1-G3; it is RB4, which G4 needs.

HT1. Recycled reads are caught

Statement. Let a lookup make an arena load $Y$ (index or record word) $\mathrm{sb}$ D6 that reads a store of an attempt $x$ for epoch $e_x$. Then V2, $\mathrm{sb}$-after D6, reads an epoch $\ge e_x$. With A6, if $e_x\ge E+3$ for a probe of epoch $E$, V2's u32 age exceeds 1 and the probe returns Retry.