Herlihy

The Herlihy Doctrine

Named for Maurice Herlihy, who founded wait-free synchronization. This skill turns "everything atomic" from a slogan into a procedure grounded in his published results — so every atomicize/rewrite picks the sound primitive, has a provable correctness point, claims the true progress guarantee, and never chases something topology forbids.

Before writing the concurrent code, invoke read-the-damn-docs for the exact atomic API in play (Rust std::sync::atomic orderings, CUDA atomicCAS/ atomicAdd semantics, the memory model). A wrong memory ordering is a Heisenbug that a parity gate catches only sometimes — ground it in the docs.

The scholarship (verified primary sources, with the NOT-Herlihy flags) lives in references/corpus.md. Read it before citing any result — misattributing a technique to Herlihy is the exact overclaim this skill exists to prevent.

The core move: constraint → atomicize

Given a constraint (a lock, a blocking wait, a serialization/step-barrier), rewrite it atomic by running these seven rules in order. Each rule is grounded in a specific Herlihy result — cite it, don't assert it.

1. Name the constraint's consensus need. Does the rewrite require multi-party agreement — who wins a slot, who commits, who retires exactly once? If yes, the primitive floor is CAS. (Consensus-number hierarchy — Herlihy, "Wait-Free Synchronization", TOPLAS 1991.)

2. Pick the minimum sound primitive. Monotonic reservation / counters → fetch-add (consensus number 2). Any contended commit or reclaim → CAS (consensus number ∞). Never fetch-add where agreement is needed — two "winners" is a latent correctness bug. Never CAS a pure counter — a wasted retry loop. (Herlihy 1991.)

3. Check the impossibility wall first. A CAS-free (read/write/fetch-add-only) fast path for any contended commit is provably impossible wait-free. Don't burn a run inventing one. CAS (∞) is exactly the primitive that buys you out of the register wall. (Topological computability — Herlihy & Shavit, JACM 1999, Gödel Prize.)

4. Fix the linearization point = the single atomic step. Every fast path gets exactly one instant — the successful CAS or the release-store — where its effect becomes visible. A reader seeing old state must see a legal pre-commit history. Linearizability is local: prove each object at its point, and whole-engine correctness composes for free. (Herlihy & Wing, TOPLAS 1990.)

5. Choose the progress guarantee by whether a token can wait. Token-flow paths target wait-free. But upgrade a lock-free path to wait-free (via helping) only where measured starvation exists — helping costs an announce-scan on every op. Most paths at low concurrency are fine lock-free. (Universal construction / helping — Herlihy 1991; progress lattice — Herlihy & Shavit, OPODIS 2011.)

6. Reduce multi-word to one word before reaching for transactions. Prefer a version-pointer / index swap that makes the commit a single CAS (wait-free) over STM/HTM (only lock-free — abort/retry, livelock-prone, and there is no HTM on the GPU decode path). (Transactional Memory — Herlihy & Moss, ISCA 1993 — as a design lens, not a hot-path kernel.)

7. Pick reclamation by reader lifetime. Bounded, non-stalling readers (GPU decode kernels, one step long) → epoch-based reclamation (tick an epoch per step, free blocks retired ≥2 epochs back). Cite Pass-the-Buck as the canonical safe-reclamation lineage; use its per-guard handoff only if readers can stall unboundedly (not our case). (Repeat Offender / Pass-the-Buck — Herlihy, Luchangco, Moir, DISC 2002, Dijkstra Prize 2022. EBR itself is Fraser 2004 — NOT Herlihy.)

Per-subsystem map (LLM-inference)

Match the subsystem to the right result, progress guarantee, and linearization point. This is the reference for atomic-inference; the shape generalizes.

The honest hot-path caveat (read before you build)

Two Herlihy constructions are correctness references, not hot-path kernels:

• The universal construction (announce + consensus + help) proves any sequential object can be made wait-free — but its O(n) announce-scan per op serializes throughput. Borrow the helping idea and the proof, not the literal construction. Ship a bespoke single-CAS / fetch-add structure.
• Transactional memory gives multi-word atomicity but pays abort/retry and has no GPU-decode implementation. Reduce to one word instead.

Where a hand-rolled lock-free structure already gives the needed progress (a Treiber stack for the free-list, an MS-queue for the ring — both not Herlihy, see corpus.md), use it. The doctrine tells you which primitive is sound and which guarantee you actually have — it is not a mandate to build the general construction literally.

Audit rubric (labeling an existing path's true guarantee)

Cheap, high-value — run it before claiming any path is "lock-free":

• Single CAS / single release-store, bounded retries → genuinely wait-free.
• CAS-loop that can livelock under contention → only lock-free (or obstruction-free) — do not call it wait-free.
• Any Mutex / RwLock / epoch barrier / blocking wait on the path → it is blocking, not non-blocking. That is the constraint to rewrite.

Over-claiming a progress guarantee is the concurrency equivalent of an unscoped "world-first" — the same honesty discipline applies. Label the true class, then upgrade only the paths a token actually waits on.

The one-sentence version

Name what needs agreement, pick CAS if it does and fetch-add if it doesn't, give the commit one visible instant, claim only the progress you can prove, free memory by epoch, and never chase a wait-free path topology already ruled out.