|
|
|
|
@ -31,7 +31,7 @@ CONSTANTS
|
|
|
|
|
Jobs, Workers, InitialWorkers, NoJob, NoWorker,
|
|
|
|
|
MaxAttempts, MaxProgress, LeaseLimit, ReservationLimit,
|
|
|
|
|
LocalLimit, GlobalLimit, FaultsEnabled, FaultServices,
|
|
|
|
|
MaxCoordLosses, MaxPartitions
|
|
|
|
|
MaxCoordLosses, MaxPartitions, MaxCredentialIntents
|
|
|
|
|
|
|
|
|
|
ASSUME /\ Jobs # {}
|
|
|
|
|
/\ Workers # {}
|
|
|
|
|
@ -47,6 +47,7 @@ ASSUME /\ Jobs # {}
|
|
|
|
|
/\ FaultServices \subseteq {"Coordination", "Durable", "Target"}
|
|
|
|
|
/\ MaxCoordLosses \in Nat
|
|
|
|
|
/\ MaxPartitions \in Nat
|
|
|
|
|
/\ MaxCredentialIntents \in Nat
|
|
|
|
|
/\ NoJob \notin Jobs
|
|
|
|
|
/\ NoWorker \notin Workers
|
|
|
|
|
|
|
|
|
|
@ -94,6 +95,24 @@ StageComplete == "StageComplete"
|
|
|
|
|
StageCleaned == "StageCleaned"
|
|
|
|
|
StageStates == {StageNone, StagePartial, StageComplete, StageCleaned}
|
|
|
|
|
|
|
|
|
|
CredentialIntentUnused == "CredentialIntentUnused"
|
|
|
|
|
CredentialIntentPrepared == "CredentialIntentPrepared"
|
|
|
|
|
CredentialIntentWriting == "CredentialIntentWriting"
|
|
|
|
|
CredentialIntentWritten == "CredentialIntentWritten"
|
|
|
|
|
CredentialIntentCommitted == "CredentialIntentCommitted"
|
|
|
|
|
CredentialIntentAbandoning == "CredentialIntentAbandoning"
|
|
|
|
|
CredentialIntentAbandoned == "CredentialIntentAbandoned"
|
|
|
|
|
CredentialIntentStates ==
|
|
|
|
|
{CredentialIntentUnused, CredentialIntentPrepared,
|
|
|
|
|
CredentialIntentWriting, CredentialIntentWritten,
|
|
|
|
|
CredentialIntentCommitted, CredentialIntentAbandoning,
|
|
|
|
|
CredentialIntentAbandoned}
|
|
|
|
|
|
|
|
|
|
VaultSecretAbsent == "VaultSecretAbsent"
|
|
|
|
|
VaultSecretLive == "VaultSecretLive"
|
|
|
|
|
VaultSecretDestroyed == "VaultSecretDestroyed"
|
|
|
|
|
VaultSecretStates == {VaultSecretAbsent, VaultSecretLive, VaultSecretDestroyed}
|
|
|
|
|
|
|
|
|
|
NoOutcome == "NoOutcome"
|
|
|
|
|
WantsSuccess == "WantsSuccess"
|
|
|
|
|
WantsRetryableFailure == "WantsRetryableFailure"
|
|
|
|
|
@ -111,6 +130,9 @@ AttemptIds ==
|
|
|
|
|
AttemptId(j, token) == [job |-> j, token |-> token]
|
|
|
|
|
JobOf(a) == a.job
|
|
|
|
|
TokenOf(a) == a.token
|
|
|
|
|
CredentialIntents ==
|
|
|
|
|
{[job |-> j, sequence |-> sequence] :
|
|
|
|
|
j \in Jobs, sequence \in 1..MaxCredentialIntents}
|
|
|
|
|
|
|
|
|
|
VARIABLES
|
|
|
|
|
\* DurableStore authority.
|
|
|
|
|
@ -128,7 +150,10 @@ VARIABLES
|
|
|
|
|
|
|
|
|
|
\* Attempts, staging, delayed outcome requests.
|
|
|
|
|
attemptState, attemptWorker, attemptProgress, initialProgress,
|
|
|
|
|
resumedFromCheckpoint, stageState, pendingOutcome
|
|
|
|
|
resumedFromCheckpoint, stageState, pendingOutcome,
|
|
|
|
|
|
|
|
|
|
\* Credential write ownership across DurableStore and Vault.
|
|
|
|
|
credentialIntentState, vaultSecretState, credentialVersionDurable
|
|
|
|
|
|
|
|
|
|
durableVars ==
|
|
|
|
|
<<phase, cancelRequested, currentToken, authority, dispatchNeeded,
|
|
|
|
|
@ -140,7 +165,10 @@ workerVars == <<workerState, links, partitionCount>>
|
|
|
|
|
attemptVars ==
|
|
|
|
|
<<attemptState, attemptWorker, attemptProgress, initialProgress,
|
|
|
|
|
resumedFromCheckpoint, stageState, pendingOutcome>>
|
|
|
|
|
vars == <<durableVars, coordinationVars, workerVars, attemptVars>>
|
|
|
|
|
credentialVars ==
|
|
|
|
|
<<credentialIntentState, vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
jobVars == <<durableVars, coordinationVars, workerVars, attemptVars>>
|
|
|
|
|
vars == <<jobVars, credentialVars>>
|
|
|
|
|
|
|
|
|
|
Terminal(j) == phase[j] \in TerminalPhases
|
|
|
|
|
CanReach(w, service) == links[w][service] # LinkDown
|
|
|
|
|
@ -175,8 +203,8 @@ CoordinationClean(j) ==
|
|
|
|
|
/\ liveProgressAttempt[j] = NoAttempt
|
|
|
|
|
|
|
|
|
|
\* TLC full quiescence (terminal + coord clean + non-winner staging cleaned).
|
|
|
|
|
\* Product may retain orphans; do not assert this at runtime. Safety is
|
|
|
|
|
\* CommittedResult + StagingOwnership, not zero residual objects.
|
|
|
|
|
\* Attempt-scoped target staging may remain; secret writes are covered separately
|
|
|
|
|
\* by NoOrphanSecrets because residual credential material is sensitive.
|
|
|
|
|
SystemQuiescent ==
|
|
|
|
|
/\ \A j \in Jobs : Terminal(j) /\ CoordinationClean(j)
|
|
|
|
|
/\ \A a \in AttemptIds :
|
|
|
|
|
@ -185,6 +213,10 @@ SystemQuiescent ==
|
|
|
|
|
/\ attemptState[a] \notin {AttemptAuthorized, AttemptExecuting}
|
|
|
|
|
/\ (stageState[a] \in {StagePartial, StageComplete} =>
|
|
|
|
|
committedAttempt[JobOf(a)] = a)
|
|
|
|
|
/\ \A c \in CredentialIntents :
|
|
|
|
|
credentialIntentState[c] \in
|
|
|
|
|
{CredentialIntentUnused, CredentialIntentCommitted,
|
|
|
|
|
CredentialIntentAbandoned}
|
|
|
|
|
|
|
|
|
|
Init ==
|
|
|
|
|
/\ phase = [j \in Jobs |-> Queued]
|
|
|
|
|
@ -216,6 +248,10 @@ Init ==
|
|
|
|
|
/\ resumedFromCheckpoint = [a \in AttemptIds |-> FALSE]
|
|
|
|
|
/\ stageState = [a \in AttemptIds |-> StageNone]
|
|
|
|
|
/\ pendingOutcome = [a \in AttemptIds |-> NoOutcome]
|
|
|
|
|
/\ credentialIntentState =
|
|
|
|
|
[c \in CredentialIntents |-> CredentialIntentUnused]
|
|
|
|
|
/\ vaultSecretState = [c \in CredentialIntents |-> VaultSecretAbsent]
|
|
|
|
|
/\ credentialVersionDurable = [c \in CredentialIntents |-> FALSE]
|
|
|
|
|
|
|
|
|
|
\* Ambient reconciler: projects durable dispatch into CoordinationStore.
|
|
|
|
|
Enqueue(j) ==
|
|
|
|
|
@ -773,6 +809,83 @@ CleanupStage(a) ==
|
|
|
|
|
/\ UNCHANGED <<attemptState, attemptWorker, attemptProgress,
|
|
|
|
|
initialProgress, resumedFromCheckpoint, pendingOutcome>>
|
|
|
|
|
|
|
|
|
|
PrepareCredentialIntent(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentUnused
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentPrepared]
|
|
|
|
|
/\ UNCHANGED <<vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
BeginCredentialWrite(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentPrepared
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretAbsent
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentWriting]
|
|
|
|
|
/\ UNCHANGED <<vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
CompleteCredentialWrite(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentWriting
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretAbsent
|
|
|
|
|
/\ vaultSecretState' = [vaultSecretState EXCEPT ![c] = VaultSecretLive]
|
|
|
|
|
/\ UNCHANGED <<credentialIntentState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
RecordCredentialWrite(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentWriting
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretLive
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentWritten]
|
|
|
|
|
/\ UNCHANGED <<vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
FenceFailedCredentialWrite(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentWriting
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretAbsent
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentPrepared]
|
|
|
|
|
/\ UNCHANGED <<vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
CommitCredentialVersion(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentWritten
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretLive
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentCommitted]
|
|
|
|
|
/\ credentialVersionDurable' =
|
|
|
|
|
[credentialVersionDurable EXCEPT ![c] = TRUE]
|
|
|
|
|
/\ UNCHANGED vaultSecretState
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
ClaimCredentialCleanup(c) ==
|
|
|
|
|
/\ credentialIntentState[c] \in
|
|
|
|
|
{CredentialIntentWriting, CredentialIntentWritten}
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretLive
|
|
|
|
|
/\ ~credentialVersionDurable[c]
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentAbandoning]
|
|
|
|
|
/\ UNCHANGED <<vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
DestroyClaimedCredentialSecret(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentAbandoning
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretLive
|
|
|
|
|
/\ ~credentialVersionDurable[c]
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentAbandoned]
|
|
|
|
|
/\ vaultSecretState' =
|
|
|
|
|
[vaultSecretState EXCEPT ![c] = VaultSecretDestroyed]
|
|
|
|
|
/\ UNCHANGED credentialVersionDurable
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
AbandonFencedCredentialIntent(c) ==
|
|
|
|
|
/\ credentialIntentState[c] = CredentialIntentPrepared
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretAbsent
|
|
|
|
|
/\ credentialIntentState' =
|
|
|
|
|
[credentialIntentState EXCEPT ![c] = CredentialIntentAbandoned]
|
|
|
|
|
/\ UNCHANGED <<vaultSecretState, credentialVersionDurable>>
|
|
|
|
|
/\ UNCHANGED jobVars
|
|
|
|
|
|
|
|
|
|
\* Stuttering sink for CHECK_DEADLOCK when SystemQuiescent; not a product API.
|
|
|
|
|
Done ==
|
|
|
|
|
/\ SystemQuiescent
|
|
|
|
|
@ -798,7 +911,7 @@ ProcessOutcome(a) ==
|
|
|
|
|
ReapJob(j) ==
|
|
|
|
|
\E a \in AttemptIds : JobOf(a) = j /\ ReapLostAttempt(a)
|
|
|
|
|
|
|
|
|
|
Next ==
|
|
|
|
|
JobNext ==
|
|
|
|
|
\/ \E j \in Jobs : Enqueue(j)
|
|
|
|
|
\/ \E j \in Jobs, w \in Workers : Reserve(j, w)
|
|
|
|
|
\/ \E j \in Jobs, w \in Workers : AuthorizeAttempt(j, w)
|
|
|
|
|
@ -834,31 +947,49 @@ Next ==
|
|
|
|
|
\/ \E a \in AttemptIds : AcceptRetryableFailureExhausted(a)
|
|
|
|
|
\/ \E a \in AttemptIds : RejectOutcome(a)
|
|
|
|
|
\/ \E a \in AttemptIds : CleanupStage(a)
|
|
|
|
|
|
|
|
|
|
CredentialNext ==
|
|
|
|
|
\/ \E c \in CredentialIntents : PrepareCredentialIntent(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : BeginCredentialWrite(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : CompleteCredentialWrite(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : RecordCredentialWrite(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : FenceFailedCredentialWrite(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : CommitCredentialVersion(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : ClaimCredentialCleanup(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : DestroyClaimedCredentialSecret(c)
|
|
|
|
|
\/ \E c \in CredentialIntents : AbandonFencedCredentialIntent(c)
|
|
|
|
|
|
|
|
|
|
Next ==
|
|
|
|
|
\/ /\ JobNext
|
|
|
|
|
/\ UNCHANGED credentialVars
|
|
|
|
|
\/ CredentialNext
|
|
|
|
|
\/ Done
|
|
|
|
|
|
|
|
|
|
JobStep(action) == action /\ UNCHANGED credentialVars
|
|
|
|
|
|
|
|
|
|
\* 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))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(AuthorizeJob(j))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(ActivateJob(j))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(ExecuteJob(j))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(ProcessOutcome(a))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(ExpireLease(a))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(ExpireReservation(j))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(CooperativeStop(a))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(ReleaseLease(a))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(CleanupStage(a))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(ReleaseReservation(j))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(ReapJob(j))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(ScheduleRetry(j))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(FinalizeCancel(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 w \in Workers, s \in Services : WF_vars(RestoreLink(w, s))
|
|
|
|
|
/\ \A w \in Workers : WF_vars(StartIncarnation(w))
|
|
|
|
|
/\ WF_vars(Tick)
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(Enqueue(j)))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(JobStep(ReserveJob(j)))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(JobStep(AuthorizeJob(j)))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(JobStep(ActivateJob(j)))
|
|
|
|
|
/\ \A j \in Jobs : SF_vars(JobStep(ExecuteJob(j)))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(JobStep(ProcessOutcome(a)))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(JobStep(ExpireLease(a)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(ExpireReservation(j)))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(JobStep(CooperativeStop(a)))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(JobStep(ReleaseLease(a)))
|
|
|
|
|
/\ \A a \in AttemptIds : WF_vars(JobStep(CleanupStage(a)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(ReleaseReservation(j)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(ReapJob(j)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(ScheduleRetry(j)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(FinalizeCancel(j)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(PublishCancelNotice(j)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(ClearStaleLiveProgress(j)))
|
|
|
|
|
/\ \A j \in Jobs : WF_vars(JobStep(CleanTerminalCoordination(j)))
|
|
|
|
|
/\ \A w \in Workers, s \in Services : WF_vars(JobStep(RestoreLink(w, s)))
|
|
|
|
|
/\ \A w \in Workers : WF_vars(JobStep(StartIncarnation(w)))
|
|
|
|
|
/\ WF_vars(JobStep(Tick))
|
|
|
|
|
|
|
|
|
|
SafetySpec == Init /\ [][Next]_vars
|
|
|
|
|
Spec == SafetySpec /\ Fairness
|
|
|
|
|
@ -891,6 +1022,44 @@ TypeOK ==
|
|
|
|
|
/\ resumedFromCheckpoint \in [AttemptIds -> BOOLEAN]
|
|
|
|
|
/\ stageState \in [AttemptIds -> StageStates]
|
|
|
|
|
/\ pendingOutcome \in [AttemptIds -> OutcomeRequests]
|
|
|
|
|
/\ credentialIntentState \in
|
|
|
|
|
[CredentialIntents -> CredentialIntentStates]
|
|
|
|
|
/\ vaultSecretState \in [CredentialIntents -> VaultSecretStates]
|
|
|
|
|
/\ credentialVersionDurable \in [CredentialIntents -> BOOLEAN]
|
|
|
|
|
|
|
|
|
|
CredentialLifecycleWellFormed ==
|
|
|
|
|
\A c \in CredentialIntents :
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentUnused =>
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretAbsent
|
|
|
|
|
/\ ~credentialVersionDurable[c])
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentPrepared =>
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretAbsent
|
|
|
|
|
/\ ~credentialVersionDurable[c])
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentWriting =>
|
|
|
|
|
/\ vaultSecretState[c] \in {VaultSecretAbsent, VaultSecretLive}
|
|
|
|
|
/\ ~credentialVersionDurable[c])
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentWritten =>
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretLive
|
|
|
|
|
/\ ~credentialVersionDurable[c])
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentCommitted =>
|
|
|
|
|
/\ vaultSecretState[c] \in
|
|
|
|
|
{VaultSecretLive, VaultSecretDestroyed}
|
|
|
|
|
/\ credentialVersionDurable[c])
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentAbandoning =>
|
|
|
|
|
/\ vaultSecretState[c] = VaultSecretLive
|
|
|
|
|
/\ ~credentialVersionDurable[c])
|
|
|
|
|
/\ (credentialIntentState[c] = CredentialIntentAbandoned =>
|
|
|
|
|
/\ vaultSecretState[c] \in
|
|
|
|
|
{VaultSecretAbsent, VaultSecretDestroyed}
|
|
|
|
|
/\ ~credentialVersionDurable[c])
|
|
|
|
|
|
|
|
|
|
NoOrphanSecrets ==
|
|
|
|
|
\A c \in CredentialIntents :
|
|
|
|
|
vaultSecretState[c] = VaultSecretLive =>
|
|
|
|
|
\/ credentialVersionDurable[c]
|
|
|
|
|
\/ credentialIntentState[c] \in
|
|
|
|
|
{CredentialIntentWriting, CredentialIntentWritten,
|
|
|
|
|
CredentialIntentAbandoning}
|
|
|
|
|
|
|
|
|
|
StateConsistency ==
|
|
|
|
|
/\ \A j \in Jobs :
|
|
|
|
|
|
