A One-page orientation. W7 is Jonathan Rees's 1996 security kernel built on the lambda calculus, in which capabilities, closures, and continuations are all first-class values. That design is powerful and clean, but making continuations first-class exposes a cluster of hazards — the "W7 problems." The Church Machine (CM) shares W7's lambda-calculus foundation but is a machine, not a language runtime: capabilities, Threads, and continuations are enforced in hardware, not by a trusted interpreter. That shift is what lets the CM turn several of W7's soft guarantees into hard ones.
The claims below are marked [proven] (holds today on settled CM machinery), [modelled] (designed and reviewed, not yet demonstrated on the FPGA), or [open] (a real gap still under review).
1. Continuation re-invocation — a captured continuation spent twice
W7 hazard: a first-class continuation can be resumed more than once; any effect downstream of the capture point re-runs on each resume. CM answer — [modelled]. A retained checkpoint is one-shot: capture arms it, the first restore consumes it, a second restore hard-faults. The consumed mark is set as part of the restore commit (one protocol, not check-then-set), is excluded from the state that rollback itself restores, and cannot be minted anew by copying the checkpoint bytes. This makes the continuation an affine — spend-once — authority, which is the correct capability-grain answer. Honest limit: one-shot restoration stops the continuation being reused; it does not make the world transactional (see §5).
2. Capture consistency — saving state while it changes
W7 hazard: capturing your own continuation mid-execution can snapshot an
internally inconsistent state.
CM answer — [modelled]. A machine-maintained running bit records active
execution ownership (not IDE Run/Walk status). Capture happens at a defined
instruction boundary with ownership held continuously; a CHANGE to a
different Thread whose bit is already set is rejected, while a self-target
CHANGE is the explicit, preserved exception. The running bit and the one-shot
mark solve different problems — ownership vs. reuse — and neither substitutes
for the other.
3. The confused deputy — authority of the name vs. authority over the data
W7 hazard: naming a method or holding a reference is mistaken for authority over what it touches. CM answer — [proven]. The CM's founding rule: callable-method authority and authority over the accessed data are distinct; naming a method grants no memory access. Endpoint IDs, slot numbers, and tuple references are data, never authority — "conditions do not confer permissions." A stale reference cannot reach a later allocation. This is the capability model the CM has enforced since the PP250.
4. Capability leakage and revocation
W7 hazard: capabilities escape their intended scope, or cannot be withdrawn. CM answer — [proven] for containment, [open] for general revocation. Containment is structural: Thread-local storage is not automatically shared, another Thread does not silently acquire access, and private authority is never returned or published as a public method. Capture/restore of a checkpoint is itself gated by explicit, validated capability — an IDE label or a zero-filled reservation is not authorization. General revocation and replay policy for long-lived capabilities remain an explicitly flagged review item.
5. The transactional-continuation illusion — effects already in the world
W7 hazard: treating "restore the continuation" as if it undid everything the computation did. CM answer — [proven as a stated limit]. The CM refuses the illusion outright: rollback restores execution state, and optionally selected records or a heap snapshot that must be mutually consistent with it — but it cannot undo an established telephone connection, a sent message, or a device operation. Even the first rollback can replay effects performed after capture, so one-shot restore does not promise exactly-once messaging. External effects live outside the rollback boundary, and the design says so rather than pretending otherwise.
6. Failure must never degrade into a soft state
W7 hazard: a partial or interrupted operation leaves a usable-but-wrong state. CM answer — [proven discipline], [open] at one boundary. Every failed check is a hard fault — no silent fallback, no automatic retry, no restoration of an unrelated snapshot; partial internal writes leave execution blocked, not "mostly done." The one boundary still being pinned: the interrupted-restore window (consume-then-fault vs. resume-then-fault). The CM's stated preference is fail-closed — lose the continuation rather than leave it replayable — but the required ordering must be committed before build.
The through-line
Every answer above is the same mechanism in a different costume — the CM's standing principle, "everything is different but the mechanisms are always the same." A continuation is an authority; an authority is spent once, is distinct from the data it names, cannot be forged by copying, and fails closed. W7 asked these questions of a trusted interpreter; the CM answers them in hardware, which is why several soft guarantees become architectural ones. What remains open is honestly bounded: general revocation/replay policy, and the exact atomic ordering at the consume/resume commit. Neither blocks the near-term, lower-risk work (Thread-local tuple storage); both sit inside the gated continuation/rollback increment, where they belong.
Status: modelled/reviewed explainer, not an implementation specification. Mechanisms cited are at outline-and-review stage except where marked [proven].
Comments
Post a Comment