373 lines
13 KiB
Text
373 lines
13 KiB
Text
------------------------- MODULE PreparedLower -------------------------
|
|
EXTENDS FiniteSets, TLC
|
|
|
|
(***************************************************************************
|
|
Artifact-level refinement for concurrent prepared-lower publication,
|
|
materializer-loss recovery, generation leases, State Anchor use, and reclaim.
|
|
***************************************************************************)
|
|
|
|
CONSTANTS
|
|
Generations,
|
|
Preparations,
|
|
Artifact,
|
|
NoArtifact,
|
|
G1,
|
|
G2,
|
|
P1,
|
|
P2,
|
|
A1,
|
|
A2
|
|
|
|
ASSUME
|
|
/\ Generations = {G1, G2}
|
|
/\ G1 # G2
|
|
/\ Preparations = {P1, P2}
|
|
/\ P1 # P2
|
|
/\ NoArtifact # Artifact
|
|
/\ A1 # A2
|
|
/\ NoArtifact \notin {A1, A2}
|
|
/\ Artifact \notin {A1, A2}
|
|
|
|
ArtifactStates == {"Absent", "Published"}
|
|
ArtifactIncarnations == {A1, A2}
|
|
StageStates == {"Absent", "Owned", "Foreign"}
|
|
MaterializerStates == {"Absent", "Live", "Lost"}
|
|
GenerationsFixture == {G1, G2}
|
|
PreparationsFixture == {P1, P2}
|
|
|
|
VARIABLES
|
|
artifactState,
|
|
artifactIncarnation,
|
|
stageState,
|
|
prepareIntent,
|
|
materializerState,
|
|
leases,
|
|
selectionBinding,
|
|
mounts,
|
|
artifactBinding,
|
|
gcRequested,
|
|
replacementPresent,
|
|
foreignObserved
|
|
|
|
vars == <<
|
|
artifactState,
|
|
artifactIncarnation,
|
|
stageState,
|
|
prepareIntent,
|
|
materializerState,
|
|
leases,
|
|
selectionBinding,
|
|
mounts,
|
|
artifactBinding,
|
|
gcRequested,
|
|
replacementPresent,
|
|
foreignObserved
|
|
>>
|
|
|
|
Init ==
|
|
/\ artifactState = "Absent"
|
|
/\ artifactIncarnation = NoArtifact
|
|
/\ stageState = [p \in Preparations |-> "Absent"]
|
|
/\ prepareIntent = [p \in Preparations |-> FALSE]
|
|
/\ materializerState = [p \in Preparations |-> "Absent"]
|
|
/\ leases = {}
|
|
/\ selectionBinding = [g \in Generations |-> NoArtifact]
|
|
/\ mounts = {}
|
|
/\ artifactBinding = [g \in Generations |-> NoArtifact]
|
|
/\ gcRequested = FALSE
|
|
/\ replacementPresent = FALSE
|
|
/\ foreignObserved = FALSE
|
|
|
|
BeginPrepare(p) ==
|
|
/\ artifactState = "Absent"
|
|
/\ stageState[p] = "Absent"
|
|
/\ ~prepareIntent[p]
|
|
/\ materializerState[p] = "Absent"
|
|
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = TRUE]
|
|
/\ materializerState' = [materializerState EXCEPT ![p] = "Live"]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
|
|
selectionBinding, mounts, artifactBinding, gcRequested,
|
|
replacementPresent, foreignObserved>>
|
|
|
|
CreateOwnedStage(p) ==
|
|
/\ stageState[p] = "Absent"
|
|
/\ prepareIntent[p]
|
|
/\ materializerState[p] = "Live"
|
|
/\ stageState' = [stageState EXCEPT ![p] = "Owned"]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, prepareIntent,
|
|
materializerState, leases, selectionBinding, mounts, artifactBinding,
|
|
gcRequested, replacementPresent, foreignObserved>>
|
|
|
|
LoseMaterializer(p) ==
|
|
/\ prepareIntent[p]
|
|
/\ materializerState[p] = "Live"
|
|
/\ materializerState' = [materializerState EXCEPT ![p] = "Lost"]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, leases, selectionBinding, mounts, artifactBinding,
|
|
gcRequested, replacementPresent, foreignObserved>>
|
|
|
|
PublishArtifact(p) ==
|
|
/\ artifactState = "Absent"
|
|
/\ stageState[p] = "Owned"
|
|
/\ prepareIntent[p]
|
|
/\ materializerState[p] = "Live"
|
|
/\ artifactState' = "Published"
|
|
/\ artifactIncarnation' = A1
|
|
/\ stageState' = [stageState EXCEPT ![p] = "Absent"]
|
|
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
|
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
|
/\ UNCHANGED <<leases, selectionBinding, mounts, artifactBinding,
|
|
gcRequested, replacementPresent, foreignObserved>>
|
|
|
|
ReusePublishedArtifact(p) ==
|
|
/\ artifactState = "Published"
|
|
/\ ~gcRequested
|
|
/\ stageState[p] = "Owned"
|
|
/\ prepareIntent[p]
|
|
/\ materializerState[p] = "Live"
|
|
/\ stageState' = [stageState EXCEPT ![p] = "Absent"]
|
|
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
|
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, leases,
|
|
selectionBinding, mounts, artifactBinding, gcRequested,
|
|
replacementPresent, foreignObserved>>
|
|
|
|
RecoverUnmaterializedIntent(p) ==
|
|
/\ stageState[p] = "Absent"
|
|
/\ prepareIntent[p]
|
|
/\ materializerState[p] = "Lost"
|
|
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
|
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
|
|
selectionBinding, mounts, artifactBinding, gcRequested,
|
|
replacementPresent, foreignObserved>>
|
|
|
|
RecoverOwnedStage(p) ==
|
|
/\ stageState[p] = "Owned"
|
|
/\ prepareIntent[p]
|
|
/\ materializerState[p] = "Lost"
|
|
/\ stageState' = [stageState EXCEPT ![p] = "Absent"]
|
|
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
|
|
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, leases,
|
|
selectionBinding, mounts, artifactBinding, gcRequested,
|
|
replacementPresent, foreignObserved>>
|
|
|
|
ObserveForeignStage(p) ==
|
|
/\ stageState[p] = "Absent"
|
|
/\ ~prepareIntent[p]
|
|
/\ materializerState[p] = "Absent"
|
|
/\ stageState' = [stageState EXCEPT ![p] = "Foreign"]
|
|
/\ foreignObserved' = TRUE
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, prepareIntent,
|
|
materializerState, leases, selectionBinding, mounts, artifactBinding,
|
|
gcRequested, replacementPresent>>
|
|
|
|
RefuseForeignStage(p) ==
|
|
/\ stageState[p] = "Foreign"
|
|
/\ UNCHANGED vars
|
|
|
|
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>>
|
|
|
|
ReleaseSelection(g) ==
|
|
/\ selectionBinding[g] # NoArtifact
|
|
/\ g \notin leases
|
|
/\ selectionBinding' = [selectionBinding EXCEPT ![g] = NoArtifact]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, materializerState, leases, mounts, artifactBinding,
|
|
gcRequested, 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,
|
|
foreignObserved>>
|
|
|
|
MountStateAnchor(g) ==
|
|
/\ g \in leases
|
|
/\ artifactBinding[g] = Artifact
|
|
/\ g \notin mounts
|
|
/\ mounts' = mounts \cup {g}
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, materializerState, leases, selectionBinding,
|
|
artifactBinding, gcRequested, replacementPresent, foreignObserved>>
|
|
|
|
UnmountStateAnchor(g) ==
|
|
/\ g \in mounts
|
|
/\ mounts' = mounts \ {g}
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, materializerState, leases, selectionBinding,
|
|
artifactBinding, gcRequested, replacementPresent, foreignObserved>>
|
|
|
|
ReleaseLease(g) ==
|
|
/\ g \in leases
|
|
/\ g \notin mounts
|
|
/\ leases' = leases \ {g}
|
|
/\ artifactBinding' = [artifactBinding EXCEPT ![g] = NoArtifact]
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, materializerState, selectionBinding, mounts,
|
|
gcRequested, replacementPresent, foreignObserved>>
|
|
|
|
RequestGC ==
|
|
/\ artifactState = "Published"
|
|
/\ leases = {}
|
|
/\ \A g \in Generations : selectionBinding[g] = NoArtifact
|
|
/\ ~gcRequested
|
|
/\ gcRequested' = TRUE
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, materializerState, leases, selectionBinding, mounts,
|
|
artifactBinding, replacementPresent, foreignObserved>>
|
|
|
|
PublishReplacementDuringGC ==
|
|
/\ artifactState = "Published"
|
|
/\ gcRequested
|
|
/\ ~replacementPresent
|
|
/\ replacementPresent' = TRUE
|
|
/\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
|
|
prepareIntent, materializerState, leases, selectionBinding, mounts,
|
|
artifactBinding, gcRequested, foreignObserved>>
|
|
|
|
ReclaimArtifact ==
|
|
/\ artifactState = "Published"
|
|
/\ gcRequested
|
|
/\ leases = {}
|
|
/\ \A g \in Generations : selectionBinding[g] = NoArtifact
|
|
/\ mounts = {}
|
|
/\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent"
|
|
/\ artifactIncarnation' =
|
|
IF replacementPresent
|
|
THEN IF artifactIncarnation = A1 THEN A2 ELSE A1
|
|
ELSE NoArtifact
|
|
/\ gcRequested' = FALSE
|
|
/\ replacementPresent' = FALSE
|
|
/\ UNCHANGED <<stageState, prepareIntent, materializerState, leases,
|
|
selectionBinding, mounts, artifactBinding, foreignObserved>>
|
|
|
|
Next ==
|
|
\/ (\E p \in Preparations : BeginPrepare(p))
|
|
\/ (\E p \in Preparations : CreateOwnedStage(p))
|
|
\/ (\E p \in Preparations : LoseMaterializer(p))
|
|
\/ (\E p \in Preparations : PublishArtifact(p))
|
|
\/ (\E p \in Preparations : ReusePublishedArtifact(p))
|
|
\/ (\E p \in Preparations : RecoverUnmaterializedIntent(p))
|
|
\/ (\E p \in Preparations : RecoverOwnedStage(p))
|
|
\/ (\E p \in Preparations : ObserveForeignStage(p))
|
|
\/ (\E p \in Preparations : RefuseForeignStage(p))
|
|
\/ (\E g \in Generations : SelectPublishedArtifact(g))
|
|
\/ (\E g \in Generations : ReleaseSelection(g))
|
|
\/ (\E g \in Generations : AcquireLease(g))
|
|
\/ (\E g \in Generations : MountStateAnchor(g))
|
|
\/ (\E g \in Generations : UnmountStateAnchor(g))
|
|
\/ (\E g \in Generations : ReleaseLease(g))
|
|
\/ RequestGC
|
|
\/ PublishReplacementDuringGC
|
|
\/ ReclaimArtifact
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
TypeOK ==
|
|
/\ artifactState \in ArtifactStates
|
|
/\ artifactIncarnation \in ArtifactIncarnations \cup {NoArtifact}
|
|
/\ stageState \in [Preparations -> StageStates]
|
|
/\ prepareIntent \in [Preparations -> BOOLEAN]
|
|
/\ materializerState \in [Preparations -> MaterializerStates]
|
|
/\ leases \subseteq Generations
|
|
/\ selectionBinding \in
|
|
[Generations -> ArtifactIncarnations \cup {NoArtifact}]
|
|
/\ mounts \subseteq Generations
|
|
/\ artifactBinding \in [Generations -> {NoArtifact, Artifact}]
|
|
/\ gcRequested \in BOOLEAN
|
|
/\ replacementPresent \in BOOLEAN
|
|
/\ foreignObserved \in BOOLEAN
|
|
|
|
PrepareOwnershipConsistent ==
|
|
\A p \in Preparations :
|
|
/\ prepareIntent[p] <=> materializerState[p] # "Absent"
|
|
/\ stageState[p] = "Owned" => prepareIntent[p]
|
|
/\ stageState[p] = "Foreign" =>
|
|
/\ ~prepareIntent[p]
|
|
/\ materializerState[p] = "Absent"
|
|
|
|
ArtifactIncarnationConsistent ==
|
|
(artifactState = "Absent") <=> (artifactIncarnation = NoArtifact)
|
|
|
|
SelectionBindingConsistent ==
|
|
\A g \in Generations :
|
|
selectionBinding[g] # NoArtifact =>
|
|
/\ artifactState = "Published"
|
|
/\ selectionBinding[g] = artifactIncarnation
|
|
/\ g \notin leases
|
|
|
|
LiveOwnedStageNotRecoverable ==
|
|
\A p \in Preparations :
|
|
materializerState[p] = "Live" => ~ENABLED RecoverOwnedStage(p)
|
|
|
|
LostOwnedStageRecoverable ==
|
|
\A p \in Preparations :
|
|
/\ materializerState[p] = "Lost"
|
|
/\ stageState[p] = "Owned"
|
|
=> ENABLED RecoverOwnedStage(p)
|
|
|
|
LostIntentRecoverable ==
|
|
\A p \in Preparations :
|
|
/\ materializerState[p] = "Lost"
|
|
/\ stageState[p] = "Absent"
|
|
=> ENABLED RecoverUnmaterializedIntent(p)
|
|
|
|
PublishedOwnedStageReusable ==
|
|
\A p \in Preparations :
|
|
/\ artifactState = "Published"
|
|
/\ ~gcRequested
|
|
/\ materializerState[p] = "Live"
|
|
/\ stageState[p] = "Owned"
|
|
=> ENABLED ReusePublishedArtifact(p)
|
|
|
|
LeaseBindingConsistent ==
|
|
\A g \in Generations :
|
|
(g \in leases) <=> (artifactBinding[g] = Artifact)
|
|
|
|
MountedGenerationLeased ==
|
|
/\ mounts \subseteq leases
|
|
/\ \A g \in mounts : artifactBinding[g] = Artifact
|
|
|
|
LeasedArtifactPublished ==
|
|
leases # {} => artifactState = "Published"
|
|
|
|
GCExcludesLeases ==
|
|
gcRequested =>
|
|
/\ artifactState = "Published"
|
|
/\ leases = {}
|
|
/\ mounts = {}
|
|
|
|
GCExcludesSelections ==
|
|
gcRequested =>
|
|
\A g \in Generations : selectionBinding[g] = NoArtifact
|
|
|
|
SelectedArtifactStable ==
|
|
\A g \in Generations :
|
|
selectionBinding[g] # NoArtifact =>
|
|
/\ ~ENABLED RequestGC
|
|
/\ ~ENABLED ReclaimArtifact
|
|
|
|
ReplacementOnlyDuringGC ==
|
|
replacementPresent => gcRequested
|
|
|
|
ForeignStagePreserved ==
|
|
foreignObserved => \E p \in Preparations : stageState[p] = "Foreign"
|
|
|
|
=============================================================================
|