Model prepared artifact selection before lease acquisition

docs/protocol/PreparedLower.cfg

@@ -3,11 +3,12 @@ CONSTANTS
     G2 = g2
     P1 = p1
     P2 = p2
-    A1 = a1
+    A1 = incarnation1
+    A2 = incarnation2
     NoArtifact = noArtifact
     Generations <- GenerationsFixture
     Preparations <- PreparationsFixture
-    Artifact = a1
+    Artifact = artifact
 
 SPECIFICATION Spec
 CHECK_DEADLOCK FALSE
@@ -15,6 +16,8 @@ CHECK_DEADLOCK FALSE
 INVARIANTS
     TypeOK
     PrepareOwnershipConsistent
+    ArtifactIncarnationConsistent
+    SelectionBindingConsistent
     LiveOwnedStageNotRecoverable
     LostOwnedStageRecoverable
     LostIntentRecoverable
@@ -23,5 +26,7 @@ INVARIANTS
     MountedGenerationLeased
     LeasedArtifactPublished
     GCExcludesLeases
+    GCExcludesSelections
+    SelectedArtifactStable
     ReplacementOnlyDuringGC
     ForeignStagePreserved

docs/protocol/PreparedLower.tla

@@ -15,17 +15,21 @@ CONSTANTS
     G2,
     P1,
     P2,
-    A1
+    A1,
+    A2
 
 ASSUME
     /\ Generations = {G1, G2}
     /\ G1 # G2
     /\ Preparations = {P1, P2}
     /\ P1 # P2
-    /\ Artifact = A1
     /\ 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}
@@ -33,10 +37,12 @@ PreparationsFixture == {P1, P2}
 
 VARIABLES
     artifactState,
+    artifactIncarnation,
     stageState,
     prepareIntent,
     materializerState,
     leases,
+    selectionBinding,
     mounts,
     artifactBinding,
     gcRequested,
@@ -45,10 +51,12 @@ VARIABLES
 
 vars == <<
     artifactState,
+    artifactIncarnation,
     stageState,
     prepareIntent,
     materializerState,
     leases,
+    selectionBinding,
     mounts,
     artifactBinding,
     gcRequested,
@@ -58,10 +66,12 @@ vars == <<
 
 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
@@ -75,24 +85,26 @@ BeginPrepare(p) ==
     /\ materializerState[p] = "Absent"
     /\ prepareIntent' = [prepareIntent EXCEPT ![p] = TRUE]
     /\ materializerState' = [materializerState EXCEPT ![p] = "Live"]
-    /\ UNCHANGED <<artifactState, stageState, leases, mounts,
-        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+    /\ 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, prepareIntent, materializerState, leases,
-        mounts, artifactBinding, gcRequested, replacementPresent,
-        foreignObserved>>
+    /\ 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, stageState, prepareIntent, leases, mounts,
-        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
+        prepareIntent, leases, selectionBinding, mounts, artifactBinding,
+        gcRequested, replacementPresent, foreignObserved>>
 
 PublishArtifact(p) ==
     /\ artifactState = "Absent"
@@ -100,11 +112,12 @@ PublishArtifact(p) ==
     /\ 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, mounts, artifactBinding, gcRequested,
-        replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<leases, selectionBinding, mounts, artifactBinding,
+        gcRequested, replacementPresent, foreignObserved>>
 
 ReusePublishedArtifact(p) ==
     /\ artifactState = "Published"
@@ -115,8 +128,9 @@ ReusePublishedArtifact(p) ==
     /\ stageState' = [stageState EXCEPT ![p] = "Absent"]
     /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
     /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
-    /\ UNCHANGED <<artifactState, leases, mounts, artifactBinding,
-        gcRequested, replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<artifactState, artifactIncarnation, leases,
+        selectionBinding, mounts, artifactBinding, gcRequested,
+        replacementPresent, foreignObserved>>
 
 RecoverUnmaterializedIntent(p) ==
     /\ stageState[p] = "Absent"
@@ -124,8 +138,9 @@ RecoverUnmaterializedIntent(p) ==
     /\ materializerState[p] = "Lost"
     /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
     /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
-    /\ UNCHANGED <<artifactState, stageState, leases, mounts,
-        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState, leases,
+        selectionBinding, mounts, artifactBinding, gcRequested,
+        replacementPresent, foreignObserved>>
 
 RecoverOwnedStage(p) ==
     /\ stageState[p] = "Owned"
@@ -134,8 +149,9 @@ RecoverOwnedStage(p) ==
     /\ stageState' = [stageState EXCEPT ![p] = "Absent"]
     /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
     /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
-    /\ UNCHANGED <<artifactState, leases, mounts, artifactBinding,
-        gcRequested, replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<artifactState, artifactIncarnation, leases,
+        selectionBinding, mounts, artifactBinding, gcRequested,
+        replacementPresent, foreignObserved>>
 
 ObserveForeignStage(p) ==
     /\ stageState[p] = "Absent"
@@ -143,20 +159,42 @@ ObserveForeignStage(p) ==
     /\ materializerState[p] = "Absent"
     /\ stageState' = [stageState EXCEPT ![p] = "Foreign"]
     /\ foreignObserved' = TRUE
-    /\ UNCHANGED <<artifactState, prepareIntent, materializerState, leases,
-        mounts, artifactBinding, gcRequested, replacementPresent>>
+    /\ 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, stageState, prepareIntent,
+    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState, prepareIntent,
         materializerState, mounts, gcRequested, replacementPresent,
         foreignObserved>>
 
@@ -165,54 +203,60 @@ MountStateAnchor(g) ==
     /\ artifactBinding[g] = Artifact
     /\ g \notin mounts
     /\ mounts' = mounts \cup {g}
-    /\ UNCHANGED <<artifactState, stageState, prepareIntent,
-        materializerState, leases, artifactBinding, gcRequested,
-        replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
+        prepareIntent, materializerState, leases, selectionBinding,
+        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
 
 UnmountStateAnchor(g) ==
     /\ g \in mounts
     /\ mounts' = mounts \ {g}
-    /\ UNCHANGED <<artifactState, stageState, prepareIntent,
-        materializerState, leases, artifactBinding, gcRequested,
-        replacementPresent, foreignObserved>>
+    /\ 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, stageState, prepareIntent,
-        materializerState, mounts, gcRequested, replacementPresent,
-        foreignObserved>>
+    /\ 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, stageState, prepareIntent,
-        materializerState, leases, mounts, artifactBinding,
-        replacementPresent, foreignObserved>>
+    /\ UNCHANGED <<artifactState, artifactIncarnation, stageState,
+        prepareIntent, materializerState, leases, selectionBinding, mounts,
+        artifactBinding, replacementPresent, foreignObserved>>
 
 PublishReplacementDuringGC ==
     /\ artifactState = "Published"
     /\ gcRequested
     /\ ~replacementPresent
     /\ replacementPresent' = TRUE
-    /\ UNCHANGED <<artifactState, stageState, prepareIntent,
-        materializerState, leases, mounts, artifactBinding, gcRequested,
-        foreignObserved>>
+    /\ 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,
-        mounts, artifactBinding, foreignObserved>>
+        selectionBinding, mounts, artifactBinding, foreignObserved>>
 
 Next ==
     \/ (\E p \in Preparations : BeginPrepare(p))
@@ -224,6 +268,8 @@ Next ==
     \/ (\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))
@@ -236,10 +282,13 @@ 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
@@ -254,6 +303,16 @@ PrepareOwnershipConsistent ==
             /\ ~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)
@@ -295,6 +354,16 @@ GCExcludesLeases ==
         /\ 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