Serialize startup prepared artifact reclamation
This commit is contained in:
parent
acd0b4cc8c
commit
7cd8a90af0
1 changed files with 195 additions and 67 deletions
|
|
@ -45,10 +45,13 @@ VARIABLES
|
|||
selectionBinding,
|
||||
mounts,
|
||||
artifactBinding,
|
||||
gcRequested,
|
||||
gcObservation,
|
||||
replacementPresent,
|
||||
foreignObserved
|
||||
|
||||
FreshArtifactIncarnations ==
|
||||
ArtifactIncarnations \ {gcObservation[g] : g \in Generations}
|
||||
|
||||
vars == <<
|
||||
artifactState,
|
||||
artifactIncarnation,
|
||||
|
|
@ -59,7 +62,7 @@ vars == <<
|
|||
selectionBinding,
|
||||
mounts,
|
||||
artifactBinding,
|
||||
gcRequested,
|
||||
gcObservation,
|
||||
replacementPresent,
|
||||
foreignObserved
|
||||
>>
|
||||
|
|
@ -74,7 +77,7 @@ Init ==
|
|||
/\ selectionBinding = [g \in Generations |-> NoArtifact]
|
||||
/\ mounts = {}
|
||||
/\ artifactBinding = [g \in Generations |-> NoArtifact]
|
||||
/\ gcRequested = FALSE
|
||||
/\ gcObservation = [g \in Generations |-> NoArtifact]
|
||||
/\ replacementPresent = FALSE
|
||||
/\ foreignObserved = FALSE
|
||||
|
||||
|
|
@ -86,7 +89,7 @@ BeginPrepare(p) ==
|
|||
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = TRUE]
|
||||
/\ materializerState' = [materializerState EXCEPT ![p] = "Live"]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
|
||||
selectionBinding, mounts, artifactBinding, gcRequested,
|
||||
selectionBinding, mounts, artifactBinding, gcObservation,
|
||||
replacementPresent, foreignObserved>>
|
||||
|
||||
CreateOwnedStage(p) ==
|
||||
|
|
@ -96,7 +99,7 @@ CreateOwnedStage(p) ==
|
|||
/\ stageState' = [stageState EXCEPT ![p] = "Owned"]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, prepareIntent,
|
||||
materializerState, leases, selectionBinding, mounts, artifactBinding,
|
||||
gcRequested, replacementPresent, foreignObserved>>
|
||||
gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
LoseMaterializer(p) ==
|
||||
/\ prepareIntent[p]
|
||||
|
|
@ -104,24 +107,24 @@ LoseMaterializer(p) ==
|
|||
/\ materializerState' = [materializerState EXCEPT ![p] = "Lost"]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, leases, selectionBinding, mounts, artifactBinding,
|
||||
gcRequested, replacementPresent, foreignObserved>>
|
||||
gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
PublishArtifact(p) ==
|
||||
/\ artifactState = "Absent"
|
||||
/\ FreshArtifactIncarnations # {}
|
||||
/\ stageState[p] = "Owned"
|
||||
/\ prepareIntent[p]
|
||||
/\ materializerState[p] = "Live"
|
||||
/\ artifactState' = "Published"
|
||||
/\ artifactIncarnation' = A1
|
||||
/\ artifactIncarnation' \in FreshArtifactIncarnations
|
||||
/\ stageState' = [stageState EXCEPT ![p] = "Absent"]
|
||||
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
||||
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
||||
/\ UNCHANGED <<leases, selectionBinding, mounts, artifactBinding,
|
||||
gcRequested, replacementPresent, foreignObserved>>
|
||||
gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
ReusePublishedArtifact(p) ==
|
||||
/\ artifactState = "Published"
|
||||
/\ ~gcRequested
|
||||
/\ stageState[p] = "Owned"
|
||||
/\ prepareIntent[p]
|
||||
/\ materializerState[p] = "Live"
|
||||
|
|
@ -129,7 +132,7 @@ ReusePublishedArtifact(p) ==
|
|||
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
||||
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, leases,
|
||||
selectionBinding, mounts, artifactBinding, gcRequested,
|
||||
selectionBinding, mounts, artifactBinding, gcObservation,
|
||||
replacementPresent, foreignObserved>>
|
||||
|
||||
RecoverUnmaterializedIntent(p) ==
|
||||
|
|
@ -139,7 +142,7 @@ RecoverUnmaterializedIntent(p) ==
|
|||
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
||||
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
|
||||
selectionBinding, mounts, artifactBinding, gcRequested,
|
||||
selectionBinding, mounts, artifactBinding, gcObservation,
|
||||
replacementPresent, foreignObserved>>
|
||||
|
||||
RecoverOwnedStage(p) ==
|
||||
|
|
@ -150,7 +153,7 @@ RecoverOwnedStage(p) ==
|
|||
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
||||
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, leases,
|
||||
selectionBinding, mounts, artifactBinding, gcRequested,
|
||||
selectionBinding, mounts, artifactBinding, gcObservation,
|
||||
replacementPresent, foreignObserved>>
|
||||
|
||||
ObserveForeignStage(p) ==
|
||||
|
|
@ -161,7 +164,7 @@ ObserveForeignStage(p) ==
|
|||
/\ foreignObserved' = TRUE
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, prepareIntent,
|
||||
materializerState, leases, selectionBinding, mounts, artifactBinding,
|
||||
gcRequested, replacementPresent>>
|
||||
gcObservation, replacementPresent>>
|
||||
|
||||
RefuseForeignStage(p) ==
|
||||
/\ stageState[p] = "Foreign"
|
||||
|
|
@ -169,14 +172,13 @@ RefuseForeignStage(p) ==
|
|||
|
||||
SelectPublishedArtifact(g) ==
|
||||
/\ artifactState = "Published"
|
||||
/\ ~gcRequested
|
||||
/\ g \notin leases
|
||||
/\ selectionBinding[g] = NoArtifact
|
||||
/\ selectionBinding' =
|
||||
[selectionBinding EXCEPT ![g] = artifactIncarnation]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, mounts, artifactBinding,
|
||||
gcRequested, replacementPresent, foreignObserved>>
|
||||
gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
ReleaseSelection(g) ==
|
||||
/\ selectionBinding[g] # NoArtifact
|
||||
|
|
@ -184,18 +186,17 @@ ReleaseSelection(g) ==
|
|||
/\ selectionBinding' = [selectionBinding EXCEPT ![g] = NoArtifact]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, mounts, artifactBinding,
|
||||
gcRequested, replacementPresent, foreignObserved>>
|
||||
gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
AcquireLease(g) ==
|
||||
/\ artifactState = "Published"
|
||||
/\ ~gcRequested
|
||||
/\ g \notin leases
|
||||
/\ selectionBinding[g] = artifactIncarnation
|
||||
/\ leases' = leases \cup {g}
|
||||
/\ selectionBinding' = [selectionBinding EXCEPT ![g] = NoArtifact]
|
||||
/\ artifactBinding' = [artifactBinding EXCEPT ![g] = Artifact]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState, prepareIntent,
|
||||
materializerState, mounts, gcRequested, replacementPresent,
|
||||
materializerState, mounts, gcObservation, replacementPresent,
|
||||
foreignObserved>>
|
||||
|
||||
MountStateAnchor(g) ==
|
||||
|
|
@ -205,14 +206,14 @@ MountStateAnchor(g) ==
|
|||
/\ mounts' = mounts \cup {g}
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, selectionBinding,
|
||||
artifactBinding, gcRequested, replacementPresent, foreignObserved>>
|
||||
artifactBinding, gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
UnmountStateAnchor(g) ==
|
||||
/\ g \in mounts
|
||||
/\ mounts' = mounts \ {g}
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, selectionBinding,
|
||||
artifactBinding, gcRequested, replacementPresent, foreignObserved>>
|
||||
artifactBinding, gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
ReleaseLease(g) ==
|
||||
/\ g \in leases
|
||||
|
|
@ -221,43 +222,60 @@ ReleaseLease(g) ==
|
|||
/\ artifactBinding' = [artifactBinding EXCEPT ![g] = NoArtifact]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, selectionBinding, mounts,
|
||||
gcRequested, replacementPresent, foreignObserved>>
|
||||
gcObservation, replacementPresent, foreignObserved>>
|
||||
|
||||
RequestGC ==
|
||||
ObserveGCCandidate(g) ==
|
||||
/\ artifactState = "Published"
|
||||
/\ leases = {}
|
||||
/\ \A g \in Generations : selectionBinding[g] = NoArtifact
|
||||
/\ ~gcRequested
|
||||
/\ gcRequested' = TRUE
|
||||
/\ \A selected \in Generations :
|
||||
selectionBinding[selected] = NoArtifact
|
||||
/\ gcObservation[g] = NoArtifact
|
||||
/\ gcObservation' =
|
||||
[gcObservation EXCEPT ![g] = artifactIncarnation]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, selectionBinding, mounts,
|
||||
artifactBinding, replacementPresent, foreignObserved>>
|
||||
|
||||
PublishReplacementDuringGC ==
|
||||
/\ artifactState = "Published"
|
||||
/\ gcRequested
|
||||
/\ \E g \in Generations :
|
||||
gcObservation[g] = artifactIncarnation
|
||||
/\ (IF artifactIncarnation = A1 THEN A2 ELSE A1)
|
||||
\in FreshArtifactIncarnations
|
||||
/\ ~replacementPresent
|
||||
/\ replacementPresent' = TRUE
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, selectionBinding, mounts,
|
||||
artifactBinding, gcRequested, foreignObserved>>
|
||||
artifactBinding, gcObservation, foreignObserved>>
|
||||
|
||||
ReclaimArtifact ==
|
||||
ReclaimObservedArtifact(g) ==
|
||||
/\ artifactState = "Published"
|
||||
/\ gcRequested
|
||||
/\ gcObservation[g] = artifactIncarnation
|
||||
/\ leases = {}
|
||||
/\ \A g \in Generations : selectionBinding[g] = NoArtifact
|
||||
/\ \A selected \in Generations :
|
||||
selectionBinding[selected] = NoArtifact
|
||||
/\ mounts = {}
|
||||
/\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent"
|
||||
/\ artifactIncarnation' =
|
||||
IF replacementPresent
|
||||
THEN IF artifactIncarnation = A1 THEN A2 ELSE A1
|
||||
ELSE NoArtifact
|
||||
/\ gcRequested' = FALSE
|
||||
/\ gcObservation' =
|
||||
[gcObservation EXCEPT ![g] = NoArtifact]
|
||||
/\ replacementPresent' = FALSE
|
||||
/\ UNCHANGED <<stageState, prepareIntent, materializerState, leases,
|
||||
selectionBinding, mounts, artifactBinding, foreignObserved>>
|
||||
|
||||
ConvergeCompletedReclaim(g) ==
|
||||
/\ gcObservation[g] # NoArtifact
|
||||
/\ \/ artifactState = "Absent"
|
||||
\/ gcObservation[g] # artifactIncarnation
|
||||
/\ gcObservation' =
|
||||
[gcObservation EXCEPT ![g] = NoArtifact]
|
||||
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
||||
prepareIntent, materializerState, leases, selectionBinding, mounts,
|
||||
artifactBinding, replacementPresent, foreignObserved>>
|
||||
|
||||
Next ==
|
||||
\/ (\E p \in Preparations : BeginPrepare(p))
|
||||
\/ (\E p \in Preparations : CreateOwnedStage(p))
|
||||
|
|
@ -274,9 +292,10 @@ Next ==
|
|||
\/ (\E g \in Generations : MountStateAnchor(g))
|
||||
\/ (\E g \in Generations : UnmountStateAnchor(g))
|
||||
\/ (\E g \in Generations : ReleaseLease(g))
|
||||
\/ RequestGC
|
||||
\/ (\E g \in Generations : ObserveGCCandidate(g))
|
||||
\/ PublishReplacementDuringGC
|
||||
\/ ReclaimArtifact
|
||||
\/ (\E g \in Generations : ReclaimObservedArtifact(g))
|
||||
\/ (\E g \in Generations : ConvergeCompletedReclaim(g))
|
||||
|
||||
Spec == Init /\ [][Next]_vars
|
||||
|
||||
|
|
@ -291,7 +310,8 @@ TypeOK ==
|
|||
[Generations -> ArtifactIncarnations \cup {NoArtifact}]
|
||||
/\ mounts \subseteq Generations
|
||||
/\ artifactBinding \in [Generations -> {NoArtifact, Artifact}]
|
||||
/\ gcRequested \in BOOLEAN
|
||||
/\ gcObservation \in
|
||||
[Generations -> ArtifactIncarnations \cup {NoArtifact}]
|
||||
/\ replacementPresent \in BOOLEAN
|
||||
/\ foreignObserved \in BOOLEAN
|
||||
|
||||
|
|
@ -332,7 +352,6 @@ LostIntentRecoverable ==
|
|||
PublishedOwnedStageReusable ==
|
||||
\A p \in Preparations :
|
||||
/\ artifactState = "Published"
|
||||
/\ ~gcRequested
|
||||
/\ materializerState[p] = "Live"
|
||||
/\ stageState[p] = "Owned"
|
||||
=> ENABLED ReusePublishedArtifact(p)
|
||||
|
|
@ -348,24 +367,36 @@ MountedGenerationLeased ==
|
|||
LeasedArtifactPublished ==
|
||||
leases # {} => artifactState = "Published"
|
||||
|
||||
GCExcludesLeases ==
|
||||
gcRequested =>
|
||||
/\ artifactState = "Published"
|
||||
/\ leases = {}
|
||||
/\ mounts = {}
|
||||
GCReclaimExcludesLeases ==
|
||||
\A g \in Generations :
|
||||
ENABLED ReclaimObservedArtifact(g) =>
|
||||
/\ leases = {}
|
||||
/\ mounts = {}
|
||||
|
||||
GCExcludesSelections ==
|
||||
gcRequested =>
|
||||
\A g \in Generations : selectionBinding[g] = NoArtifact
|
||||
GCReclaimExcludesSelections ==
|
||||
\A g \in Generations :
|
||||
ENABLED ReclaimObservedArtifact(g) =>
|
||||
\A selected \in Generations :
|
||||
selectionBinding[selected] = NoArtifact
|
||||
|
||||
SelectedArtifactStable ==
|
||||
\A g \in Generations :
|
||||
selectionBinding[g] # NoArtifact =>
|
||||
/\ ~ENABLED RequestGC
|
||||
/\ ~ENABLED ReclaimArtifact
|
||||
\A observer \in Generations :
|
||||
~ENABLED ReclaimObservedArtifact(observer)
|
||||
|
||||
CompletedReclaimConverges ==
|
||||
\A g \in Generations :
|
||||
/\ gcObservation[g] # NoArtifact
|
||||
/\ \/ artifactState = "Absent"
|
||||
\/ gcObservation[g] # artifactIncarnation
|
||||
=> /\ ENABLED ConvergeCompletedReclaim(g)
|
||||
/\ ~ENABLED ReclaimObservedArtifact(g)
|
||||
|
||||
ReplacementOnlyDuringGC ==
|
||||
replacementPresent => gcRequested
|
||||
replacementPresent =>
|
||||
\E g \in Generations :
|
||||
gcObservation[g] = artifactIncarnation
|
||||
|
||||
ForeignStagePreserved ==
|
||||
foreignObserved => \E p \in Preparations : stageState[p] = "Foreign"
|
||||
|
|
|
|||
Loading…
Reference in a new issue