ms2k/remora
SHA256
Watch
0
Code Releases Activity

Weaken live progress to a coordination-only hint (IF-6).

Browse source 
Drop LiveProgressAligned in favor of well-formedness and lease-compatible
progress, stop durable CAS from clearing Redis progress, and add ambient
ClearStaleLiveProgress so TLC matches Postgres + Dragonfly separation.
This commit is contained in:
ms2k 2026-07-10 14:16:29 +09:00
commit a3f502f6b6
10 changed files with 78 additions and 84 deletions
Download patch file Download diff file Expand all files Collapse all files

3
docs/protocol/Remora.cfg
View file

@ -25,7 +25,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

135
docs/protocol/Remora.tla
View file

@ -12,15 +12,17 @@ EXTENDS Naturals, FiniteSets, TLC
\* \*
\* Abstractions and bounds: \* Abstractions and bounds:
\* - Jobs in Init are already durably accepted (submission outbox precedes queueing). \* - Jobs in Init are already durably accepted (submission outbox precedes queueing).
\* - Reconciler projection (Enqueue, PublishCancelNotice, CleanTerminalCoordination) \* - Reconciler projection (Enqueue, PublishCancelNotice, CleanTerminalCoordination,
\* is ambient: it models a daemon with CoordinationStore access independent of \* ClearStaleLiveProgress) is ambient: CoordinationStore access independent of
\* per-worker links. Worker-facing coord ops still require CanReach(w, CoordSvc). \* per-worker links. Worker-facing coord ops still require CanReach(w, CoordSvc).
\* - Live progress is coordination-only; durable steps never clear it. Stale hints
\* linger until ClearStaleLiveProgress, ActivateAttempt overwrite, terminal clean,
\* or full coord wipe — not co-stepped with Postgres CAS.
\* - MaxCoordLosses bounds full CoordinationStore wipes; MaxPartitions bounds \* - MaxCoordLosses bounds full CoordinationStore wipes; MaxPartitions bounds
\* DropLink events (re-partition of LinkUp or LinkRecovered is allowed within budget). \* DropLink events (re-partition of LinkUp or LinkRecovered is allowed within budget).
\* - Worker ids are incarnations: WorkerUnused -> WorkerUp is scale-up/restart; \* - Worker ids are incarnations: WorkerUnused -> WorkerUp is scale-up/restart;
\* WorkerDown is permanent for that id. CrashWorker will not crash the last \* 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. \* 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. \* - CHECK_DEADLOCK expects Done when the system is protocol-quiescent.
CONSTANTS CONSTANTS
@ -96,6 +98,7 @@ OutcomeRequests == {NoOutcome, WantsSuccess, WantsFailure}
NoAttempt == [job |-> NoJob, token |-> 0] NoAttempt == [job |-> NoJob, token |-> 0]
\* Product: opaque attempt id + separate fence; model fuses them as <<job, token>>.
AttemptIds == AttemptIds ==
{[job |-> j, token |-> token] : {[job |-> j, token |-> token] :
j \in Jobs, token \in 1..MaxAttempts} j \in Jobs, token \in 1..MaxAttempts}
@ -314,22 +317,18 @@ Tick ==
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED attemptVars /\ UNCHANGED attemptVars
\* Lease expiry does not clear live progress: product may retain a stale
\* (attempt, bytes) hint until overwrite, reader discard, or terminal GC.
ExpireLease(a) == ExpireLease(a) ==
LET j == JobOf(a) /\ leaseState[a] = LeaseLive
IN /\ leaseState[a] = LeaseLive /\ leaseAge[a] = LeaseLimit
/\ leaseAge[a] = LeaseLimit /\ leaseState' = [leaseState EXCEPT ![a] = LeaseExpired]
/\ leaseState' = [leaseState EXCEPT ![a] = LeaseExpired] /\ leaseAge' = [leaseAge EXCEPT ![a] = 0]
/\ leaseAge' = [leaseAge EXCEPT ![a] = 0] /\ UNCHANGED durableVars
/\ liveProgress' = /\ UNCHANGED <<queued, reservation, cancelNotice, liveProgress,
[liveProgress EXCEPT liveProgressAttempt, coordLossCount>>
![j] = IF liveProgressAttempt[j] = a THEN 0 ELSE @] /\ UNCHANGED workerVars
/\ liveProgressAttempt' = /\ UNCHANGED attemptVars
[liveProgressAttempt EXCEPT
![j] = IF @ = a THEN NoAttempt ELSE @]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
\* Full CoordinationStore wipe; durable authority and processes unchanged. \* Full CoordinationStore wipe; durable authority and processes unchanged.
LoseCoordinationState == LoseCoordinationState ==
@ -374,6 +373,7 @@ RestoreLink(w, service) ==
/\ UNCHANGED partitionCount /\ UNCHANGED partitionCount
/\ UNCHANGED attemptVars /\ UNCHANGED attemptVars
\* Crash does not clear coordination progress (Redis keys outlive the process).
CrashWorker(w) == CrashWorker(w) ==
/\ FaultsEnabled /\ FaultsEnabled
/\ workerState[w] = WorkerUp /\ workerState[w] = WorkerUp
@ -384,19 +384,8 @@ CrashWorker(w) ==
IF attemptWorker[a] = w IF attemptWorker[a] = w
/\ attemptState[a] \in {AttemptAuthorized, AttemptExecuting} /\ attemptState[a] \in {AttemptAuthorized, AttemptExecuting}
THEN AttemptStopped ELSE attemptState[a]] 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 durableVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, /\ UNCHANGED coordinationVars
cancelNotice, coordLossCount>>
/\ UNCHANGED links /\ UNCHANGED links
/\ UNCHANGED partitionCount /\ UNCHANGED partitionCount
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress, /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
@ -428,6 +417,7 @@ ReleaseReservation(j) ==
\* Revoke durable authority; stop authorized-never-activated attempts so staging \* Revoke durable authority; stop authorized-never-activated attempts so staging
\* can clean. Executing attempts become zombies until CooperativeStop. \* can clean. Executing attempts become zombies until CooperativeStop.
\* Progress stays in coordination until ClearStaleLiveProgress (not co-stepped).
ReapLostAttempt(a) == ReapLostAttempt(a) ==
LET j == JobOf(a) LET j == JobOf(a)
IN /\ CurrentAuthority(a) IN /\ CurrentAuthority(a)
@ -444,16 +434,9 @@ ReapLostAttempt(a) ==
[attemptState EXCEPT [attemptState EXCEPT
![a] = IF attemptState[a] = AttemptAuthorized ![a] = IF attemptState[a] = AttemptAuthorized
THEN AttemptStopped ELSE @] 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, /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid>> committedAttempt, checkpoint, checkpointValid>>
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, /\ UNCHANGED coordinationVars
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress, /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>> resumedFromCheckpoint, stageState, pendingOutcome>>
@ -484,19 +467,14 @@ RequestCancel(j) ==
/\ UNCHANGED attemptVars /\ UNCHANGED attemptVars
\* Cancelled forbids durable publication; it does not assert process stop. \* Cancelled forbids durable publication; it does not assert process stop.
\* Progress remains until coord GC (ClearStaleLiveProgress / terminal clean).
FinalizeCancel(j) == FinalizeCancel(j) ==
/\ phase[j] = Cancelling /\ phase[j] = Cancelling
/\ phase' = [phase EXCEPT ![j] = Cancelled] /\ phase' = [phase EXCEPT ![j] = Cancelled]
/\ authority' = [authority EXCEPT ![j] = NoAttempt] /\ 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, /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid>> committedAttempt, checkpoint, checkpointValid>>
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, /\ UNCHANGED coordinationVars
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED attemptVars /\ UNCHANGED attemptVars
@ -519,19 +497,13 @@ CooperativeStop(a) ==
\/ (CanReach(w, DurableSvc) /\ cancelRequested[j]) \/ (CanReach(w, DurableSvc) /\ cancelRequested[j])
\/ ~CurrentAuthority(a)) \/ ~CurrentAuthority(a))
/\ attemptState' = [attemptState EXCEPT ![a] = AttemptStopped] /\ 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 durableVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, /\ UNCHANGED coordinationVars
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress, /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState, pendingOutcome>> resumedFromCheckpoint, stageState, pendingOutcome>>
\* Coord-only lease drop; progress GC is separate (ClearStaleLiveProgress).
ReleaseLease(a) == ReleaseLease(a) ==
LET j == JobOf(a) LET j == JobOf(a)
IN /\ leaseState[a] = LeaseLive IN /\ leaseState[a] = LeaseLive
@ -539,17 +511,27 @@ ReleaseLease(a) ==
\/ ~CurrentAuthority(a) \/ Terminal(j)) \/ ~CurrentAuthority(a) \/ Terminal(j))
/\ leaseState' = [leaseState EXCEPT ![a] = LeaseExpired] /\ leaseState' = [leaseState EXCEPT ![a] = LeaseExpired]
/\ leaseAge' = [leaseAge EXCEPT ![a] = 0] /\ leaseAge' = [leaseAge EXCEPT ![a] = 0]
/\ liveProgress' =
[liveProgress EXCEPT
![j] = IF liveProgressAttempt[j] = a THEN 0 ELSE @]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT
![j] = IF @ = a THEN NoAttempt ELSE @]
/\ UNCHANGED durableVars /\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, cancelNotice, coordLossCount>> /\ UNCHANGED <<queued, reservation, cancelNotice, liveProgress,
liveProgressAttempt, coordLossCount>>
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED attemptVars /\ UNCHANGED attemptVars
\* Ambient: drop progress that is not backed by current authority + live lease.
\* Models Redis GC / reaper independent of durable CAS.
ClearStaleLiveProgress(j) ==
/\ liveProgressAttempt[j] # NoAttempt
/\ LET a == liveProgressAttempt[j]
IN ~(CurrentAuthority(a) /\ leaseState[a] = LeaseLive)
/\ liveProgress' = [liveProgress EXCEPT ![j] = 0]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED durableVars
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge,
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars
/\ UNCHANGED attemptVars
CleanTerminalCoordination(j) == CleanTerminalCoordination(j) ==
/\ Terminal(j) /\ Terminal(j)
/\ (queued[j] \/ reservation[j] # NoWorker \/ cancelNotice[j] /\ (queued[j] \/ reservation[j] # NoWorker \/ cancelNotice[j]
@ -663,6 +645,7 @@ FailureEligible(a) ==
/\ ~cancelRequested[j] /\ ~cancelRequested[j]
\* Sole publication linearization point: durable fenced CAS. \* Sole publication linearization point: durable fenced CAS.
\* Does not touch coordination progress (cleared by ambient coord GC).
AcceptSuccess(a) == AcceptSuccess(a) ==
LET j == JobOf(a) LET j == JobOf(a)
IN /\ CommitEligible(a) IN /\ CommitEligible(a)
@ -674,12 +657,8 @@ AcceptSuccess(a) ==
/\ attemptState' = /\ attemptState' =
[attemptState EXCEPT ![a] = AttemptCommitted] [attemptState EXCEPT ![a] = AttemptCommitted]
/\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome] /\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome]
/\ liveProgress' = [liveProgress EXCEPT ![j] = 0]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded>> /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded>>
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, /\ UNCHANGED coordinationVars
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress, /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState>> resumedFromCheckpoint, stageState>>
@ -695,13 +674,9 @@ AcceptFailure(a) ==
/\ attemptState' = /\ attemptState' =
[attemptState EXCEPT ![a] = AttemptStopped] [attemptState EXCEPT ![a] = AttemptStopped]
/\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome] /\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome]
/\ liveProgress' = [liveProgress EXCEPT ![j] = 0]
/\ liveProgressAttempt' =
[liveProgressAttempt EXCEPT ![j] = NoAttempt]
/\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded, /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
committedAttempt, checkpoint, checkpointValid>> committedAttempt, checkpoint, checkpointValid>>
/\ UNCHANGED <<queued, reservation, leaseState, leaseAge, /\ UNCHANGED coordinationVars
cancelNotice, coordLossCount>>
/\ UNCHANGED workerVars /\ UNCHANGED workerVars
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress, /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState>> resumedFromCheckpoint, stageState>>
@ -772,6 +747,7 @@ Next ==
\/ \E j \in Jobs : PublishCancelNotice(j) \/ \E j \in Jobs : PublishCancelNotice(j)
\/ \E a \in AttemptIds : CooperativeStop(a) \/ \E a \in AttemptIds : CooperativeStop(a)
\/ \E a \in AttemptIds : ReleaseLease(a) \/ \E a \in AttemptIds : ReleaseLease(a)
\/ \E j \in Jobs : ClearStaleLiveProgress(j)
\/ \E j \in Jobs : CleanTerminalCoordination(j) \/ \E j \in Jobs : CleanTerminalCoordination(j)
\/ \E a \in AttemptIds, n \in 1..MaxProgress : AdvanceAttempt(a, n) \/ \E a \in AttemptIds, n \in 1..MaxProgress : AdvanceAttempt(a, n)
\/ \E a \in AttemptIds : PersistCheckpoint(a) \/ \E a \in AttemptIds : PersistCheckpoint(a)
@ -802,6 +778,7 @@ Fairness ==
/\ \A j \in Jobs : WF_vars(ScheduleRetry(j)) /\ \A j \in Jobs : WF_vars(ScheduleRetry(j))
/\ \A j \in Jobs : WF_vars(FinalizeCancel(j)) /\ \A j \in Jobs : WF_vars(FinalizeCancel(j))
/\ \A j \in Jobs : WF_vars(PublishCancelNotice(j)) /\ \A j \in Jobs : WF_vars(PublishCancelNotice(j))
/\ \A j \in Jobs : WF_vars(ClearStaleLiveProgress(j))
/\ \A j \in Jobs : WF_vars(CleanTerminalCoordination(j)) /\ \A j \in Jobs : WF_vars(CleanTerminalCoordination(j))
/\ \A w \in Workers, s \in Services : WF_vars(RestoreLink(w, s)) /\ \A w \in Workers, s \in Services : WF_vars(RestoreLink(w, s))
/\ \A w \in Workers : WF_vars(StartIncarnation(w)) /\ \A w \in Workers : WF_vars(StartIncarnation(w))
@ -872,17 +849,25 @@ AllocatedTokensUsed ==
\A t \in 1..currentToken[j] : \A t \in 1..currentToken[j] :
attemptState[AttemptId(j, t)] # AttemptUnused attemptState[AttemptId(j, t)] # AttemptUnused
\* Live progress is always scoped to the current authoritative live lease. \* Live progress is a coordination hint, not a cross-store snapshot invariant.
LiveProgressAligned == \* Stale tuples may remain after lease loss; readers revalidate against authority.
LiveProgressWellFormed ==
\A j \in Jobs : \A j \in Jobs :
liveProgressAttempt[j] # NoAttempt => liveProgressAttempt[j] # NoAttempt =>
LET a == liveProgressAttempt[j] LET a == liveProgressAttempt[j]
IN /\ JobOf(a) = j IN /\ JobOf(a) = j
/\ CurrentAuthority(a) /\ attemptState[a] # AttemptUnused
/\ leaseState[a] = LeaseLive /\ TokenOf(a) <= currentToken[j]
/\ attemptState[a] = AttemptExecuting
/\ liveProgress[j] <= attemptProgress[a] /\ liveProgress[j] <= attemptProgress[a]
\* Catches leftover zombie progress under a live lease for a different attempt
\* (forgot to overwrite/clear on activate/replace). Empty progress is allowed.
LiveProgressCompatibleWithLiveLease ==
\A j \in Jobs :
\A a \in AttemptIds :
(JobOf(a) = j /\ leaseState[a] = LeaseLive) =>
liveProgressAttempt[j] \in {NoAttempt, a}
\* At most one deployment-wide live lease per job. \* At most one deployment-wide live lease per job.
AtMostOneLiveLeasePerJob == AtMostOneLiveLeasePerJob ==
\A j \in Jobs : \A j \in Jobs :

3
docs/protocol/RemoraCombined.cfg
View file

@ -25,7 +25,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraDurableFault.cfg
View file

@ -24,7 +24,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraFencing.cfg
View file

@ -24,7 +24,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraGlobal.cfg
View file

@ -23,7 +23,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraLocal.cfg
View file

@ -23,7 +23,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraMultiShot.cfg
View file

@ -23,7 +23,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraStress.cfg
View file

@ -25,7 +25,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent

3
docs/protocol/RemoraTargetFault.cfg
View file

@ -24,7 +24,8 @@ INVARIANTS
TypeOK TypeOK
StateConsistency StateConsistency
AllocatedTokensUsed AllocatedTokensUsed
LiveProgressAligned LiveProgressWellFormed
LiveProgressCompatibleWithLiveLease
AtMostOneLiveLeasePerJob AtMostOneLiveLeasePerJob
AuthorityWellFormed AuthorityWellFormed
CommittedResultConsistent CommittedResultConsistent