# Herlihy

> Use when atomicizing any subsystem or removing a concurrency constraint — a lock, a Mutex/RwLock, a blocking wait, a serialization point, a step-barrier, a GIL-serialized scheduler. Triggers on "make this lock-free", "atomicize this", "rewrite this atomic", "which atomic primitive", "CAS or fetch-add", "is this actually wait-free / lock-free", "prove this concurrent path correct", "how do I safely reclaim this memory under lock-free readers", or designing a KV cache / scheduler / commit / free-list / ring on hardware atomics. This is the Herlihy doctrine: pick the primitive by consensus number, fix the linearization point, choose the progress guarantee by whether a token can wait, pick the reclamation scheme by reader lifetime, and know the impossibility walls before burning a run. Reach for it by default whenever a token-flow path must be non-blocking; skip only for genuinely single-threaded code with no shared mutable state.

- Skill: `88plug/herlihy` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add 88plug/herlihy`
- Raw SKILL.md: https://api.skillmd.com/api/skills/88plug/herlihy/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: 88plug (https://skillmd.com/u/88plug)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/88plug/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.

| Subsystem | Result to apply | Progress | Linearization point |
|---|---|---|---|
| KV cache slot commit | Linearizability + CAS (∞) | Wait-free | Release-store of `ready`/tail |
| Scheduler / mid-step admission | Universal construction (announce+help) | Lock-free → wait-free *if starved* | Winning CAS on running-set splice |
| MTP commit | Single-CAS reduction (consensus ∞) | Wait-free | Successful `committed_len` CAS |
| KV-block reclamation | Pass-the-Buck lineage → EBR | Lock-free (reclaimer) | Epoch-tick store |
| Request ring | Michael-Scott queue *(NOT Herlihy)* | Lock-free | fetch-add slot index |
| On-device sampling | Linearizability discipline | Wait-free | Single argmax CAS/store |

## 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.