ms2k/remora
SHA256
Watch
0
Code Releases Activity

Strengthen JobProtocol model after independent review.

Browse source 
Replace tautological invariants with non-trivial ones, allow multi-shot
coordination loss and re-partition, fix reap/progress lifecycle, enable
deadlock checking via Done, and add stress and multi-shot TLC configs.
This commit is contained in:
ms2k 2026-07-10 12:43:32 +09:00
commit 7d490194c3
10 changed files with 342 additions and 124 deletions
Download patch file Download diff file Expand all files Collapse all files

20
docs/protocol/Remora.cfg
View file

@ -1,8 +1,10 @@
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Fault/recovery and temporal-property configuration.
\* Fair Spec + liveness under coordination faults. Fault budgets are 1 so
\* temporal checking finishes in minutes; multi-shot budgets are covered by
\* RemoraMultiShot.cfg (safety-only).
CONSTANTS
Jobs = {j1}
Workers = {w1, w2}
@ -16,24 +18,26 @@ CONSTANTS
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Coordination"}
MaxCoordLosses = 1
MaxPartitions = 1
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable
FencingTokensMonotonic
CommitIsFencedCAS
AtLeastOnceDelivery
EventuallyDispatched
EventuallyReaped
EventuallyTerminal

279
docs/protocol/Remora.tla
View file

@ -1,18 +1,33 @@
------------------------------ MODULE Remora ------------------------------
EXTENDS Naturals, FiniteSets, TLC
\* Implementation-level distributed job protocol.
\* JobProtocol: distributed job coordination for Remora (see docs/spec/architecture.md).
\*
\* Durable variables are authoritative PostgreSQL state. Coordination
\* variables are reconstructible Dragonfly state. Attempts remain observable
\* after losing authority, so delayed requests and zombie target writes are
\* checked. Target writes use an attempt-specific staging identity; only the
\* durable AcceptSuccess compare-and-swap publishes a result.
\* DurableStore variables are sole authority for phase, cancellation, attempt
\* allocation, fencing tokens, and committed results. CoordinationStore variables
\* are reconstructible: queues, reservations, leases, cancel notices, live progress.
\* Attempts remain observable after losing authority so delayed outcomes and zombie
\* target writes are checked. Each attempt uses an attempt-specific staging identity;
\* only the durable AcceptSuccess compare-and-swap publishes a CommittedResult.
\*
\* Abstractions and bounds:
\* - Jobs in Init are already durably accepted (submission outbox precedes queueing).
\* - Reconciler projection (Enqueue, PublishCancelNotice, CleanTerminalCoordination)
\* is ambient: it models a daemon with CoordinationStore access independent of
\* per-worker links. Worker-facing coord ops still require CanReach(w, CoordSvc).
\* - MaxCoordLosses bounds full CoordinationStore wipes; MaxPartitions bounds
\* DropLink events (re-partition of LinkUp or LinkRecovered is allowed within budget).
\* - Worker ids are incarnations: WorkerUnused -> WorkerUp is scale-up/restart;
\* WorkerDown is permanent for that id. CrashWorker will not crash the last
\* remaining Up/Unused incarnation so safety models stay free of total capacity loss.
\* - Opaque attempt ids refine to <<job, token>>; tokens are dense and never reused.
\* - CHECK_DEADLOCK expects Done when the system is protocol-quiescent.
CONSTANTS
Jobs, Workers, InitialWorkers, NoJob, NoWorker,
MaxAttempts, MaxProgress, LeaseLimit,
LocalLimit, GlobalLimit, FaultsEnabled, FaultServices
LocalLimit, GlobalLimit, FaultsEnabled, FaultServices,
MaxCoordLosses, MaxPartitions
ASSUME /\ Jobs # {}
/\ Workers # {}
@ -25,6 +40,8 @@ ASSUME /\ Jobs # {}
/\ GlobalLimit \in Nat \ {0}
/\ FaultsEnabled \in BOOLEAN
/\ FaultServices \subseteq {"Coordination", "Durable", "Target"}
/\ MaxCoordLosses \in Nat
/\ MaxPartitions \in Nat
/\ NoJob \notin Jobs
/\ NoWorker \notin Workers
@ -79,8 +96,6 @@ OutcomeRequests == {NoOutcome, WantsSuccess, WantsFailure}
NoAttempt == [job |-> NoJob, token |-> 0]
\* Implementations use opaque attempt IDs. The bounded model canonically uses
\* <<job, token>>; the token is strictly increasing and never reused per job.
AttemptIds ==
{[job |-> j, token |-> token] :
j \in Jobs, token \in 1..MaxAttempts}
@ -89,18 +104,18 @@ JobOf(a) == a.job
TokenOf(a) == a.token
VARIABLES
\* Authoritative durable state.
\* DurableStore authority.
phase, cancelRequested, currentToken, authority, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid,
\* Reconstructible coordination state.
\* CoordinationStore (reconstructible).
queued, reservation, leaseState, leaseAge, cancelNotice,
liveProgress, liveProgressAttempt, coordinationLostOnce,
liveProgress, liveProgressAttempt, coordLossCount,
\* Worker incarnations and service-specific connectivity.
workerState, links,
\* Worker incarnations, per-service links, partition budget.
workerState, links, partitionCount,
\* Explicit attempts, staging, and delayed outcome requests.
\* Attempts, staging, delayed outcome requests.
attemptState, attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome
@ -109,8 +124,8 @@ durableVars ==
committedAttempt, checkpoint, checkpointValid>>
coordinationVars ==
<<queued, reservation, leaseState, leaseAge, cancelNotice,
liveProgress, liveProgressAttempt, coordinationLostOnce>>
workerVars == <<workerState, links>>
liveProgress, liveProgressAttempt, coordLossCount>>
workerVars == <<workerState, links, partitionCount>>
attemptVars ==
<<attemptState, attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>>
@ -135,8 +150,29 @@ CapacityAvailable(w) ==
/\ Cardinality(ReservedJobs) + Cardinality(LiveLeases) < GlobalLimit
/\ Cardinality(ReservedFor(w)) + Cardinality(ExecutingFor(w)) < LocalLimit
OtherCapacity(w) ==
\E w2 \in Workers :
/\ w2 # w
/\ workerState[w2] \in {WorkerUp, WorkerUnused}
CoordinationClean(j) ==
/\ ~queued[j]
/\ reservation[j] = NoWorker
/\ ~cancelNotice[j]
/\ liveProgress[j] = 0
/\ liveProgressAttempt[j] = NoAttempt
\* No in-flight protocol work and no uncommitted staging left to clean.
SystemQuiescent ==
/\ \A j \in Jobs : Terminal(j) /\ CoordinationClean(j)
/\ \A a \in AttemptIds :
/\ leaseState[a] # LeaseLive
/\ pendingOutcome[a] = NoOutcome
/\ attemptState[a] \notin {AttemptAuthorized, AttemptExecuting}
/\ (stageState[a] \in {StagePartial, StageComplete} =>
committedAttempt[JobOf(a)] = a)
Init ==
\* Jobs denotes accepted durable submissions. The outbox precedes queueing.
/\ phase = [j \in Jobs |-> Queued]
/\ cancelRequested = [j \in Jobs |-> FALSE]
/\ currentToken = [j \in Jobs |-> 0]
@ -152,11 +188,12 @@ Init ==
/\ cancelNotice = [j \in Jobs |-> FALSE]
/\ liveProgress = [j \in Jobs |-> 0]
/\ liveProgressAttempt = [j \in Jobs |-> NoAttempt]
/\ coordinationLostOnce = FALSE
/\ coordLossCount = 0
/\ workerState =
[w \in Workers |->
IF w \in InitialWorkers THEN WorkerUp ELSE WorkerUnused]
/\ links = [w \in Workers |-> [s \in Services |-> LinkUp]]
/\ partitionCount = 0
/\ attemptState = [a \in AttemptIds |-> AttemptUnused]
/\ attemptWorker = [a \in AttemptIds |-> NoWorker]
/\ attemptProgress = [a \in AttemptIds |-> 0]
@ -165,7 +202,7 @@ Init ==
/\ stageState = [a \in AttemptIds |-> StageNone]
/\ pendingOutcome = [a \in AttemptIds |-> NoOutcome]
\* Durable outbox projection. Duplicate dispatch is idempotent.
\* Ambient reconciler: projects durable dispatch into CoordinationStore.
Enqueue(j) ==
/\ phase[j] = Queued
/\ dispatchNeeded[j]
@ -174,11 +211,10 @@ Enqueue(j) ==
/\ queued' = [queued EXCEPT ![j] = TRUE]
/\ UNCHANGED durableVars
/\ UNCHANGED <<reservation, leaseState, leaseAge, cancelNotice,
liveProgress, liveProgressAttempt, coordinationLostOnce>>
liveProgress, liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Coordination atomically reserves a logical permit. It is not authority.
Reserve(j, w) ==
/\ queued[j]
/\ reservation[j] = NoWorker
@ -189,12 +225,11 @@ Reserve(j, w) ==
/\ reservation' = [reservation EXCEPT ![j] = w]
/\ UNCHANGED durableVars
/\ UNCHANGED <<leaseState, leaseAge, cancelNotice, liveProgress,
liveProgressAttempt, coordinationLostOnce>>
liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Durable CAS: allocate the next attempt and token. This claim linearization
\* point consumes retry budget even if the worker is lost before execution.
\* Durable CAS: next attempt and fencing token; consumes retry budget.
AuthorizeAttempt(j, w) ==
LET a == AttemptId(j, currentToken[j] + 1)
IN /\ phase[j] = Queued
@ -231,7 +266,6 @@ AuthorizeAttempt(j, w) ==
/\ UNCHANGED workerVars
/\ UNCHANGED pendingOutcome
\* Coordination converts the reservation to a renewable lease and execution.
ActivateAttempt(a) ==
LET j == JobOf(a)
w == attemptWorker[a]
@ -249,7 +283,7 @@ ActivateAttempt(a) ==
[liveProgressAttempt EXCEPT ![j] = a]
/\ attemptState' = [attemptState EXCEPT ![a] = AttemptExecuting]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, cancelNotice, coordinationLostOnce>>
/\ UNCHANGED <<queued, cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>>
@ -263,11 +297,10 @@ RenewLease(a) ==
/\ leaseAge' = [leaseAge EXCEPT ![a] = 0]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, leaseState, cancelNotice,
liveProgress, liveProgressAttempt, coordinationLostOnce>>
liveProgress, liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Real durations refine this bounded logical age.
Tick ==
/\ \E a \in AttemptIds :
leaseState[a] = LeaseLive /\ leaseAge[a] < LeaseLimit
@ -277,7 +310,7 @@ Tick ==
THEN leaseAge[a] + 1 ELSE leaseAge[a]]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, leaseState, cancelNotice,
liveProgress, liveProgressAttempt, coordinationLostOnce>>
liveProgress, liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
@ -294,16 +327,15 @@ ExpireLease(a) ==
[liveProgressAttempt EXCEPT
![j] = IF @ = a THEN NoAttempt ELSE @]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, cancelNotice,
coordinationLostOnce>>
/\ UNCHANGED <<queued, reservation, cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Failover erases ephemeral state but leaves durable state and processes.
\* Full CoordinationStore wipe; durable authority and processes unchanged.
LoseCoordinationState ==
/\ FaultsEnabled
/\ CoordSvc \in FaultServices
/\ ~coordinationLostOnce
/\ coordLossCount < MaxCoordLosses
/\ queued' = [j \in Jobs |-> FALSE]
/\ reservation' = [j \in Jobs |-> NoWorker]
/\ leaseState' =
@ -314,17 +346,20 @@ LoseCoordinationState ==
/\ cancelNotice' = [j \in Jobs |-> FALSE]
/\ liveProgress' = [j \in Jobs |-> 0]
/\ liveProgressAttempt' = [j \in Jobs |-> NoAttempt]
/\ coordinationLostOnce' = TRUE
/\ coordLossCount' = coordLossCount + 1
/\ UNCHANGED durableVars
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Re-partition allowed from recovered links until MaxPartitions is reached.
DropLink(w, service) ==
/\ FaultsEnabled
/\ service \in FaultServices
/\ workerState[w] = WorkerUp
/\ links[w][service] = LinkUp
/\ links[w][service] \in {LinkUp, LinkRecovered}
/\ partitionCount < MaxPartitions
/\ links' = [links EXCEPT ![w][service] = LinkDown]
/\ partitionCount' = partitionCount + 1
/\ UNCHANGED durableVars
/\ UNCHANGED coordinationVars
/\ UNCHANGED workerState
@ -336,30 +371,44 @@ RestoreLink(w, service) ==
/\ UNCHANGED durableVars
/\ UNCHANGED coordinationVars
/\ UNCHANGED workerState
/\ UNCHANGED partitionCount
/\ UNCHANGED attemptVars
CrashWorker(w) ==
/\ FaultsEnabled
/\ workerState[w] = WorkerUp
/\ OtherCapacity(w)
/\ workerState' = [workerState EXCEPT ![w] = WorkerDown]
/\ attemptState' =
[a \in AttemptIds |->
IF attemptWorker[a] = w
/\ attemptState[a] \in {AttemptAuthorized, AttemptExecuting}
THEN AttemptStopped ELSE attemptState[a]]
/\ liveProgress' =
[j \in Jobs |->
IF liveProgressAttempt[j] # NoAttempt
/\ attemptWorker[liveProgressAttempt[j]] = w
THEN 0 ELSE liveProgress[j]]
/\ liveProgressAttempt' =
[j \in Jobs |->
IF liveProgressAttempt[j] # NoAttempt
/\ attemptWorker[liveProgressAttempt[j]] = w
THEN NoAttempt ELSE liveProgressAttempt[j]]
/\ UNCHANGED durableVars
/\ UNCHANGED coordinationVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED links
/\ UNCHANGED partitionCount
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>>
\* An unused element denotes a fresh incarnation or scale-up, never reuse.
StartIncarnation(w) ==
/\ workerState[w] = WorkerUnused
/\ workerState' = [workerState EXCEPT ![w] = WorkerUp]
/\ UNCHANGED durableVars
/\ UNCHANGED coordinationVars
/\ UNCHANGED links
/\ UNCHANGED partitionCount
/\ UNCHANGED attemptVars
ReleaseReservation(j) ==
@ -373,11 +422,12 @@ ReleaseReservation(j) ==
/\ reservation' = [reservation EXCEPT ![j] = NoWorker]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, leaseState, leaseAge, cancelNotice,
liveProgress, liveProgressAttempt, coordinationLostOnce>>
liveProgress, liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Reaping revokes durable authority but does not stop a zombie process.
\* Revoke durable authority; stop authorized-never-activated attempts so staging
\* can clean. Executing attempts become zombies until CooperativeStop.
ReapLostAttempt(a) ==
LET j == JobOf(a)
IN /\ CurrentAuthority(a)
@ -390,11 +440,23 @@ ReapLostAttempt(a) ==
![j] = IF currentToken[j] < MaxAttempts
THEN RetryWait ELSE Failed]
/\ authority' = [authority EXCEPT ![j] = NoAttempt]
/\ attemptState' =
[attemptState EXCEPT
![a] = IF attemptState[a] = AttemptAuthorized
THEN AttemptStopped ELSE @]
/\ liveProgress' =
[liveProgress EXCEPT
![j] = IF liveProgressAttempt[j] = a THEN 0 ELSE @]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT
![j] = IF @ = a THEN NoAttempt ELSE @]
/\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid>>
/\ UNCHANGED coordinationVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>>
ScheduleRetry(j) ==
/\ phase[j] = RetryWait
@ -421,14 +483,20 @@ RequestCancel(j) ==
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Cancelled means durable publication is forbidden, not process quiescence.
\* Cancelled forbids durable publication; it does not assert process stop.
FinalizeCancel(j) ==
/\ phase[j] = Cancelling
/\ phase' = [phase EXCEPT ![j] = Cancelled]
/\ authority' = [authority EXCEPT ![j] = NoAttempt]
/\ liveProgress' =
[liveProgress EXCEPT
![j] = IF liveProgressAttempt[j] # NoAttempt THEN 0 ELSE @]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid>>
/\ UNCHANGED coordinationVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
@ -438,7 +506,7 @@ PublishCancelNotice(j) ==
/\ cancelNotice' = [cancelNotice EXCEPT ![j] = TRUE]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, liveProgress,
liveProgressAttempt, coordinationLostOnce>>
liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
@ -451,8 +519,15 @@ CooperativeStop(a) ==
\/ (CanReach(w, DurableSvc) /\ cancelRequested[j])
\/ ~CurrentAuthority(a))
/\ attemptState' = [attemptState EXCEPT ![a] = AttemptStopped]
/\ liveProgress' =
[liveProgress EXCEPT
![j] = IF liveProgressAttempt[j] = a THEN 0 ELSE @]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT
![j] = IF @ = a THEN NoAttempt ELSE @]
/\ UNCHANGED durableVars
/\ UNCHANGED coordinationVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>>
@ -471,8 +546,7 @@ ReleaseLease(a) ==
[liveProgressAttempt EXCEPT
![j] = IF @ = a THEN NoAttempt ELSE @]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, cancelNotice,
coordinationLostOnce>>
/\ UNCHANGED <<queued, reservation, cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
@ -487,12 +561,11 @@ CleanTerminalCoordination(j) ==
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED durableVars
/\ UNCHANGED <<leaseState, leaseAge, coordinationLostOnce>>
/\ UNCHANGED <<leaseState, leaseAge, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Target write remains enabled after lease loss/replacement. Isolation by
\* attempt identity prevents this physical zombie from publishing.
\* Target write remains enabled after lease loss; staging identity fences publish.
AdvanceAttempt(a, amount) ==
LET w == attemptWorker[a]
IN /\ attemptState[a] = AttemptExecuting
@ -511,7 +584,6 @@ AdvanceAttempt(a, amount) ==
/\ UNCHANGED <<attemptState, attemptWorker, initialProgress,
resumedFromCheckpoint, pendingOutcome>>
\* Only current authority can persist a validated reusable checkpoint.
PersistCheckpoint(a) ==
LET j == JobOf(a)
w == attemptWorker[a]
@ -556,11 +628,10 @@ ReportProgress(a) ==
[liveProgressAttempt EXCEPT ![j] = a]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordinationLostOnce>>
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Invocation and processing are split, allowing delayed stale requests.
SendOutcome(a, outcome) ==
LET w == attemptWorker[a]
IN /\ outcome \in {WantsSuccess, WantsFailure}
@ -591,7 +662,7 @@ FailureEligible(a) ==
/\ phase[j] = Running
/\ ~cancelRequested[j]
\* Sole publication linearization point: a durable fenced CAS.
\* Sole publication linearization point: durable fenced CAS.
AcceptSuccess(a) ==
LET j == JobOf(a)
IN /\ CommitEligible(a)
@ -603,8 +674,12 @@ AcceptSuccess(a) ==
/\ attemptState' =
[attemptState EXCEPT ![a] = AttemptCommitted]
/\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome]
/\ liveProgress' = [liveProgress EXCEPT ![j] = 0]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded>>
/\ UNCHANGED coordinationVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState>>
@ -620,9 +695,13 @@ AcceptFailure(a) ==
/\ attemptState' =
[attemptState EXCEPT ![a] = AttemptStopped]
/\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome]
/\ liveProgress' = [liveProgress EXCEPT ![j] = 0]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid>>
/\ UNCHANGED coordinationVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState>>
@ -652,6 +731,11 @@ CleanupStage(a) ==
/\ UNCHANGED <<attemptState, attemptWorker, attemptProgress,
initialProgress, resumedFromCheckpoint, pendingOutcome>>
\* Terminal clean state: avoids TLC deadlock once protocol work is finished.
Done ==
/\ SystemQuiescent
/\ UNCHANGED vars
ReserveJob(j) == \E w \in Workers : Reserve(j, w)
AuthorizeJob(j) == \E w \in Workers : AuthorizeAttempt(j, w)
ActivateJob(j) ==
@ -699,8 +783,9 @@ Next ==
\/ \E a \in AttemptIds : AcceptFailure(a)
\/ \E a \in AttemptIds : RejectOutcome(a)
\/ \E a \in AttemptIds : CleanupStage(a)
\/ Done
\* Protocol-agent fairness is separate from the recovery assumption below.
\* Protocol-agent fairness is separate from RecoveryAssumption below.
Fairness ==
/\ \A j \in Jobs : WF_vars(Enqueue(j))
/\ \A j \in Jobs : SF_vars(ReserveJob(j))
@ -725,7 +810,6 @@ Fairness ==
SafetySpec == Init /\ [][Next]_vars
Spec == SafetySpec /\ Fairness
\* State invariants
TypeOK ==
/\ phase \in [Jobs -> Phases]
/\ cancelRequested \in [Jobs -> BOOLEAN]
@ -742,9 +826,10 @@ TypeOK ==
/\ cancelNotice \in [Jobs -> BOOLEAN]
/\ liveProgress \in [Jobs -> 0..MaxProgress]
/\ liveProgressAttempt \in [Jobs -> AttemptIds \cup {NoAttempt}]
/\ coordinationLostOnce \in BOOLEAN
/\ coordLossCount \in 0..MaxCoordLosses
/\ workerState \in [Workers -> WorkerStates]
/\ links \in [Workers -> [Services -> LinkStates]]
/\ partitionCount \in 0..MaxPartitions
/\ attemptState \in [AttemptIds -> AttemptStates]
/\ attemptWorker \in [AttemptIds -> Workers \cup {NoWorker}]
/\ attemptProgress \in [AttemptIds -> 0..MaxProgress]
@ -781,14 +866,38 @@ StateConsistency ==
/\ (stageState[a] = StageCleaned =>
committedAttempt[JobOf(a)] # a)
AuthoritativeAttempts(j) ==
{a \in AttemptIds : CurrentAuthority(a) /\ JobOf(a) = j}
AtMostOneAuthoritativeAttempt ==
\A j \in Jobs : Cardinality(AuthoritativeAttempts(j)) <= 1
FencingTokensUnique ==
\A a \in AttemptIds :
attemptState[a] # AttemptUnused =>
TokenOf(a) <= currentToken[JobOf(a)]
\* Tokens 1..currentToken are allocated densely (claim linearization).
AllocatedTokensUsed ==
\A j \in Jobs :
\A t \in 1..currentToken[j] :
attemptState[AttemptId(j, t)] # AttemptUnused
\* Live progress is always scoped to the current authoritative live lease.
LiveProgressAligned ==
\A j \in Jobs :
liveProgressAttempt[j] # NoAttempt =>
LET a == liveProgressAttempt[j]
IN /\ JobOf(a) = j
/\ CurrentAuthority(a)
/\ leaseState[a] = LeaseLive
/\ attemptState[a] = AttemptExecuting
/\ liveProgress[j] <= attemptProgress[a]
\* At most one deployment-wide live lease per job.
AtMostOneLiveLeasePerJob ==
\A j \in Jobs :
Cardinality({a \in AttemptIds :
JobOf(a) = j /\ leaseState[a] = LeaseLive}) <= 1
\* Authority, if present, is a non-unused attempt of this job at currentToken.
AuthorityWellFormed ==
\A j \in Jobs :
authority[j] # NoAttempt =>
/\ JobOf(authority[j]) = j
/\ TokenOf(authority[j]) = currentToken[j]
/\ attemptState[authority[j]] \in
{AttemptAuthorized, AttemptExecuting, AttemptStopped}
CommittedResultConsistent ==
\A j \in Jobs :
committedAttempt[j] # NoAttempt =>
@ -796,29 +905,33 @@ CommittedResultConsistent ==
/\ TokenOf(committedAttempt[j]) = currentToken[j]
/\ attemptState[committedAttempt[j]] = AttemptCommitted
/\ stageState[committedAttempt[j]] = StageComplete
/\ ~cancelRequested[j]
CancellationSafety ==
\A j \in Jobs :
cancelRequested[j] => committedAttempt[j] = NoAttempt
PermitSafety ==
/\ Cardinality(ReservedJobs) + Cardinality(LiveLeases) <= GlobalLimit
/\ \A w \in Workers :
Cardinality(ReservedFor(w)) + Cardinality(ExecutingFor(w)) <= LocalLimit
QueueRecoverable ==
\A j \in Jobs : phase[j] = Queued => dispatchNeeded[j]
AttemptIsolation ==
\A a \in AttemptIds :
committedAttempt[JobOf(a)] = a => stageState[a] = StageComplete
ResumeValidity ==
\A a \in AttemptIds :
/\ attemptProgress[a] >= initialProgress[a]
/\ (initialProgress[a] > 0 => resumedFromCheckpoint[a])
/\ (resumedFromCheckpoint[a] => initialProgress[a] > 0)
ZombieIsolation ==
\A a \in AttemptIds :
attemptState[a] = AttemptExecuting /\ ~CurrentAuthority(a) =>
committedAttempt[JobOf(a)] # a
\* Step properties
\* Uncommitted staging is only retained for live or stopped attempts, not cleaned
\* while still authoritative (cleanup gated in CleanupStage).
StagingOwnership ==
\A a \in AttemptIds :
/\ (stageState[a] = StageCleaned =>
/\ committedAttempt[JobOf(a)] # a
/\ ~CurrentAuthority(a))
/\ (committedAttempt[JobOf(a)] = a =>
stageState[a] = StageComplete)
TerminalStep ==
\A j \in Jobs :
Terminal(j) =>
@ -846,12 +959,18 @@ TerminalStateIsImmutable == [][TerminalStep]_vars
FencingTokensMonotonic == [][FenceStep]_vars
CommitIsFencedCAS == [][CommitLinearizationStep]_vars
\* Liveness is conditional; safety above needs no recovery assumption.
\* Liveness is conditional on eventual lasting capacity. Safety needs no recovery.
\* WorkerAvailable requires Coord, Durable, and Target reachable for some Up worker.
\* EventuallyDispatched: accepted work leaves Queued (starts Running or ends terminal,
\* including Cancelled). It is not "successful delivery of bytes."
\* EventuallyTerminal: some terminal outcome (Succeeded, Failed, or Cancelled).
\* Permanent source/target failure may yield Failed after the retry budget; success
\* is not guaranteed under unrestricted WantsFailure nondeterminism.
WorkerAvailable(w) ==
/\ workerState[w] = WorkerUp
/\ \A s \in Services : CanReach(w, s)
RecoveryAssumption == <>[](\E w \in Workers : WorkerAvailable(w))
AtLeastOnceDelivery ==
EventuallyDispatched ==
RecoveryAssumption =>
\A j \in Jobs :
phase[j] = Queued ~> (phase[j] = Running \/ Terminal(j))

18
docs/protocol/RemoraCombined.cfg
View file

@ -1,10 +1,12 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Combined contention: both local and deployment-wide limits constrain work.
\* Shrunk from 3 jobs to 2 so TLC finishes in minutes; Local=1 and Global=2
\* still force both limiters to bind under two live workers.
CONSTANTS
Jobs = {j1, j2, j3}
Jobs = {j1, j2}
Workers = {w1, w2}
InitialWorkers = {w1, w2}
NoJob = NoJob
@ -16,19 +18,21 @@ CONSTANTS
GlobalLimit = 2
FaultsEnabled = FALSE
FaultServices = {}
MaxCoordLosses = 0
MaxPartitions = 0
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable

15
docs/protocol/RemoraDurableFault.cfg
View file

@ -1,8 +1,9 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Worker can reach coordination and target while durable authority is cut.
\* Single worker: CrashWorker disabled (OtherCapacity); partitions only.
CONSTANTS
Jobs = {j1}
Workers = {w1}
@ -16,19 +17,21 @@ CONSTANTS
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Durable"}
MaxCoordLosses = 0
MaxPartitions = 2
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable

15
docs/protocol/RemoraFencing.cfg
View file

@ -1,8 +1,9 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Repeated fencing with delayed outcomes, lease loss, and replacement.
\* MaxAttempts=3 stresses token replacement; fault budgets kept at 1 for TLC size.
CONSTANTS
Jobs = {j1}
Workers = {w1, w2}
@ -16,19 +17,21 @@ CONSTANTS
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Coordination"}
MaxCoordLosses = 1
MaxPartitions = 1
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable

14
docs/protocol/RemoraGlobal.cfg
View file

@ -1,6 +1,6 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Global contention: local capacity does not constrain the global limit.
CONSTANTS
@ -16,19 +16,21 @@ CONSTANTS
GlobalLimit = 1
FaultsEnabled = FALSE
FaultServices = {}
MaxCoordLosses = 0
MaxPartitions = 0
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable

14
docs/protocol/RemoraLocal.cfg
View file

@ -1,6 +1,6 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Local contention: the global limit permits every worker-local slot.
CONSTANTS
@ -16,19 +16,21 @@ CONSTANTS
GlobalLimit = 3
FaultsEnabled = FALSE
FaultServices = {}
MaxCoordLosses = 0
MaxPartitions = 0
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable

38
docs/protocol/RemoraMultiShot.cfg Normal file
View file

@ -0,0 +1,38 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK TRUE
\* Multi-shot coordination wipe and re-partition (safety only; liveness is Remora.cfg).
CONSTANTS
Jobs = {j1}
Workers = {w1, w2}
InitialWorkers = {w1}
NoJob = NoJob
NoWorker = NoWorker
MaxAttempts = 2
MaxProgress = 1
LeaseLimit = 1
LocalLimit = 1
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Coordination"}
MaxCoordLosses = 2
MaxPartitions = 2
INVARIANTS
TypeOK
StateConsistency
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
ResumeValidity
StagingOwnership
PROPERTIES
TerminalStateIsImmutable
FencingTokensMonotonic
CommitIsFencedCAS

40
docs/protocol/RemoraStress.cfg Normal file
View file

@ -0,0 +1,40 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK TRUE
\* Stress envelope: MaxProgress=2 (partial resume), MaxAttempts=2 (retry),
\* multi-service faults (Coordination+Durable), single-shot fault budgets.
\* Deeper multi-shot budgets live in Remora.cfg; deeper MaxAttempts in RemoraFencing.
CONSTANTS
Jobs = {j1}
Workers = {w1, w2}
InitialWorkers = {w1}
NoJob = NoJob
NoWorker = NoWorker
MaxAttempts = 2
MaxProgress = 2
LeaseLimit = 1
LocalLimit = 1
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Coordination", "Durable"}
MaxCoordLosses = 1
MaxPartitions = 1
INVARIANTS
TypeOK
StateConsistency
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
ResumeValidity
StagingOwnership
PROPERTIES
TerminalStateIsImmutable
FencingTokensMonotonic
CommitIsFencedCAS

15
docs/protocol/RemoraTargetFault.cfg
View file

@ -1,8 +1,9 @@
SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE
CHECK_DEADLOCK TRUE
\* Worker can reach coordination and durable authority while target is cut.
\* Single worker: CrashWorker disabled (OtherCapacity); partitions only.
CONSTANTS
Jobs = {j1}
Workers = {w1}
@ -16,19 +17,21 @@ CONSTANTS
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Target"}
MaxCoordLosses = 0
MaxPartitions = 2
INVARIANTS
TypeOK
StateConsistency
AtMostOneAuthoritativeAttempt
FencingTokensUnique
AllocatedTokensUsed
LiveProgressAligned
AtMostOneLiveLeasePerJob
AuthorityWellFormed
CommittedResultConsistent
CancellationSafety
PermitSafety
QueueRecoverable
AttemptIsolation
ResumeValidity
ZombieIsolation
StagingOwnership
PROPERTIES
TerminalStateIsImmutable