Skip to main content

Module fence

car_sync

Module fence 

Source
Expand description

The executor dispatch fence (slice B6 of docs/proposals/multi-device-sync.md, §“Layer 2 (safety): the idempotency / fencing gradient” + §“Deep dive: the execution-lease / fencing protocol”).

B5 shipped deterministic ledger convergence + a durable idempotency oracle and was explicit that this is NOT exactly-once execution:

The exactly-once EXECUTION gate is B6’s dispatch fence — a dispatch-time linearizable “am I still epoch N?” read plus the durable non-fenced oracle read before the external side effect. That is necessary, not an optimization; the fold gates the ledger, not the effect.

This module is that gate. check_dispatch runs the two checks the proposal requires at the point of effect (immediately before the executor performs a side-effecting tool call for a leased run):

  1. The durable non-fenced idempotency read — crate::fold::SyncState::committed_run. This is checked first and is fence-independent: a run that has ever committed (per the keep-all oracle carried in the checkpoint) must never re-execute, whatever the current epoch. This closes the failover-double-run: a new holder that legitimately steals the lease still sees the old holder’s committed record and declines.
  2. The linearizable epoch read — LeaseCoordinator::current. Only a caller that is still the current holder at the epoch it claims may proceed. A stale-epoch zombie (paused past its TTL while another site stole the lease) is rejected here — the Kleppmann fence: a holder that knows it is stale never acts.

The residual the proposal is honest about is unchanged: the fence cannot stop a holder that pauses after passing this check and before its external write lands (the external resource does not honor CAR’s token). That window is bounded by TTL + the write-ahead intent ledger + reversibility, not eliminated — see the proposal’s tier-3 discussion. This module implements the part that IS closeable.

Enums§

FenceDecision
The fence verdict for one dispatch attempt.

Functions§

check_dispatch
Run the dispatch fence for one leased run at the point of effect.