Lifecycle states

AWC holds state that outlives any single process. A snapshot, once published, is an immutable root that other workspaces fork from. A workspace head is one durable pointer that many readers trust. A writer lease decides who may advance that pointer. When a host crashes and returns, the daemon must rebuild a correct view from disk and one database. There is no operator in that loop to disambiguate.

That is the case for explicit state machines. A snapshot is not "uploaded and maybe validated and maybe deleted." It sits in one named state, and only a fixed set of edges leave that state. The same holds for workspaces, mount sessions, and leases. This page explains why those machines are shaped the way they are, and what the daemon does with them on restart.

Why states, not flags

The rejected alternative is a handful of booleans. A snapshot could carry uploaded, validated, deleting. Six booleans compose into dozens of combinations, and most of them are impossible. Recovery code would have to test each one. The head pointer would depend on a convention nobody enforced.

A state collapses that space. "The snapshot is READY" is one fact. The legal exits are enumerable, and the illegal exits are rejectable in code. The workspace, mount-session, and lease enums each ship a transition predicate. The snapshot enum does not — its transitions are validated separately by the control plane. For a mount-session move, the store consults the predicate before it persists the record, and a transition that skips a state, loops on itself, or leaves a terminal state returns IllegalTransition. For the enums that carry the predicate, the diagram in the spec is the same graph the daemon or control plane enforces.

The payoff is deterministic recovery. On restart the daemon does not ask "what combination of flags did the dead process leave?" It asks "what state is this record in, and what edges are legal from here?"

Snapshots: gate usability behind validation

A snapshot moves through a fixed path:

UPLOADING → VALIDATING → READY
                       └──► FAILED
READY → DELETING → DELETED

The shape answers two questions.

Why is READY gated behind VALIDATING? Because a snapshot becomes a workspace base only after two things are true. Its object closure must be complete and content-addressed. Its backing objects must be durably readable before the metadata record commits. The publisher sequences the work as upload, verify, publish record, advance head, and must never publish metadata first. VALIDATING is the state where that ordering is checked. A snapshot that fails closure becomes FAILED, and only READY snapshots may serve as a new workspace base. FAILED means "never usable," not "was usable and broke."

Why is DELETING distinct from DELETED? Because logical deletion and garbage collection are two transactions. A snapshot may be DELETING while its immutable objects remain on disk, and retained references must keep reading until the deletion transaction proves the snapshot is unreachable. Conflating the two would either delete objects under live readers or never reclaim them at all.

The code adds one state the spec §12.1 diagram does not draw: DEGRADED. The spec §12.1 diagram omits it; the runbooks treat it as an operational mark set when a published snapshot references a missing object. The system returns a distinct integrity error and starts the repair runbook rather than rewriting history. DEGRADED means "readable, but some backing objects are unavailable." It is an operator condition, not a base a new workspace forks from. (The control-plane transition validator does model edges to and from it — see the caveat in Limits and what is not proven here.)

Workspaces: separate the writer from the head

A workspace is mutable; its head snapshot is not. The workspace state machine keeps the two apart:

CREATING → IDLE → MOUNTED → CHECKPOINTING → MOUNTED → IDLE → EXPIRING → DELETED

CHECKPOINTING exists as its own state so a crash mid-publish has an unambiguous resume target. On restart the daemon sees the record in CHECKPOINTING and knows the publish transaction may not have committed. It does not guess. It retries the publication with the same expected version and idempotency key. The head advances only if the precondition conjunction still holds. If it does not, the workspace stays where it was. See recover an interrupted checkpoint.

EXPIRING waits rather than deletes. An expired workspace that still has an active lease enters EXPIRING and stays there until the lease resolves. Deleting a workspace under a live writer would discard uncommitted upper bytes the agent might still need. The TTL is a statement about logical retention, not an order to tear down a data path.

FAILED is recoverable, not terminal. A workspace whose creation failed may be retried or torn down according to the failure reason. The code makes Failed → Creating, Failed → Idle, Failed → Expiring, and Failed → Deleted legal edges. Expiration is reversible for the same reason: a configurable grace period lets an operator undo a mistaken expiry, so Expiring → Idle is legal. Deleted alone is terminal.

Leases: terminal means terminal

A writer lease carries the fencing generation. Its lifecycle is small:

ISSUED → ACTIVE → RELEASING → RELEASED
           ├── timeout ──► EXPIRED
           └── admin ────► REVOKED

Two design choices matter here.

RELEASING exists so a clean unmount can publish a final checkpoint. Publication is gated by a publication predicate, and only ACTIVE and RELEASING pass it. Without RELEASING, the last checkpoint of a session would have to publish from a state the predicate rejects. The alternative is to leave the lease ACTIVE and rely on a timer, which gives publication no defined endpoint.

The three terminal states — RELEASED, EXPIRED, REVOKED — never leave. A new writer does not resurrect a released lease. It is a fresh lease row at a strictly higher generation. The transition predicate encodes this: there is no edge out of a terminal state. This is what makes fencing monotonic. Once host B holds a higher generation, host A's token is permanently behind, no matter when A resumes. What a stale writer keeps and loses is in fencing and split-brain.

Guarded transitions

The states are only useful if the edges are enforced. The workspace, mount-session, and lease enums each carry a transition predicate that rejects three classes of move: skipping a state, looping on the same state, and leaving a terminal state. The session store calls that predicate before it persists any mount-session move and returns IllegalTransition otherwise. Workspace transitions are checked the same way at the control-plane database; snapshot transitions go through a separate validator.

Guarding transitions turns the spec diagrams into a machine the daemon enforces, not a convention it hopes to honor. The atomic-publication rule depends on it. A checkpoint advances the head in one transaction, or not at all. If the transaction rolls back, the workspace state rolls back with it. A reader never observes a workspace stuck in CHECKPOINTING with a head that already moved.

Recovery is the one path allowed to skip. A stale mount may need to move straight to CLOSED, and the normal "must unmount first" edge does not apply. The store exposes a separate forced-state path for that, used only by reconciliation. The rule is that recovery is the authoritative unmount, not a second front door.

Restart reconciliation

On restart the daemon scans its durable session store and reconciles each local session against the authoritative lease the control plane holds. The recovery classifier assigns each session one verdict:

• Active lease valid — the lease is live, unexpired, and its generation matches. Renew it and resume serving. This is the only verdict that permits publishing.
• Control plane unknown — the mount is live but the control plane holds no matching lease. Preserve the session and its upper. Do not delete, fence, or publish.
• Stale generation — the lease exists but the generation is wrong, the lease is expired, or it is revoked. Fence the session to CLOSED. Never publish.
• Preserved delta — the session is torn down but its upper holds uncommitted data. Preserve it for a bounded host-local recovery window.

The classifier also handles two more checkpoint precedence cases — cleanup incomplete (a checkpoint committed but local cleanup remained) and checkpoint interrupted (a checkpoint was in flight when the host died) — and a final fallthrough, safe to delete (torn down, no delta).

The order is deliberate. Interrupted durable operations take precedence over lease status. The classifier checks for pending checkpoint cleanup and an in-flight checkpoint before it looks at the lease. A half-finished durable checkpoint is more dangerous to abandon than a stale lease, so it is preserved for resume regardless of what the control plane says. Only after those cases does the classifier ask whether the lease still authorizes the session.

The control-plane-unknown verdict carries the strongest invariant. The spec forbids deleting an upper directory merely because the control plane is unreachable. The code enforces it twice. The classifier routes an unknown live mount to a preserve-and-mark-unknown verdict. The live executor then refuses to delete any session whose upper still holds uncommitted data, even if it were routed there. See handle a stale writer and recover from a control-plane outage.

Limits and what is not proven here

Be precise about what the evidence supports.

• The state machines and their transition predicates are unit-tested. The tests cover every legal edge and the rejected skips, self-loops, and terminal exits.
• The recovery classifier is pure policy and is unit-tested for all seven verdicts, including the precedence of interrupted checkpoints over lease status.
• Restart reconciliation is wired into daemon startup. Startup calls the reconcile path against a control-plane lease cache that consults authoritative leases and returns None when the control plane is unreachable.
• Two limits are real. First, the mount path does not yet issue control-plane leases, so no durable session carries a lease_id. On restart every live session resolves to the control-plane-unknown verdict and is preserved. The active-lease and stale-generation paths are exercised in tests, not yet by a live mount. Second, the recovery executor updates durable records, the in-memory session registry, and health counters, but the privileged kernel effects — remount read-only and real OverlayFS teardown — are layered on by the mount component when wired.
• The DEGRADED snapshot state is defined in the code and described in the spec runbooks. It is not drawn in the spec §12.1 diagram, but the control-plane transition validator does model edges to and from it (Ready → Degraded, Degraded → Ready, Degraded → Deleting). Treat it as a repair-driven condition, not a base a new workspace forks from.
• No recorded chaos test restarts a live two-host deployment and observes the stale-generation verdict under a real partition. The recorded measurements cover economics and amplification, not multi-host restart recovery.