279 lines
14 KiB
Text
279 lines
14 KiB
Text
---- MODULE MirroredImage ----
|
|
EXTENDS Naturals, FiniteSets, TLC
|
|
|
|
CONSTANTS Tagged, Safe, AllowRemoval, AllowFailure, AllowRetry, RetryStageSet, MaxEpoch, MaxRetries
|
|
|
|
Stages == {"prepare", "promotion", "cleanup"}
|
|
Repos == {"candidate", "mirror"}
|
|
Children == {"amd64", "arm64"}
|
|
Phases == {"absent", "pending", "queued", "running", "published", "succeeded", "failed"}
|
|
Terminal(p) == p \in {"succeeded", "failed"}
|
|
|
|
VARIABLES desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount, retryAck,
|
|
cleanupObserved, grace, epoch, retryStage, badPromotion
|
|
|
|
vars == <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount, retryAck,
|
|
cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Available(r) == stored[r] /\ (temporary[r] \/ durableTags[r] # {})
|
|
Active == \E s \in Stages : attempts[s] # "absent" /\ ~Terminal(attempts[s])
|
|
|
|
Init ==
|
|
/\ desired = TRUE
|
|
/\ managed = FALSE
|
|
/\ retired = FALSE
|
|
/\ attempts = [s \in Stages |-> "absent"]
|
|
/\ workflows = [s \in Stages |-> "absent"]
|
|
/\ scanned = {}
|
|
/\ verdict = "pending"
|
|
/\ stored = [r \in Repos |-> FALSE]
|
|
/\ temporary = [r \in Repos |-> FALSE]
|
|
/\ durableTags = [r \in Repos |-> {}]
|
|
/\ promoted = FALSE
|
|
/\ copies = 0
|
|
/\ retryCount = 0
|
|
/\ retryAck = FALSE
|
|
/\ cleanupObserved = FALSE
|
|
/\ grace = [r \in Repos |-> FALSE]
|
|
/\ epoch = 1
|
|
/\ retryStage = "none" /\ badPromotion = FALSE
|
|
|
|
Manage ==
|
|
/\ desired /\ ~managed /\ ~retired
|
|
/\ managed' = TRUE
|
|
/\ UNCHANGED <<desired, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Plan(s) ==
|
|
/\ managed /\ ~Active /\ attempts[s] = "absent"
|
|
/\ CASE s = "prepare" -> desired /\ attempts["cleanup"] = "absent"
|
|
[] s = "promotion" -> desired /\ attempts["cleanup"] = "absent"
|
|
/\ attempts["prepare"] = "succeeded" /\ verdict = "accepted"
|
|
[] s = "cleanup" -> ~desired
|
|
/\ attempts' = [attempts EXCEPT ![s] = "pending"]
|
|
/\ UNCHANGED <<desired, managed, retired, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Submit(s) ==
|
|
/\ attempts[s] = "pending" /\ workflows[s] = "absent"
|
|
/\ s = "cleanup" => \A t \in {"prepare", "promotion"} : attempts[t] = "absent" \/ Terminal(attempts[t])
|
|
/\ workflows' = [workflows EXCEPT ![s] = "queued"]
|
|
/\ retryAck' = (retryAck \/ (retryCount > 0 /\ s = retryStage))
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Start(s) ==
|
|
/\ workflows[s] = "queued"
|
|
/\ ~\E t \in Stages : workflows[t] \in {"running", "published"}
|
|
/\ workflows' = [workflows EXCEPT ![s] = "running"]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
PartialCopy(s) ==
|
|
/\ s \in {"prepare", "promotion"} /\ workflows[s] = "running"
|
|
/\ s = "promotion" => Available("candidate")
|
|
/\ LET r == IF s = "prepare" THEN "candidate" ELSE "mirror"
|
|
IN /\ ~stored[r]
|
|
/\ stored' = [stored EXCEPT ![r] = TRUE]
|
|
/\ temporary' = [temporary EXCEPT ![r] = TRUE]
|
|
/\ grace' = [grace EXCEPT ![r] = FALSE]
|
|
/\ badPromotion' = (badPromotion \/ (s = "promotion" /\ (~Safe \/ verdict # "accepted" \/ scanned # Children)))
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
durableTags, promoted, copies, retryCount, retryAck,
|
|
cleanupObserved, epoch, retryStage>>
|
|
|
|
Publish(s) ==
|
|
/\ s \in {"prepare", "promotion"} /\ workflows[s] = "running"
|
|
/\ s = "promotion" => Available("candidate")
|
|
/\ LET r == IF s = "prepare" THEN "candidate" ELSE "mirror"
|
|
IN /\ stored' = [stored EXCEPT ![r] = TRUE]
|
|
/\ temporary' = [temporary EXCEPT ![r] = TRUE]
|
|
/\ durableTags' = [durableTags EXCEPT ![r] = @ \cup {"retention"}]
|
|
/\ grace' = [grace EXCEPT ![r] = FALSE]
|
|
/\ promoted' = (promoted \/ (s = "promotion" /\ attempts["cleanup"] = "absent"))
|
|
/\ copies' = IF s = "promotion" THEN copies + 1 ELSE copies
|
|
/\ badPromotion' = (badPromotion \/ (s = "promotion" /\ (~Safe \/ verdict # "accepted" \/ scanned # Children)))
|
|
/\ workflows' = [workflows EXCEPT ![s] = "published"]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
|
|
retryCount, retryAck, cleanupObserved, epoch, retryStage>>
|
|
|
|
Alias(s) ==
|
|
/\ Tagged /\ s \in {"prepare", "promotion"} /\ workflows[s] = "published"
|
|
/\ LET r == IF s = "prepare" THEN "candidate" ELSE "mirror"
|
|
IN /\ "declared" \notin durableTags[r]
|
|
/\ durableTags' = [durableTags EXCEPT ![r] = @ \cup {"declared"}]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, promoted, copies, retryCount, retryAck,
|
|
cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Delete(r) ==
|
|
/\ workflows["cleanup"] = "running"
|
|
/\ durableTags[r] # {}
|
|
/\ durableTags' = [durableTags EXCEPT ![r] = {}]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, promoted, copies, retryCount, retryAck,
|
|
cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Finish(s, success) ==
|
|
/\ workflows[s] \in {"running", "published"}
|
|
/\ success \/ AllowFailure \/ (s = "promotion" /\ ~Available("candidate"))
|
|
/\ success => IF s = "cleanup" THEN \A r \in Repos : durableTags[r] = {}
|
|
ELSE /\ workflows[s] = "published"
|
|
/\ Tagged => "declared" \in durableTags[IF s = "prepare" THEN "candidate" ELSE "mirror"]
|
|
/\ workflows' = [workflows EXCEPT ![s] = IF success THEN "succeeded" ELSE "failed"]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Observe(s) ==
|
|
/\ attempts[s] = "pending" /\ Terminal(workflows[s])
|
|
/\ attempts' = [attempts EXCEPT ![s] = workflows[s]]
|
|
/\ UNCHANGED <<desired, managed, retired, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Scan(c) ==
|
|
/\ desired /\ attempts["prepare"] = "succeeded"
|
|
/\ attempts["cleanup"] = "absent" /\ verdict = "pending"
|
|
/\ Available("candidate") /\ c \notin scanned
|
|
/\ scanned' = scanned \cup {c}
|
|
/\ verdict' = IF ~Safe /\ c = "arm64" THEN "rejected"
|
|
ELSE IF scanned' = Children THEN "accepted" ELSE "pending"
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Expire(r) ==
|
|
/\ temporary[r]
|
|
/\ temporary' = [temporary EXCEPT ![r] = FALSE]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Age(r) ==
|
|
/\ stored[r] /\ ~Available(r) /\ ~grace[r]
|
|
/\ grace' = [grace EXCEPT ![r] = TRUE]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, epoch, retryStage, badPromotion>>
|
|
|
|
Collect(r) ==
|
|
/\ stored[r] /\ ~Available(r) /\ grace[r]
|
|
/\ stored' = [stored EXCEPT ![r] = FALSE]
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Remove ==
|
|
/\ AllowRemoval /\ desired
|
|
/\ desired' = FALSE
|
|
/\ UNCHANGED <<managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, promoted, copies, retryCount,
|
|
retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Forget ==
|
|
/\ managed /\ ~Active /\ attempts["cleanup"] = "succeeded"
|
|
/\ \A r \in Repos : ~stored[r]
|
|
/\ managed' = desired
|
|
/\ retired' = ~desired
|
|
/\ cleanupObserved' = ~desired
|
|
/\ attempts' = IF desired THEN [s \in Stages |-> "absent"] ELSE attempts
|
|
/\ workflows' = IF desired THEN [s \in Stages |-> "absent"] ELSE workflows
|
|
/\ scanned' = IF desired THEN {} ELSE scanned
|
|
/\ verdict' = IF desired THEN "pending" ELSE verdict
|
|
/\ promoted' = IF desired THEN FALSE ELSE promoted
|
|
/\ retryAck' = IF desired THEN FALSE ELSE retryAck
|
|
/\ UNCHANGED <<desired, stored, temporary, durableTags, copies, retryCount, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Readd ==
|
|
/\ ~desired /\ epoch < MaxEpoch
|
|
/\ desired' = TRUE /\ epoch' = epoch + 1
|
|
/\ retired' = FALSE /\ promoted' = FALSE /\ cleanupObserved' = FALSE
|
|
/\ attempts' = IF managed THEN attempts ELSE [s \in Stages |-> "absent"]
|
|
/\ workflows' = IF managed THEN workflows ELSE [s \in Stages |-> "absent"]
|
|
/\ scanned' = IF managed THEN scanned ELSE {}
|
|
/\ verdict' = IF managed THEN verdict ELSE "pending"
|
|
/\ retryAck' = IF managed THEN retryAck ELSE FALSE
|
|
/\ UNCHANGED <<managed, stored, temporary, durableTags, copies, retryCount, grace, retryStage, badPromotion>>
|
|
|
|
ObservePromoted ==
|
|
/\ desired /\ ~promoted /\ attempts["promotion"] = "succeeded"
|
|
/\ attempts["cleanup"] = "absent" /\ Available("mirror")
|
|
/\ promoted' = TRUE
|
|
/\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
|
|
stored, temporary, durableTags, copies, retryCount, retryAck,
|
|
cleanupObserved, grace, epoch, retryStage, badPromotion>>
|
|
|
|
Retry(s) ==
|
|
/\ AllowRetry /\ retryCount < MaxRetries /\ managed /\ ~Active
|
|
/\ Terminal(attempts[s])
|
|
/\ attempts' = [t \in Stages |->
|
|
IF t = s THEN "pending"
|
|
ELSE IF s = "prepare" /\ t = "promotion" THEN "absent"
|
|
ELSE IF t = "cleanup" /\ attempts[t] # "absent" THEN "pending"
|
|
ELSE attempts[t]]
|
|
/\ workflows' = [t \in Stages |->
|
|
IF t = s \/ (s = "prepare" /\ t = "promotion") \/ t = "cleanup"
|
|
THEN "absent" ELSE workflows[t]]
|
|
/\ scanned' = IF s = "prepare" THEN {} ELSE scanned
|
|
/\ verdict' = IF s = "prepare" THEN "pending" ELSE verdict
|
|
/\ retryCount' = retryCount + 1
|
|
/\ retryStage' = s
|
|
/\ retryAck' = FALSE
|
|
/\ UNCHANGED <<desired, managed, retired,
|
|
stored, temporary, durableTags, promoted, copies,
|
|
cleanupObserved, grace, epoch, badPromotion>>
|
|
|
|
Next ==
|
|
\/ Manage
|
|
\/ \E s \in Stages : Plan(s) \/ Submit(s) \/ Start(s) \/ Observe(s)
|
|
\/ \E success \in BOOLEAN : Finish(s, success)
|
|
\/ \E s \in {"prepare", "promotion"} : PartialCopy(s) \/ Publish(s) \/ Alias(s)
|
|
\/ \E r \in Repos : Delete(r) \/ Expire(r) \/ Age(r) \/ Collect(r)
|
|
\/ \E c \in Children : Scan(c)
|
|
\/ Remove \/ Forget \/ (\E s \in RetryStageSet : Retry(s)) \/ Readd \/ ObservePromoted
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
FairSpec == Spec
|
|
/\ WF_vars(Manage) /\ WF_vars(Forget) /\ WF_vars(ObservePromoted)
|
|
/\ (\A s \in Stages : WF_vars(Plan(s)) /\ WF_vars(Submit(s))
|
|
/\ WF_vars(Start(s)) /\ WF_vars(Observe(s))
|
|
/\ WF_vars(Finish(s, TRUE) \/ Finish(s, FALSE)))
|
|
/\ (\A s \in {"prepare", "promotion"} : WF_vars(Publish(s)) /\ WF_vars(Alias(s)))
|
|
/\ (\A r \in Repos : WF_vars(Delete(r)) /\ WF_vars(Expire(r))
|
|
/\ WF_vars(Age(r)) /\ WF_vars(Collect(r)))
|
|
/\ (\A c \in Children : WF_vars(Scan(c)))
|
|
|
|
TypeOK ==
|
|
/\ desired \in BOOLEAN /\ managed \in BOOLEAN /\ retired \in BOOLEAN
|
|
/\ attempts \in [Stages -> Phases] /\ workflows \in [Stages -> Phases]
|
|
/\ scanned \subseteq Children /\ verdict \in {"pending", "accepted", "rejected"}
|
|
/\ stored \in [Repos -> BOOLEAN] /\ temporary \in [Repos -> BOOLEAN]
|
|
/\ durableTags \in [Repos -> SUBSET {"retention", "declared", "retry"}]
|
|
/\ promoted \in BOOLEAN /\ copies \in Nat /\ epoch \in 1..MaxEpoch
|
|
/\ retryCount \in 0..MaxRetries /\ retryAck \in BOOLEAN
|
|
/\ retryStage \in Stages \cup {"none"} /\ badPromotion \in BOOLEAN
|
|
/\ cleanupObserved \in BOOLEAN /\ grace \in [Repos -> BOOLEAN]
|
|
|
|
PromotionRequiresAcceptance == ~badPromotion
|
|
DeclaredPromotionRetained == desired /\ promoted => Available("mirror")
|
|
DeclaredCandidateRetained == desired /\ attempts["cleanup"] = "absent" /\ attempts["prepare"] = "succeeded" => Available("candidate")
|
|
CleanupObservedMeansGone == cleanupObserved => \A r \in Repos : ~stored[r]
|
|
DeclaredAliasOnlyWhenRequested == ~Tagged => \A r \in Repos : "declared" \notin durableTags[r]
|
|
RetryPreservesTagIdentity == \A r \in Repos : durableTags[r] \subseteq {"retention", "declared"}
|
|
RetryAcknowledgedAfterCreation == retryAck => retryStage # "none" /\ workflows[retryStage] # "absent"
|
|
CleanupExcludesCopy == workflows["cleanup"] \in {"running", "published"} =>
|
|
\A s \in {"prepare", "promotion"} : workflows[s] \notin {"running", "published"}
|
|
|
|
EventuallyPromoted == (desired /\ managed) ~> (~desired \/ promoted)
|
|
EventuallyRetired == (~desired /\ managed) ~> (retired \/ desired)
|
|
EventuallyRejected == <>(verdict = "rejected")
|
|
|
|
====
|