What Survives kill -9: The Accumulator as a Write-Ahead Log With Offset, Settled and Residue Verdicts

Pitch

Most undo systems promise to reverse everything; revl's crash recovery says, per effect, which ones are moot, which can be re-issued from a captured description, and which remain as residue, and it labels a recovery run against a model as modelled, not performed.

Abstract

A process that dies with kill -9 takes its in-memory undo closures with it, so the usual picture of crash recovery as "run the inverses again" is wrong. We describe the recovery design of revl, a language whose runtime already keeps an ordered accumulator of committed effects, each paired with its inverse. The accumulator is persisted as a write-ahead log (JSON Lines, one fsync per entry). A fresh process reads it and classifies only boundary state that outlives the dead process: an emission that left the process, or an acquire whose resource persists. In-process inverses are reported as moot. An inverse is re-issued only if it is reconstructible from a description (a named call with captured arguments); closure-only inverses are reported as residue and never pretended to run. Each emission ends as offset (its compensation ran), settled, or residue. Re-issue is graded by three register tiers (read, keyed, declared) and anything unknown gets one fenced at-most-once attempt. Recovery run without the real composition executes against an in-memory model and says so in the verdict and the exit status. On main today, crash tests exist for the Python tier (simulated kill) and for go, java, rust and wasm (real process exit after fsync), and a Lean model of the commit/abort decision is checked against the shipped recovery code on an enumerated corpus of 1620 logs (the model was edited once after 60 of them disagreed; see limits). We state what is not covered: power loss, and a crash between a witnessed mutation and its log entry.

Problem and claim

Write-ahead logging in databases logs "about to do X, and how to undo it", and recovery replays or reverses the log. Application-level effect systems (sagas, workflow engines, Python contextlib-style unwinding) usually either keep their undo in process memory, which is gone after a crash, or persist opaque callbacks that cannot be re-run in a new process.

The claim is narrower and more honest. After a crash only the boundary state matters (docs/crash-recovery.md:117-150). Recovery is sound to attempt for an effect only if its inverse can be rebuilt from a description, a named operation plus concrete arguments (docs/crash-recovery.md:152-190). Everything else must be reported, not guessed. The verdict is therefore three-valued per crossing (offset, settled, residue) and the report states which world it ran against.

A second claim is about the process, not the algorithm: because the accumulator was already a typed list of (effect, inverse) pairs with explicit non-invertible emissions, the WAL costs the language no new concept. The only new language-level requirement is the reconstructible-from-description rule.

Contributions

1. The accumulator as a write-ahead log: JSON Lines, fsync per entry, fsync failure fail-closed with truncation of the failed entry, torn tail sealed before any append (docs/crash-recovery.md:14-65,193-290).
2. The reconstructible-from-description requirement and the inverse_descriptor() split between reconstructible and closure-only inverses, with closure-only inverses surfaced as residue (docs/crash-recovery.md:152-190,736-749).
3. Two recovery paths decided by a durable marker: roll forward when activation completed (with steady-state crossings after the marker reported as residue), roll back newest-first when it did not (docs/crash-recovery.md:403-495).
4. A call-tier taxonomy for safe re-issue (read, keyed, declared, absent) and a single re-issue seam World.reissue, with at-most-once fences written before the attempt (docs/crash-recovery.md:292-375).
5. "The model is not the world": every verdict carries world: model|real, modelled calls are marked [modelled, not performed], a model run never spends a fence, and exit code 3 means clean-in-the-model but nothing reconciled (docs/crash-recovery.md:495-543).
6. Opt-in --require-settled-wal refuses to start on a WAL with unsettled emissions, and revl recover --operator-resolved SEQ logs a human acknowledgement without claiming an undo (docs/crash-recovery.md:69-93).
7. Evidence: crash tests on five tiers and a differential check of the recovery verdict against a Lean model on 1620 enumerated logs (see Evidence on main).

Related work

Evidence on main

Tree: revl main at commit 45bec431f.

Numbers that exist

• 1620 enumerated WAL scenarios where the outcome, applied set and residue of recovery.recover agree with the Lean model: formal/STATUS.md:66. The sample is exhaustive over the stated shape space, not a sample of real crashes.
• Test counts by function name (not pass rates; nothing was re-run): tests/test_crash_recovery.py 39, tests/test_wal_torn_tail_535.py 8, tests/test_idempotent_inverse_309.py 25, go 2, java 4, rust 2, wasm 2.
• Lean A8 file: 21 top-level theorem declarations. formal/STATUS.md:66 gives 18 in its theorems column. The two counts do not match and are not reconciled.
• No performance numbers (WAL overhead per effect, fsync cost, recovery time) exist.

Paper outline

1. Introduction: closures die with the process; what a restart can honestly say.
2. Background: the accumulator, inverse-or-emit (G4), compensation is not inversion.
3. The WAL: entry format, durability rules, torn tails, fail-closed fsync.
4. Reconstructible from description: descriptors, closure-only, the outlives policy.
5. Recovery: roll forward, roll back, steady-state residue, offset pairing, nested crossings and placement runs.
6. Safe re-issue: call tiers, fences, the World seam, the operator knob.
7. Model versus world: labels, exit codes, fences never spent by a model run.
8. Evaluation: crash tests on five tiers, the 1620-log differential against the Lean model, overhead (not yet measured), real-kill campaign (not yet run).
9. Limits and related work.

Threats to validity and limits

• The Python crash test is a simulated kill (tests/test_crash_recovery.py:14). The other four tiers use a clean process exit after fsync, not SIGKILL and not power loss.
• docs/crash-recovery.md:736-749 says recovery does not promise state was restored, does not reconstruct closure-only inverses, and does not undo a bare emission.
• Recovery without --composition runs against DictWorld; the verdict "is a proof about the model" (docs/crash-recovery.md:492; the no---composition default is at :502).
• The Lean model covers the abort path only; the roll-forward flush-residue surface, cascading abort and escrow are "not covered and not claimed" (formal/STATUS.md:66,69).
• The 1620-log agreement was reached by editing the model. formal/STATUS.md:1685 states that 60 of the 1620 scenarios disagreed (the model called a legacy effect re-issue clean where recover fences and reports residue) and that the model was changed to match the reference. The oracle found a real divergence, but the agreement reported is post-fix, not an independent prediction.
• The 1620 logs are enumerated at depth 2; deeper interactions are untested by that corpus.
• Several Lean theorems are specification-agreement or definitional by the file's own account, so they pin drift rather than prove depth.
• Durability is "a floor rather than a theorem" in the Lean file: power loss and fsync reaching disk are host obligations that no in-tree test settles. A witnessed mutation whose log entry is written after the forward extern returns is not covered (formal/RevL/Theorems/A8_WalDischarge.lean, header, "Not covered").
• --require-settled-wal and the opt-out flag are py-single-process only.
• The outlives-the-process decision is name-based and the language "cannot know this in general" (docs/crash-recovery.md:145-150).
• No baseline (saga engine, persisted closures) has been run on the same crash scenarios.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 45 checked, 7 corrected.

Cite this draft

@misc{revlp15,
  author       = {Thomas Moussajee},
  title        = {What Survives kill -9: The Accumulator as a Write-Ahead Log With Offset, Settled and Residue Verdicts},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P15.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.