ms2k/lazaret
SHA256
Watch
0
Code Releases 3 Activity

Model live prepared-lower ownership during recovery

Browse source
This commit is contained in:
ms2k 2026-07-21 23:46:54 +09:00
commit 6eba9f25ca
2 changed files with 151 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

9
docs/protocol/PreparedLower.cfg
View file

@ -1,9 +1,12 @@
CONSTANTS CONSTANTS
G1 = g1 G1 = g1
G2 = g2 G2 = g2
P1 = p1
P2 = p2
A1 = a1 A1 = a1
NoArtifact = noArtifact NoArtifact = noArtifact
Generations <- GenerationsFixture Generations <- GenerationsFixture
Preparations <- PreparationsFixture
Artifact = a1 Artifact = a1
SPECIFICATION Spec SPECIFICATION Spec
@ -11,10 +14,14 @@ CHECK_DEADLOCK FALSE
INVARIANTS INVARIANTS
TypeOK TypeOK
PrepareOwnershipConsistent
LiveOwnedStageNotRecoverable
LostOwnedStageRecoverable
LostIntentRecoverable
PublishedOwnedStageReusable
LeaseBindingConsistent LeaseBindingConsistent
MountedGenerationLeased MountedGenerationLeased
LeasedArtifactPublished LeasedArtifactPublished
GCExcludesLeases GCExcludesLeases
ReplacementOnlyDuringGC ReplacementOnlyDuringGC
ForeignStagePreserved ForeignStagePreserved
OwnedStageRequiresIntent

205
docs/protocol/PreparedLower.tla
View file

@ -2,32 +2,40 @@
EXTENDS FiniteSets, TLC EXTENDS FiniteSets, TLC
(*************************************************************************** (***************************************************************************
Artifact-level refinement for prepared-lower publication, generation leases, Artifact-level refinement for concurrent prepared-lower publication,
State Anchor use, exact-owned abandoned preparation recovery, and reclaim. materializer-loss recovery, generation leases, State Anchor use, and reclaim.
***************************************************************************) ***************************************************************************)
CONSTANTS CONSTANTS
Generations, Generations,
Preparations,
Artifact, Artifact,
NoArtifact, NoArtifact,
G1, G1,
G2, G2,
P1,
P2,
A1 A1
ASSUME ASSUME
/\ Generations = {G1, G2} /\ Generations = {G1, G2}
/\ G1 # G2 /\ G1 # G2
/\ Preparations = {P1, P2}
/\ P1 # P2
/\ Artifact = A1 /\ Artifact = A1
/\ NoArtifact # Artifact /\ NoArtifact # Artifact
ArtifactStates == {"Absent", "Published"} ArtifactStates == {"Absent", "Published"}
StageStates == {"Absent", "Owned", "Foreign"} StageStates == {"Absent", "Owned", "Foreign"}
MaterializerStates == {"Absent", "Live", "Lost"}
GenerationsFixture == {G1, G2} GenerationsFixture == {G1, G2}
PreparationsFixture == {P1, P2}
VARIABLES VARIABLES
artifactState, artifactState,
stageState, stageState,
prepareIntent, prepareIntent,
materializerState,
leases, leases,
mounts, mounts,
artifactBinding, artifactBinding,
@ -39,6 +47,7 @@ vars == <<
artifactState, artifactState,
stageState, stageState,
prepareIntent, prepareIntent,
materializerState,
leases, leases,
mounts, mounts,
artifactBinding, artifactBinding,
@ -49,8 +58,9 @@ vars == <<
Init == Init ==
/\ artifactState = "Absent" /\ artifactState = "Absent"
/\ stageState = "Absent" /\ stageState = [p \in Preparations |-> "Absent"]
/\ prepareIntent = FALSE /\ prepareIntent = [p \in Preparations |-> FALSE]
/\ materializerState = [p \in Preparations |-> "Absent"]
/\ leases = {} /\ leases = {}
/\ mounts = {} /\ mounts = {}
/\ artifactBinding = [g \in Generations |-> NoArtifact] /\ artifactBinding = [g \in Generations |-> NoArtifact]
@ -58,52 +68,86 @@ Init ==
/\ replacementPresent = FALSE /\ replacementPresent = FALSE
/\ foreignObserved = FALSE /\ foreignObserved = FALSE
BeginPrepare == BeginPrepare(p) ==
/\ artifactState = "Absent" /\ artifactState = "Absent"
/\ stageState = "Absent" /\ stageState[p] = "Absent"
/\ ~prepareIntent /\ ~prepareIntent[p]
/\ prepareIntent' = TRUE /\ materializerState[p] = "Absent"
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = TRUE]
/\ materializerState' = [materializerState EXCEPT ![p] = "Live"]
/\ UNCHANGED <<artifactState, stageState, leases, mounts, /\ UNCHANGED <<artifactState, stageState, leases, mounts,
artifactBinding, gcRequested, replacementPresent, foreignObserved>> artifactBinding, gcRequested, replacementPresent, foreignObserved>>
CreateOwnedStage == CreateOwnedStage(p) ==
/\ artifactState = "Absent" /\ stageState[p] = "Absent"
/\ stageState = "Absent" /\ prepareIntent[p]
/\ prepareIntent /\ materializerState[p] = "Live"
/\ stageState' = "Owned" /\ stageState' = [stageState EXCEPT ![p] = "Owned"]
/\ UNCHANGED <<artifactState, prepareIntent, leases, mounts, /\ UNCHANGED <<artifactState, prepareIntent, materializerState, leases,
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>> artifactBinding, gcRequested, replacementPresent, foreignObserved>>
PublishArtifact == PublishArtifact(p) ==
/\ artifactState = "Absent" /\ artifactState = "Absent"
/\ stageState = "Owned" /\ stageState[p] = "Owned"
/\ prepareIntent /\ prepareIntent[p]
/\ materializerState[p] = "Live"
/\ artifactState' = "Published" /\ artifactState' = "Published"
/\ stageState' = "Absent" /\ stageState' = [stageState EXCEPT ![p] = "Absent"]
/\ prepareIntent' = FALSE /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
/\ UNCHANGED <<leases, mounts, artifactBinding, gcRequested, /\ UNCHANGED <<leases, mounts, artifactBinding, gcRequested,
replacementPresent, foreignObserved>> replacementPresent, foreignObserved>>
RecoverOwnedStage == ReusePublishedArtifact(p) ==
/\ artifactState = "Absent" /\ artifactState = "Published"
/\ stageState = "Owned" /\ ~gcRequested
/\ prepareIntent /\ stageState[p] = "Owned"
/\ stageState' = "Absent" /\ prepareIntent[p]
/\ prepareIntent' = FALSE /\ materializerState[p] = "Live"
/\ stageState' = [stageState EXCEPT ![p] = "Absent"]
/\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
/\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
/\ UNCHANGED <<artifactState, leases, mounts, artifactBinding, /\ UNCHANGED <<artifactState, leases, mounts, artifactBinding,
gcRequested, replacementPresent, foreignObserved>> gcRequested, replacementPresent, foreignObserved>>
ObserveForeignStage == RecoverUnmaterializedIntent(p) ==
/\ artifactState = "Absent" /\ stageState[p] = "Absent"
/\ stageState = "Absent" /\ prepareIntent[p]
/\ ~prepareIntent /\ materializerState[p] = "Lost"
/\ stageState' = "Foreign" /\ prepareIntent' = [prepareIntent EXCEPT ![p] = FALSE]
/\ foreignObserved' = TRUE /\ materializerState' = [materializerState EXCEPT ![p] = "Absent"]
/\ UNCHANGED <<artifactState, prepareIntent, leases, mounts, /\ UNCHANGED <<artifactState, stageState, leases, mounts,
artifactBinding, gcRequested, replacementPresent>> artifactBinding, gcRequested, replacementPresent, foreignObserved>>
RefuseForeignStage == RecoverOwnedStage(p) ==
/\ stageState = "Foreign" /\ 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, leases, mounts, artifactBinding,
gcRequested, replacementPresent, foreignObserved>>
ObserveForeignStage(p) ==
/\ stageState[p] = "Absent"
/\ ~prepareIntent[p]
/\ materializerState[p] = "Absent"
/\ stageState' = [stageState EXCEPT ![p] = "Foreign"]
/\ foreignObserved' = TRUE
/\ UNCHANGED <<artifactState, prepareIntent, materializerState, leases,
mounts, artifactBinding, gcRequested, replacementPresent>>
RefuseForeignStage(p) ==
/\ stageState[p] = "Foreign"
/\ UNCHANGED vars /\ UNCHANGED vars
AcquireLease(g) == AcquireLease(g) ==
@ -112,46 +156,52 @@ AcquireLease(g) ==
/\ g \notin leases /\ g \notin leases
/\ leases' = leases \cup {g} /\ leases' = leases \cup {g}
/\ artifactBinding' = [artifactBinding EXCEPT ![g] = Artifact] /\ artifactBinding' = [artifactBinding EXCEPT ![g] = Artifact]
/\ UNCHANGED <<artifactState, stageState, prepareIntent, mounts, /\ UNCHANGED <<artifactState, stageState, prepareIntent,
gcRequested, replacementPresent, foreignObserved>> materializerState, mounts, gcRequested, replacementPresent,
foreignObserved>>
MountStateAnchor(g) == MountStateAnchor(g) ==
/\ g \in leases /\ g \in leases
/\ artifactBinding[g] = Artifact /\ artifactBinding[g] = Artifact
/\ g \notin mounts /\ g \notin mounts
/\ mounts' = mounts \cup {g} /\ mounts' = mounts \cup {g}
/\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, /\ UNCHANGED <<artifactState, stageState, prepareIntent,
artifactBinding, gcRequested, replacementPresent, foreignObserved>> materializerState, leases, artifactBinding, gcRequested,
replacementPresent, foreignObserved>>
UnmountStateAnchor(g) == UnmountStateAnchor(g) ==
/\ g \in mounts /\ g \in mounts
/\ mounts' = mounts \ {g} /\ mounts' = mounts \ {g}
/\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, /\ UNCHANGED <<artifactState, stageState, prepareIntent,
artifactBinding, gcRequested, replacementPresent, foreignObserved>> materializerState, leases, artifactBinding, gcRequested,
replacementPresent, foreignObserved>>
ReleaseLease(g) == ReleaseLease(g) ==
/\ g \in leases /\ g \in leases
/\ g \notin mounts /\ g \notin mounts
/\ leases' = leases \ {g} /\ leases' = leases \ {g}
/\ artifactBinding' = [artifactBinding EXCEPT ![g] = NoArtifact] /\ artifactBinding' = [artifactBinding EXCEPT ![g] = NoArtifact]
/\ UNCHANGED <<artifactState, stageState, prepareIntent, mounts, /\ UNCHANGED <<artifactState, stageState, prepareIntent,
gcRequested, replacementPresent, foreignObserved>> materializerState, mounts, gcRequested, replacementPresent,
foreignObserved>>
RequestGC == RequestGC ==
/\ artifactState = "Published" /\ artifactState = "Published"
/\ leases = {} /\ leases = {}
/\ ~gcRequested /\ ~gcRequested
/\ gcRequested' = TRUE /\ gcRequested' = TRUE
/\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, mounts, /\ UNCHANGED <<artifactState, stageState, prepareIntent,
artifactBinding, replacementPresent, foreignObserved>> materializerState, leases, mounts, artifactBinding,
replacementPresent, foreignObserved>>
PublishReplacementDuringGC == PublishReplacementDuringGC ==
/\ artifactState = "Published" /\ artifactState = "Published"
/\ gcRequested /\ gcRequested
/\ ~replacementPresent /\ ~replacementPresent
/\ replacementPresent' = TRUE /\ replacementPresent' = TRUE
/\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, mounts, /\ UNCHANGED <<artifactState, stageState, prepareIntent,
artifactBinding, gcRequested, foreignObserved>> materializerState, leases, mounts, artifactBinding, gcRequested,
foreignObserved>>
ReclaimArtifact == ReclaimArtifact ==
/\ artifactState = "Published" /\ artifactState = "Published"
@ -161,16 +211,19 @@ ReclaimArtifact ==
/\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent" /\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent"
/\ gcRequested' = FALSE /\ gcRequested' = FALSE
/\ replacementPresent' = FALSE /\ replacementPresent' = FALSE
/\ UNCHANGED <<stageState, prepareIntent, leases, mounts, /\ UNCHANGED <<stageState, prepareIntent, materializerState, leases,
artifactBinding, foreignObserved>> mounts, artifactBinding, foreignObserved>>
Next == Next ==
\/ BeginPrepare \/ (\E p \in Preparations : BeginPrepare(p))
\/ CreateOwnedStage \/ (\E p \in Preparations : CreateOwnedStage(p))
\/ PublishArtifact \/ (\E p \in Preparations : LoseMaterializer(p))
\/ RecoverOwnedStage \/ (\E p \in Preparations : PublishArtifact(p))
\/ ObserveForeignStage \/ (\E p \in Preparations : ReusePublishedArtifact(p))
\/ RefuseForeignStage \/ (\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 : AcquireLease(g)) \/ (\E g \in Generations : AcquireLease(g))
\/ (\E g \in Generations : MountStateAnchor(g)) \/ (\E g \in Generations : MountStateAnchor(g))
\/ (\E g \in Generations : UnmountStateAnchor(g)) \/ (\E g \in Generations : UnmountStateAnchor(g))
@ -183,8 +236,9 @@ Spec == Init /\ [][Next]_vars
TypeOK == TypeOK ==
/\ artifactState \in ArtifactStates /\ artifactState \in ArtifactStates
/\ stageState \in StageStates /\ stageState \in [Preparations -> StageStates]
/\ prepareIntent \in BOOLEAN /\ prepareIntent \in [Preparations -> BOOLEAN]
/\ materializerState \in [Preparations -> MaterializerStates]
/\ leases \subseteq Generations /\ leases \subseteq Generations
/\ mounts \subseteq Generations /\ mounts \subseteq Generations
/\ artifactBinding \in [Generations -> {NoArtifact, Artifact}] /\ artifactBinding \in [Generations -> {NoArtifact, Artifact}]
@ -192,6 +246,38 @@ TypeOK ==
/\ replacementPresent \in BOOLEAN /\ replacementPresent \in BOOLEAN
/\ foreignObserved \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"
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 == LeaseBindingConsistent ==
\A g \in Generations : \A g \in Generations :
(g \in leases) <=> (artifactBinding[g] = Artifact) (g \in leases) <=> (artifactBinding[g] = Artifact)
@ -213,9 +299,6 @@ ReplacementOnlyDuringGC ==
replacementPresent => gcRequested replacementPresent => gcRequested
ForeignStagePreserved == ForeignStagePreserved ==
foreignObserved => stageState = "Foreign" foreignObserved => \E p \in Preparations : stageState[p] = "Foreign"
OwnedStageRequiresIntent ==
stageState = "Owned" => prepareIntent
============================================================================= =============================================================================