ms2k/remora
SHA256
Watch
0
Code Releases Activity

Model durable failure disposition

Browse source
This commit is contained in:
ms2k 2026-07-13 16:41:51 +09:00
commit 5fdb339fe5
1 changed files with 113 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

72
docs/protocol/Remora.tla
View file

@ -93,10 +93,12 @@ StageComplete == "StageComplete"
StageCleaned == "StageCleaned"
StageStates == {StageNone, StagePartial, StageComplete, StageCleaned}
NoOutcome == "NoOutcome"
WantsSuccess == "WantsSuccess"
WantsFailure == "WantsFailure"
OutcomeRequests == {NoOutcome, WantsSuccess, WantsFailure}
NoOutcome == "NoOutcome"
WantsSuccess == "WantsSuccess"
WantsRetryableFailure == "WantsRetryableFailure"
WantsPermanentFailure == "WantsPermanentFailure"
FailureOutcomes == {WantsRetryableFailure, WantsPermanentFailure}
OutcomeRequests == {NoOutcome, WantsSuccess} \cup FailureOutcomes
NoAttempt == [job |-> NoJob, token |-> 0]
@ -628,12 +630,12 @@ ReportProgress(a) ==
SendOutcome(a, outcome) ==
LET w == attemptWorker[a]
IN /\ outcome \in {WantsSuccess, WantsFailure}
IN /\ outcome \in {WantsSuccess} \cup FailureOutcomes
/\ attemptState[a] = AttemptExecuting
/\ pendingOutcome[a] = NoOutcome
/\ workerState[w] = WorkerUp
/\ CanReach(w, DurableSvc)
/\ (outcome = WantsFailure \/ stageState[a] = StageComplete)
/\ (outcome \in FailureOutcomes \/ stageState[a] = StageComplete)
/\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = outcome]
/\ UNCHANGED durableVars
/\ UNCHANGED coordinationVars
@ -651,7 +653,7 @@ CommitEligible(a) ==
FailureEligible(a) ==
LET j == JobOf(a)
IN /\ pendingOutcome[a] = WantsFailure
IN /\ pendingOutcome[a] \in FailureOutcomes
/\ CurrentAuthority(a)
/\ phase[j] = Running
/\ ~cancelRequested[j]
@ -675,13 +677,16 @@ AcceptSuccess(a) ==
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState>>
AcceptFailure(a) ==
AcceptFailure(a, outcome) ==
LET j == JobOf(a)
IN /\ FailureEligible(a)
IN /\ pendingOutcome[a] = outcome
/\ FailureEligible(a)
/\ phase' =
[phase EXCEPT
![j] = IF currentToken[j] < MaxAttempts
THEN RetryWait ELSE Failed]
![j] = IF outcome = WantsPermanentFailure
THEN Failed
ELSE IF currentToken[j] < MaxAttempts
THEN RetryWait ELSE Failed]
/\ authority' = [authority EXCEPT ![j] = NoAttempt]
/\ attemptState' =
[attemptState EXCEPT ![a] = AttemptStopped]
@ -693,6 +698,18 @@ AcceptFailure(a) ==
/\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
resumedFromCheckpoint, stageState>>
AcceptPermanentFailure(a) ==
/\ pendingOutcome[a] = WantsPermanentFailure
/\ AcceptFailure(a, WantsPermanentFailure)
AcceptRetryableFailureWithBudget(a) ==
/\ currentToken[JobOf(a)] < MaxAttempts
/\ AcceptFailure(a, WantsRetryableFailure)
AcceptRetryableFailureExhausted(a) ==
/\ currentToken[JobOf(a)] = MaxAttempts
/\ AcceptFailure(a, WantsRetryableFailure)
RejectOutcome(a) ==
/\ pendingOutcome[a] # NoOutcome
/\ ~CommitEligible(a)
@ -730,11 +747,16 @@ ActivateJob(j) ==
ExecuteJob(j) ==
\E a \in AttemptIds :
/\ JobOf(a) = j
/\ (SendOutcome(a, WantsFailure)
/\ (SendOutcome(a, WantsRetryableFailure)
\/ SendOutcome(a, WantsPermanentFailure)
\/ SendOutcome(a, WantsSuccess)
\/ \E amount \in 1..MaxProgress : AdvanceAttempt(a, amount))
ProcessOutcome(a) ==
AcceptSuccess(a) \/ AcceptFailure(a) \/ RejectOutcome(a)
\/ AcceptSuccess(a)
\/ AcceptPermanentFailure(a)
\/ AcceptRetryableFailureWithBudget(a)
\/ AcceptRetryableFailureExhausted(a)
\/ RejectOutcome(a)
ReapJob(j) ==
\E a \in AttemptIds : JobOf(a) = j /\ ReapLostAttempt(a)
@ -765,10 +787,12 @@ Next ==
\/ \E a \in AttemptIds : PersistCheckpoint(a)
\/ \E j \in Jobs : InvalidateCheckpoint(j)
\/ \E a \in AttemptIds : ReportProgress(a)
\/ \E a \in AttemptIds, o \in {WantsSuccess, WantsFailure} :
\/ \E a \in AttemptIds, o \in {WantsSuccess} \cup FailureOutcomes :
SendOutcome(a, o)
\/ \E a \in AttemptIds : AcceptSuccess(a)
\/ \E a \in AttemptIds : AcceptFailure(a)
\/ \E a \in AttemptIds : AcceptPermanentFailure(a)
\/ \E a \in AttemptIds : AcceptRetryableFailureWithBudget(a)
\/ \E a \in AttemptIds : AcceptRetryableFailureExhausted(a)
\/ \E a \in AttemptIds : RejectOutcome(a)
\/ \E a \in AttemptIds : CleanupStage(a)
\/ Done
@ -952,17 +976,31 @@ CommitLinearizationStep ==
/\ ~cancelRequested[j]
/\ stageState[committedAttempt'[j]] = StageComplete
FailureDispositionStep ==
\A a \in AttemptIds :
LET j == JobOf(a)
IN /\ FailureEligible(a)
/\ attemptState'[a] = AttemptStopped
/\ pendingOutcome'[a] = NoOutcome
/\ authority'[j] = NoAttempt
=> phase'[j] =
IF pendingOutcome[a] = WantsPermanentFailure
THEN Failed
ELSE IF currentToken[j] < MaxAttempts
THEN RetryWait ELSE Failed
TerminalStateIsImmutable == [][TerminalStep]_vars
FencingTokensMonotonic == [][FenceStep]_vars
CommitIsFencedCAS == [][CommitLinearizationStep]_vars
FailureDispositionHonored == [][FailureDispositionStep]_vars
\* 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.
\* Permanent failure may yield Failed immediately; retryable failure may yield
\* Failed after the retry budget. Success is not guaranteed under either choice.
\* EventuallyNonWinnerStagingCleaned / EventuallySystemQuiescent: model GC goal under
\* fairness (infallible CleanupStage). Product seeks zero orphans under recovery;
\* not a safety invariant and not a readiness gate (IF-7).