Ownership: the model and its claims

What this is, and what it is not

This repository does not claim that Rust’s borrow checker has been extended across machines. Nothing here is checked at compile time for your application code, no lifetime crosses a network link, and no &mut is transported anywhere.

What this is: a runtime protocol for moving exclusive write authority over an actor (named by an Id) between nodes, together with machine-checked proofs that the protocol’s exclusivity and fencing properties hold in every reachable state, including under crashes, partitions, duplicated messages and interrupted handovers.

The analogy to Rust is about the shape of the guarantee, not the mechanism. Rust’s &mut T is exclusive because the compiler refuses to create a second one. Here, authority is exclusive because may_mutate is only ever true in one shape - the actor is Owned, the caller is the owner, and the caller’s fencing epoch is exactly the actor’s current epoch - and because the protocol’s transitions provably keep it that way.

The core of this repository is a model, and the proofs are about the model. Each algorithm also has a service over Jetstream RPC, which runs the verified step functions; what those services do and do not claim is stated in The protocol as a Jetstream service and in each module’s docs.

Relation to Chubby

The obvious prior art is The Chubby lock service for loosely-coupled distributed systems (Burrows, OSDI 2006). It is worth being precise about the relationship, because the central mechanism here is Chubby’s, not a new one.

The fencing mechanism is the same idea. Chubby §2.4: a lock holder may request a sequencer, “an opaque byte-string that describes the state of the lock immediately after acquisition”, containing the lock name, the mode, and the lock generation number — a per-node counter that “increases when the node’s lock transitions from free to held”. The client passes it to the resource server, which “is expected to test whether the sequencer is still valid … if not, it should reject the request”. That is exactly Token { actor, epoch, holder } plus valid_fence, and Chubby’s lock generation number is this model’s Epoch. This repository is a formalisation of that design, not an alternative to it.

What this adds is the proof, and the precision that a proof forces. Chubby is an experience paper: it describes the initial design, compares it with actual use, and explains how the design had to change. It carries no machine-checked proofs, and it does not need to — its evidence is years of production at scale. The evidence here is different in kind. “The recipient server is expected to test whether the sequencer is still valid” is doing a great deal of work in that sentence, and writing the obligation down as a state machine is what turns it into something checkable:

• who may mutate is a single predicate, may_mutate, and theorem_no_authority_without_token proves that anyone who satisfies it provably holds an issued token for exactly that (actor, epoch);
• the headline scenario — A owns at 41, B takes over at 42, A returns still holding its epoch-41 token — is the situation sequencers exist for, and it is discharged as a nine-step execution rather than argued informally;
• the awkward part, a node cannot fence itself, becomes impossible to leave implicit. FenceGuard::accepts consults the node’s own belief, so a partitioned holder accepts its own stale epoch; the rejection that matters happens where the effect lands. Chubby’s locks are advisory for exactly this reason — “holding a lock called F neither is necessary to access the file F, nor prevents other clients from doing so” — and this model is advisory in the same sense, but has to say so in a proof obligation rather than in prose.

Three deliberate differences, and why.

The third difference is where this model has something Chubby does not, and it is also where it was recently found to be wrong. Because privilege moves between peers rather than being held centrally, a node can be left believing it holds the privilege after the privilege has moved. Chubby handles the corresponding case by checking a sequencer “against the server’s Chubby cache or … the most recent sequencer that the server has observed” — belief is checked against authority. This model originally had no such split on the routing side and resolved a seizure by editing the absent node’s state, which no implementation can do; see The holder graph is a tree and the believes_holds / has_token split in src/raymond/model_t.rs.

What Chubby has that this does not: a deployed system, sessions and KeepAlives, failover, caching with invalidations, a filesystem namespace, ACLs, events, and liveness of any kind. This model proves safety only, and says so.

The state machine

#![allow(unused)]
fn main() {
// Id is `crate::id::Id`, a newtype around a `u128` (a UUID or a ULID converts to one);
// a model names a host, and an actor, by it directly. (An actor was a `nat` here
// before; the theorems now quantify over the `u128` actors a host always was, not
// over unbounded ones. No theorem relied on there being more.)
pub type Epoch   = nat;

pub enum OwnershipState {
    Owned        { owner: Id, epoch: Epoch },
    Transferring { from: Id, to: Id, old_epoch: Epoch, new_epoch: Epoch },
    Unowned      { epoch: Epoch, intended_owner: Id },
}
}

Ownership never moves atomically. A handover is four protocol transitions:

Owned(A, 41)
      |  BeginTransfer(A -> B)         epoch 42 is allocated here
Transferring(A, B, 41, 42)
      |  CompleteRelease
Unowned(42, B)
      |  Acquire(B)
Owned(B, 42)

Two deliberate design points:

• The epoch advances at the start of a handover, not at the end. From the moment A agrees to transfer, current_epoch is 42, so A’s epoch-41 authority is already fenced out. A does not have to be reachable, or even alive, for this to take effect.
• During the two middle stages nobody has authority at all. That is the trade this design makes: it gives up availability during a handover so that double ownership is not representable. It is acceptable for neither node to have mutable authority during a transfer; it is never acceptable for both to.

The two specification functions

#![allow(unused)]
fn main() {
// Who may perform an authoritative mutation.
spec fn may_mutate(s: OwnershipState, node: Id, epoch: Epoch) -> bool {
    match s {
        Owned { owner, epoch: e } => node == owner && epoch == e,
        Transferring { .. }       => false,
        Unowned { .. }            => false,
    }
}

// The fence check a server performs on an incoming request.
spec fn valid_fence(s: OwnershipState, e: Epoch) -> bool { e >= current_epoch(s) }
}

current_epoch reports new_epoch while Transferring, which is what makes the outgoing owner stale immediately.

Capability tokens

A Token { actor, epoch, holder } is a physical artifact. It can be copied, it survives a crash, and a node that was partitioned away for an hour can come back still clutching one. The model reflects that: System::issued is the set of every token ever issued and it never shrinks.

Whether a token confers authority is a completely separate question, answered by token_authorized, which consults the actor’s current state. Stale physical tokens exist; they are inert.

Failure model

These are the assumptions the proofs rest on. They are part of the system model, not hidden side conditions.

What is not claimed: liveness. Nothing here says a transfer completes, that a request is eventually served, or that an actor ever becomes owned again. Under arbitrary crashes and partitions none of those are achievable anyway. Safety survives every case above; progress does not, and is treated separately.

Claimed invariants and the proofs that establish them

Every row names a proof fn that Verus checks in CI. If a row’s proof stops verifying, the build fails.

“Reachability” means the hypothesis reachable(sys), i.e. some finite execution starting from an init state ends in sys. It is discharged once and for all by theorem_reachable_inv.

Privilege movement is partitioned by cooperation

A holder that acts hands the privilege on (ComposedStep::PassToken, which requires pre.own.live.contains(n) and believes_holds); a holder that does not has it taken (ComposedStep::SeizeToken). composed::proofs::coupling::theorem_token_movement_is_partitioned proves there is no third way: routing steps, ownership transitions, acquisition and reconciliation all leave possession exactly as they found it.

The SeizeToken arm used to claim !pre.own.live.contains(m) as well, because seizure was guarded on it. It no longer is, and the arm now says only what is true and checkable: the privilege moved away from m without m taking a step. That is the distinction a deployment can act on — a coordinator knows whether it is forcing the transfer; it does not know whether the node is alive. See Seizure needs no oracle.

The liveness guard on PassToken stays, and means something different: it is not a detection requirement but a statement about who is acting. ray_assign_privilege models the holder choosing to hand the privilege to the head of its queue, and a crashed node cannot choose anything.

A seized node must reconcile before it returns

A seizure leaves the seized node’s holder and using entries exactly as they were — nobody can reach into a machine that is down — and Step::Recover’s contract says a node comes back with no knowledge of what happened meanwhile. So a node that is simply allowed to recover comes back still believing holder[n] == n, and can enter its Raymond critical section beside the new holder. Ownership stays safe, because the epoch fences it; Raymond’s critical section has no epoch.

So Composed carries seized, the set of nodes whose privilege was taken and whose belief has not yet been repaired, and composed_inv ties it to reality: every stale holder owes a reconciliation. cs_own refuses Step::Recover for a node in that set, and ComposedStep::Reconcile is the only way out.

The reconciliation a real deployment must perform — re-read the routing state rather than trust what you remember — is therefore a modelled transition with content, not a marker: it is the step in which the belief is dropped, the critical section left, and the holder pointer re-aimed at the node that actually holds the privilege. scenario_composed_crash_takeover runs it through to A rejoining afterwards, so the guard is a discipline rather than an unreachable restriction.

It is not guarded on the node being down. Seizure is no longer restricted to crashed nodes, so a live node can be left stale by a coordinator that suspected it wrongly, and must be able to learn the truth too. What the ordering rule still enforces is the crashed case: you cannot come back and start acting on a belief you never corrected.

Seizure needs no oracle: belief versus authority

An earlier version of this model guarded ComposedStep::SeizeToken on !pre.own.live.contains(from), with this argument: RevokeOwner may fire against a perfectly healthy owner, so without a liveness guard a seizure could fire against a live node inside its Raymond critical section; ray_seize clears using[from], so the model would report exclusivity while two nodes were really inside.

The analysis was right and the conclusion was wrong, twice over.

It conflated two guarantees. Ownership safety is fenced by the epoch, which is burned before the seizure fires, so it never needed the node to be dead. Only Raymond’s critical-section exclusivity needed anything, and what it needs is a condition on the state — ray_no_stale_holders — not a guard on the step. The difference matters: a state condition is something a deployment can restore, by reconciling; a step guard is something it must evaluate.

And !live is ground truth, which no coordinator has. It has a suspicion — which is exactly why RevokeOwner is modelled as firing against healthy nodes. Guarding the forcible path on perfect failure detection put the composed machine’s strongest theorems out of reach of any real deployment, in a clause that read like an ordinary guard.

The repair was the one the ownership layer had already made once. issued keeps a crashed node’s capability for ever and token_authorized decides whether it still confers anything; the routing layer now makes the same split:

ray_seize now touches only the new holder. from’s holder, using and asked entries are left exactly as they are, because they live on a machine nobody can reach — editing them was modelling something no implementation can do. What that creates is a stale holder: a node that believes it holds the privilege, does not, and may still be inside its critical section believing that too.

That state is the point. It could not previously be written down, because ray_unique_token was an inductive invariant over the holder pointers and the state violated it outright — the invariant held partly because the dangerous state was unrepresentable, which is the pattern the ownership layer takes such care to avoid. Uniqueness is now structural (privilege is one value), the stale state is representable, and theorem_stale_holder_confers_no_authority proves it inert: couples is written against possession, so belief confers nothing however firm it is.

The rule this leaves behind. Not all liveness guards are oracles, and the difference is which node the step makes act:

Liveness may guard the nodes a step makes act, and may not guard the ones it does not.

A guard on an acting node is a statement about who takes part — nobody has to determine anything, because if the node is down the exchange simply does not happen. A guard on a non-acting node is an oracle, because something must evaluate it before the step may fire. !live(from) was the second kind, which is why it had to go; live(n) on cs_pass_token was always the first kind.

Applying the rule uniformly closed two more holes of exactly the shape the review found, on the receiving side:

• cs_pass_token now guards head as well as n. ray_assign_privilege has head record holder[head] := head, so if head crashed after its request reached n, the old step installed a belief in a node that could not receive it — and a later Recover(head) framed it in, modelling the node as knowing about an event it never observed.
• cs_seize_token guards to for the same reason: the coordinator hands it the privilege and it records that, so it is acting.

The rule covers the ownership layer too, and enumerating it there found the last gap: tr_begin_transfer is documented as “the current owner agrees to hand actor over”, which is an action by from, and it had no liveness guard. So Acquire(A) → Crash(A) → BeginTransfer(A, B) was accepted — a crashed node volunteering. That one matters beyond tidiness: RevokeOwner and SeizeToken exist precisely for the case where the owner cannot cooperate, and a model in which the dead cooperate does not need them.

The full audit, by who acts:

That is all twelve variants of Step, which is the point: a table that omits one cannot support a coverage argument, however right the rows it does contain are. This one omitted ReassignUnowned and Stutter when first published.

RevokeOwner being unguarded is the design, not an oversight: it is the step that fires without the owner’s cooperation, against a node that may be perfectly healthy. ReassignUnowned is the same shape — the coordinator re-offering an actor that nobody owns, burning an epoch to do it.

cs_ray guards whichever node the Raymond step makes act (ray_step_actor), which is the carrier that has most of them. Without it a crashed node could queue requests, forward them, and — the serious case — enter its critical section: after Crash(A) → RevokeOwner → SeizeToken(A, B), Ray { EnterCs(A) } fired on A’s untouched holder and queue while A was still down and still marked, walking straight past the reconciliation-before-acting discipline. ReceiveRequest acts at at; from sent its request earlier and takes no part in the delivery.

cs_reconcile guards nobody, and that is not an exception to the rule but a consequence of what live means here. live is participating in the protocol, not powered on — the field’s documentation said “currently up” until this was chased down, which was a second meaning hiding in one set. Reconciliation is the boundary step — the node re-reading authoritative state as part of coming back, before it resumes participating — which is why it may fire while !live and why Recover is a separate step that follows it. A node that was seized while live may also reconcile at any time, since it is acting either way.

Granting the privilege discharges the debt. Both grant steps now clear the recipient from seized, because receiving the privilege is the node learning the truth: it is live, it records holder := itself, and it really does hold, so its belief is correct again. Without that, a node marked by an earlier seizure and later handed the privilege back would stop being stale while staying marked — and cs_reconcile requires is_stale_holder, so the marker could never be cleared and recovers_a_seized_node would reject that node’s recovery for ever.

That state became reachable only when the !live(from) guard came off. Before, a marked node was always dead and had to reconcile before rejoining, so it could never be a live grant target; afterwards it can be. A guard removed for good reasons opened a path that had to be closed somewhere else.

Three consequences worth stating plainly:

• cs_seize_token has no liveness guard at all. Ownership safety survives seizure from a node that is perfectly healthy and wrongly suspected, which is the case a deployment will actually hit.
• Raymond’s mutual exclusion has a window. Between a seizure and the seized node’s reconciliation, two nodes can be inside their critical sections. That is true of any system that takes a privilege away from a node it cannot reach, and the model now says so instead of hiding it.
• cs_reconcile acquired its content. It used to remove a marker and change nothing else; the work it claimed to model had already been done at seizure time, by the coordinator, to a node it could not talk to. Now it is where the belief is dropped — by the node that holds it.

Chubby reaches the same place from the other direction: a sequencer’s validity is checked “against the server’s Chubby cache or … the most recent sequencer that the server has observed”, which is belief checked against authority. See Relation to Chubby.

A node cannot fence itself

Row E is narrower than it looks, and the gap is worth stating plainly rather than leaving a reader to infer it.

FenceGuard::accepts consults the node’s own belief about the actor — whatever generation it last observed. A partitioned A still holding FenceGuard::new(A, 41) gets accepts(A, 41) == true while the system has already moved to Owned { B, 42 }. The stale owner from the headline scenario passes its own fence, every time.

That is not a contradiction: the postcondition promises may_mutate(self.view(), ..), and view() is exactly that stale belief. But the safety property proved here is about the system’s state (can_mutate(sys, ..)), and nothing in src/ownership/exec_v.rs connects a guard to it. What a guard buys is node-local staleness rejection, not fencing.

Real fencing has to happen where the effect lands, against authoritative state: the storage layer refusing a write whose epoch is superseded, or a reply gate that re-reads the ownership record after a write is durable and before acknowledging it, refusing the acknowledgement if the record no longer names this node at this epoch. That check is what turns exclusivity into a property an outsider can rely on. It is not in this crate, and proving the protocol says nothing about whether an implementation performs it.