The per-node agent (design §5.2, implementation.md §4): a :gen_statem
running join/leave, the lease-renewal loop, self-fencing, and the
routing-table cache writer.
States: :joining → :active → :leaving → :stopped, plus :fenced,
reachable from any serving state (:joining, :active, :leaving).
Clock discipline (design §6.4)
- The lease basis is send-time:
t = Fief.Seam.monotonic_time()is captured before every acquire/renew call; on successt— never ack time — becomes the basis (fence_delay/4is the one pure function that turns a basis into a fence deadline). - One fence timer is armed at
basis + ttl − margin, re-armed from each new basis. If it ever fires, the node transitions to:fencedunilaterally — no network, no reads. {:error, :unreachable}from a renew keeps the fence timer running and keeps retrying at the renewal cadence (the fence clock is already ticking).{:error, :expired}fences NOW.margindefaults to:auto= renewal-RTT budget + 2× clock-drift bound (auto_margin/2); the 2× is model-checked inspecs/FiefLease.tla— the 1× margin has a TLC counterexample.
Every deadline here is a Fief.Seam.send_after/2 seam timer arriving as
handle_event(:info, {:timeout, ref, msg}, ...). No gen_statem native
timeouts, ever (the no-raw-timers rule, implementation.md §10).
Fencing
Fencing is a kill, not a request (implementation.md §2). In M3 there is no
serving subtree yet, so the kill is the :fence_action seam: an internal
instance opt (fn reason -> ... end or {mod, fun, args}, invoked as
apply(mod, fun, args ++ [reason]), default no-op) executed exactly
once per fencing, on the transition into :fenced. M4 points it at the
Fief.Vnode.Manager brutal-kill in one line. A crashed Fief.Node fences
by supervision instead: rest_for_one tears down and restarts everything
after it through the join path (a restarting node finds its own lease
:held and renews it — same lease, fresh send-time basis).
Published state — an ETS read, not a call
Fief.Node is the only writer of the instance's routing cache (the table is
owned by Fief.Router.Cache so it survives a Fief.Node restart). It
publishes {owned vnodes, epoch, lease_live?, state} as the :node_status
row of the same table; status/1 / owned_vnodes/1 are plain :ets.lookup
so the receive path never blocks on this process. Cache refresh triggers:
the periodic poll (seam timer), explicit refresh/1, {:fief_moved_delta, delta} handed up by Fief.Router callers bouncing off :moved, and
{:fief_presence, ...} hints (implementation.md §4). Hints accelerate,
never authorize: a delta or presence message only triggers an authoritative
re-read — its contents are never written to the cache. (Presence
subscription wiring — who sends those hints in production — arrives with
the Presence adapters at M7; under simulation, hints are scripted
deliveries.)
Leave drain (M4 phase B, design §6.2)
:leaving completes only when this node appears as neither owner nor
prev_owner for any vnode: each :finish_leave seam timer refreshes,
reconciles (so donor agents run their handoffs), and either finishes the
leave (release lease → :stopped) or re-arms at leave_drain_interval.
The planner drains :leaving members; a dead-planner fallback (leave
proceeding after the lease would have expired anyway) is an M7+ operational
concern, deliberately out of scope here.
After every refresh this process synchronously calls
Fief.Vnode.Manager.reconcile/1 (a no-op when the instance runs no vnode
impl), so agent starts/stops/handoffs complete before the triggering event
finishes processing — under simulation, one stepped refresh is one complete
reconciliation, with no unscripted concurrency. The call chain is strictly
downward (Node → Manager → Agent → Authority); agents never call back into
this process (their reads are ETS-only), so no cycle exists.
The checkpoint pattern (THE pattern M4+ process modules copy)
A single handle_event/4 entry point delegates to private handle/4
clauses and marks end-of-processing with the reserved :handled checkpoint
on every path — including raises — via the implicit try/after. Two rules
keep it sound:
- No
:next_eventactions. An inserted event would run after the checkpoint already settled the delivery, letting virtual time advance mid-processing. Multi-step transitions use 0 ms seam timers instead (:activate,:finish_leave), which are scripted schedule points under simulation and immediate in real builds. - Reply actions are sent by gen_statem after the checkpoint; that is fine
because callers (
leave/1,refresh/1) are never scheduler-gated deliveries.
Deadlock note (simulation)
Renew/CAS calls are GenServer.calls to the authority from inside
handle/4. Under simulation Fief.Authority.Local's calls are not
scheduler-gated — only queue deliveries are — and the scheduler itself never
blocks (quiescence-gated ops defer their reply instead of blocking its
loop), so mid-handler authority calls and timer (re-)arming are always
served while a step/advance waits on this process's :handled
checkpoint. No cycle exists.
Summary
Functions
The :auto margin (design §9, §6.4): renewal round-trip budget plus
twice the clock-drift bound. Twice, not once: drift can swing from one
extreme to the other across the measurement interval, so local elapsed time
can lag real elapsed time by 2× the bound — model-checked in
specs/FiefLease.tla; specs/FiefLease_thinmargin.cfg is the 1×
counterexample.
Milliseconds until the fence deadline for a lease whose last confirmed
renewal was sent at basis (local monotonic ms): the node must be inert
at basis + ttl − margin on its own clock (design §6.4). Clamped at 0.
Send-time is what makes this conservative — an ack-time basis would credit
the renewal round-trip to the lease and fence too late.
Graceful leave (design §6.2, M3 scope): sets status leaving in the
Authority, releases the lease, transitions to :stopped. The planner-driven
drain (holding :leaving open until the node is neither owner nor
prev_owner anywhere) arrives with M4.
The vnodes this node currently owns, from published state. ETS read.
Explicitly refresh the routing-table cache from the Authority.
Resolve the effective margin from instance opts: lease_margin: an explicit
positive integer, or :auto (default) = auto_margin/2 over the
:renew_rtt_budget (100 ms) and :clock_drift_bound
(50 ms) budgets.
The node's published state — an ETS read, never a call (implementation.md
§4): {:ok, %{node_id:, owned:, epoch:, lease_live?:, state:}}. owned is
derived from the cached table (empty in M3 unless a test assigns vnodes);
lease_live? is the node's own belief, updated on lease events — it flips
false on :fenced/:stopped.
Functions
@spec auto_margin(non_neg_integer(), non_neg_integer()) :: pos_integer()
The :auto margin (design §9, §6.4): renewal round-trip budget plus
twice the clock-drift bound. Twice, not once: drift can swing from one
extreme to the other across the measurement interval, so local elapsed time
can lag real elapsed time by 2× the bound — model-checked in
specs/FiefLease.tla; specs/FiefLease_thinmargin.cfg is the 1×
counterexample.
@spec fence_delay(integer(), pos_integer(), pos_integer(), integer()) :: non_neg_integer()
Milliseconds until the fence deadline for a lease whose last confirmed
renewal was sent at basis (local monotonic ms): the node must be inert
at basis + ttl − margin on its own clock (design §6.4). Clamped at 0.
Send-time is what makes this conservative — an ack-time basis would credit
the renewal round-trip to the lease and fence too late.
Graceful leave (design §6.2, M3 scope): sets status leaving in the
Authority, releases the lease, transitions to :stopped. The planner-driven
drain (holding :leaving open until the node is neither owner nor
prev_owner anywhere) arrives with M4.
@spec owned_vnodes(atom()) :: {:ok, [non_neg_integer()]} | {:error, term()}
The vnodes this node currently owns, from published state. ETS read.
@spec refresh(atom()) :: :ok | {:error, :not_serving}
Explicitly refresh the routing-table cache from the Authority.
@spec resolve_margin(keyword()) :: pos_integer()
Resolve the effective margin from instance opts: lease_margin: an explicit
positive integer, or :auto (default) = auto_margin/2 over the
:renew_rtt_budget (100 ms) and :clock_drift_bound
(50 ms) budgets.
The node's published state — an ETS read, never a call (implementation.md
§4): {:ok, %{node_id:, owned:, epoch:, lease_live?:, state:}}. owned is
derived from the cached table (empty in M3 unless a test assigns vnodes);
lease_live? is the node's own belief, updated on lease events — it flips
false on :fenced/:stopped.