Check hardlink topology in workspace routing protocol
This commit is contained in:
parent
1ad3b84db2
commit
52c8c56e4f
4 changed files with 335 additions and 1 deletions
15
docs/protocol/IgnoredWorkspaceHardlinkRouting.cfg
Normal file
15
docs/protocol/IgnoredWorkspaceHardlinkRouting.cfg
Normal file
|
|
@ -0,0 +1,15 @@
|
||||||
|
CONSTANTS
|
||||||
|
Correct = Correct
|
||||||
|
SplitCloneAliases = SplitCloneAliases
|
||||||
|
MergeCloneObjects = MergeCloneObjects
|
||||||
|
CrossBackingLink = CrossBackingLink
|
||||||
|
LinkedRuntimeRename = LinkedRuntimeRename
|
||||||
|
UnstableAliasClone = UnstableAliasClone
|
||||||
|
Mode = Correct
|
||||||
|
|
||||||
|
SPECIFICATION Spec
|
||||||
|
CHECK_DEADLOCK FALSE
|
||||||
|
|
||||||
|
INVARIANTS
|
||||||
|
TypeOK
|
||||||
|
LinkSafety
|
||||||
314
docs/protocol/IgnoredWorkspaceHardlinkRouting.tla
Normal file
314
docs/protocol/IgnoredWorkspaceHardlinkRouting.tla
Normal file
|
|
@ -0,0 +1,314 @@
|
||||||
|
------------------ MODULE IgnoredWorkspaceHardlinkRouting ------------------
|
||||||
|
EXTENDS TLC
|
||||||
|
|
||||||
|
(***************************************************************************
|
||||||
|
Generation-level alias safety for ignored-workspace operations and cloning.
|
||||||
|
***************************************************************************)
|
||||||
|
|
||||||
|
CONSTANTS Correct, SplitCloneAliases, MergeCloneObjects, CrossBackingLink,
|
||||||
|
LinkedRuntimeRename, UnstableAliasClone, Mode
|
||||||
|
|
||||||
|
Modes == {Correct, SplitCloneAliases, MergeCloneObjects, CrossBackingLink,
|
||||||
|
LinkedRuntimeRename, UnstableAliasClone}
|
||||||
|
Names == {"A", "B"}
|
||||||
|
Policies == {"Host", "Isolated"}
|
||||||
|
HostObjects == {"H1", "H2"}
|
||||||
|
IsolatedObjects == {"I1", "I2"}
|
||||||
|
Objects == HostObjects \cup IsolatedObjects
|
||||||
|
MaybeObjects == Objects \cup {"None"}
|
||||||
|
Payloads == {"V1", "V2"}
|
||||||
|
Phases == {"ReadyHost", "Planning", "Installed", "ReadyCandidate"}
|
||||||
|
Results == {"None", "Success", "EXDEV"}
|
||||||
|
Operations == {"None", "SameBackingLink", "CrossBackingLink",
|
||||||
|
"LinkedRuntimeRename", "StartupClone"}
|
||||||
|
|
||||||
|
ASSUME Mode \in Modes
|
||||||
|
|
||||||
|
CloneObject(object) == IF object = "H1" THEN "I1" ELSE "I2"
|
||||||
|
CandidatePolicies == {
|
||||||
|
policy \in [Names -> Policies] : \E name \in Names : policy[name] = "Isolated"
|
||||||
|
}
|
||||||
|
|
||||||
|
VARIABLES phase, online, candidatePolicy, hostNames, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result,
|
||||||
|
splitCloneAliases, mergedCloneObjects, crossBackingLinked,
|
||||||
|
linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted
|
||||||
|
|
||||||
|
vars == <<phase, online, candidatePolicy, hostNames, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result,
|
||||||
|
splitCloneAliases, mergedCloneObjects, crossBackingLinked,
|
||||||
|
linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>
|
||||||
|
|
||||||
|
SafetyFlags == <<splitCloneAliases, mergedCloneObjects, crossBackingLinked,
|
||||||
|
linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>
|
||||||
|
|
||||||
|
TypeOK ==
|
||||||
|
/\ phase \in Phases
|
||||||
|
/\ online \in BOOLEAN
|
||||||
|
/\ candidatePolicy \in [Names -> Policies]
|
||||||
|
/\ hostNames \in [Names -> HostObjects]
|
||||||
|
/\ isolatedNames \in [Names -> MaybeObjects]
|
||||||
|
/\ objectValues \in [Objects -> Payloads]
|
||||||
|
/\ capturedHostNames \in [Names -> HostObjects]
|
||||||
|
/\ capturedHostValues \in [HostObjects -> Payloads]
|
||||||
|
/\ operation \in Operations
|
||||||
|
/\ result \in Results
|
||||||
|
/\ splitCloneAliases \in BOOLEAN
|
||||||
|
/\ mergedCloneObjects \in BOOLEAN
|
||||||
|
/\ crossBackingLinked \in BOOLEAN
|
||||||
|
/\ linkedRuntimeRenameAdmitted \in BOOLEAN
|
||||||
|
/\ unstableAliasCloneAdmitted \in BOOLEAN
|
||||||
|
|
||||||
|
Init ==
|
||||||
|
/\ phase = "ReadyHost"
|
||||||
|
/\ online = TRUE
|
||||||
|
/\ candidatePolicy = [name \in Names |-> "Host"]
|
||||||
|
/\ hostNames \in [Names -> HostObjects]
|
||||||
|
/\ isolatedNames = [name \in Names |-> "None"]
|
||||||
|
/\ objectValues \in [Objects -> Payloads]
|
||||||
|
/\ capturedHostNames = hostNames
|
||||||
|
/\ capturedHostValues = [object \in HostObjects |-> objectValues[object]]
|
||||||
|
/\ operation = "None"
|
||||||
|
/\ result = "None"
|
||||||
|
/\ splitCloneAliases = FALSE
|
||||||
|
/\ mergedCloneObjects = FALSE
|
||||||
|
/\ crossBackingLinked = FALSE
|
||||||
|
/\ linkedRuntimeRenameAdmitted = FALSE
|
||||||
|
/\ unstableAliasCloneAdmitted = FALSE
|
||||||
|
|
||||||
|
SameBackingLink ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyHost"
|
||||||
|
/\ hostNames' = [hostNames EXCEPT !["B"] = hostNames["A"]]
|
||||||
|
/\ operation' = "SameBackingLink"
|
||||||
|
/\ result' = "Success"
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, SafetyFlags>>
|
||||||
|
|
||||||
|
HostWrite ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyHost"
|
||||||
|
/\ \E object \in HostObjects :
|
||||||
|
objectValues' = [objectValues EXCEPT ![object] = IF @ = "V1" THEN "V2" ELSE "V1"]
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>
|
||||||
|
|
||||||
|
BeginClone ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyHost"
|
||||||
|
/\ phase' = "Planning"
|
||||||
|
/\ candidatePolicy' \in CandidatePolicies
|
||||||
|
/\ capturedHostNames' = hostNames
|
||||||
|
/\ capturedHostValues' = [object \in HostObjects |-> objectValues[object]]
|
||||||
|
/\ operation' = "StartupClone"
|
||||||
|
/\ result' = "None"
|
||||||
|
/\ UNCHANGED <<online, hostNames, isolatedNames, objectValues, SafetyFlags>>
|
||||||
|
|
||||||
|
MutateCapturedAlias ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ hostNames' = [hostNames EXCEPT !["B"] = IF @ = "H1" THEN "H2" ELSE "H1"]
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>
|
||||||
|
|
||||||
|
MutateCapturedValue ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ \E object \in HostObjects :
|
||||||
|
objectValues' = [objectValues EXCEPT ![object] = IF @ = "V1" THEN "V2" ELSE "V1"]
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>
|
||||||
|
|
||||||
|
StableCapture ==
|
||||||
|
/\ hostNames = capturedHostNames
|
||||||
|
/\ \A object \in HostObjects : objectValues[object] = capturedHostValues[object]
|
||||||
|
|
||||||
|
InstallClone ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ StableCapture
|
||||||
|
/\ phase' = "Installed"
|
||||||
|
/\ isolatedNames' = [name \in Names |->
|
||||||
|
IF candidatePolicy[name] = "Isolated"
|
||||||
|
THEN CloneObject(capturedHostNames[name]) ELSE "None"]
|
||||||
|
/\ objectValues' = [objectValues EXCEPT
|
||||||
|
!["I1"] = capturedHostValues["H1"],
|
||||||
|
!["I2"] = capturedHostValues["H2"]]
|
||||||
|
/\ UNCHANGED <<online, candidatePolicy, hostNames, capturedHostNames,
|
||||||
|
capturedHostValues, operation, result, SafetyFlags>>
|
||||||
|
|
||||||
|
InstallSplitAliases ==
|
||||||
|
/\ Mode = SplitCloneAliases
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ StableCapture
|
||||||
|
/\ candidatePolicy["A"] = "Isolated"
|
||||||
|
/\ candidatePolicy["B"] = "Isolated"
|
||||||
|
/\ capturedHostNames["A"] = capturedHostNames["B"]
|
||||||
|
/\ phase' = "Installed"
|
||||||
|
/\ isolatedNames' = [name \in Names |-> IF name = "A" THEN "I1" ELSE "I2"]
|
||||||
|
/\ splitCloneAliases' = TRUE
|
||||||
|
/\ UNCHANGED <<online, candidatePolicy, hostNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result,
|
||||||
|
mergedCloneObjects, crossBackingLinked,
|
||||||
|
linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>
|
||||||
|
|
||||||
|
InstallMergedObjects ==
|
||||||
|
/\ Mode = MergeCloneObjects
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ StableCapture
|
||||||
|
/\ candidatePolicy["A"] = "Isolated"
|
||||||
|
/\ candidatePolicy["B"] = "Isolated"
|
||||||
|
/\ capturedHostNames["A"] # capturedHostNames["B"]
|
||||||
|
/\ phase' = "Installed"
|
||||||
|
/\ isolatedNames' = [name \in Names |-> "I1"]
|
||||||
|
/\ mergedCloneObjects' = TRUE
|
||||||
|
/\ UNCHANGED <<online, candidatePolicy, hostNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result,
|
||||||
|
splitCloneAliases, crossBackingLinked,
|
||||||
|
linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>
|
||||||
|
|
||||||
|
PublishClone ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Installed"
|
||||||
|
/\ StableCapture
|
||||||
|
/\ phase' = "ReadyCandidate"
|
||||||
|
/\ result' = "Success"
|
||||||
|
/\ UNCHANGED <<online, candidatePolicy, hostNames, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, SafetyFlags>>
|
||||||
|
|
||||||
|
AbortUnstableClone ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ ~StableCapture
|
||||||
|
/\ phase' = "ReadyHost"
|
||||||
|
/\ candidatePolicy' = [name \in Names |-> "Host"]
|
||||||
|
/\ isolatedNames' = [name \in Names |-> "None"]
|
||||||
|
/\ operation' = "StartupClone"
|
||||||
|
/\ result' = "EXDEV"
|
||||||
|
/\ UNCHANGED <<online, hostNames, objectValues, capturedHostNames,
|
||||||
|
capturedHostValues, SafetyFlags>>
|
||||||
|
|
||||||
|
PublishUnstableAliasClone ==
|
||||||
|
/\ Mode = UnstableAliasClone
|
||||||
|
/\ online
|
||||||
|
/\ phase = "Planning"
|
||||||
|
/\ ~StableCapture
|
||||||
|
/\ phase' = "ReadyCandidate"
|
||||||
|
/\ isolatedNames' = [name \in Names |->
|
||||||
|
IF candidatePolicy[name] = "Isolated"
|
||||||
|
THEN CloneObject(capturedHostNames[name]) ELSE "None"]
|
||||||
|
/\ result' = "Success"
|
||||||
|
/\ unstableAliasCloneAdmitted' = TRUE
|
||||||
|
/\ UNCHANGED <<online, candidatePolicy, hostNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation,
|
||||||
|
splitCloneAliases, mergedCloneObjects, crossBackingLinked,
|
||||||
|
linkedRuntimeRenameAdmitted>>
|
||||||
|
|
||||||
|
CrossBackingLinkAttempt ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyCandidate"
|
||||||
|
/\ \E hostName, isolatedName \in Names :
|
||||||
|
/\ candidatePolicy[hostName] = "Host"
|
||||||
|
/\ candidatePolicy[isolatedName] = "Isolated"
|
||||||
|
/\ operation' = "CrossBackingLink"
|
||||||
|
/\ result' = "EXDEV"
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
|
||||||
|
objectValues, capturedHostNames, capturedHostValues, SafetyFlags>>
|
||||||
|
|
||||||
|
AllowCrossBackingLink ==
|
||||||
|
/\ Mode = CrossBackingLink
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyCandidate"
|
||||||
|
/\ candidatePolicy["A"] = "Host"
|
||||||
|
/\ candidatePolicy["B"] = "Isolated"
|
||||||
|
/\ isolatedNames' = [isolatedNames EXCEPT !["B"] = hostNames["A"]]
|
||||||
|
/\ operation' = "CrossBackingLink"
|
||||||
|
/\ result' = "Success"
|
||||||
|
/\ crossBackingLinked' = TRUE
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, hostNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, splitCloneAliases,
|
||||||
|
mergedCloneObjects, linkedRuntimeRenameAdmitted,
|
||||||
|
unstableAliasCloneAdmitted>>
|
||||||
|
|
||||||
|
LinkedRuntimeRenameAttempt ==
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyCandidate"
|
||||||
|
/\ candidatePolicy["A"] = "Host"
|
||||||
|
/\ candidatePolicy["B"] = "Isolated"
|
||||||
|
/\ hostNames["A"] = hostNames["B"]
|
||||||
|
/\ operation' = "LinkedRuntimeRename"
|
||||||
|
/\ result' = "EXDEV"
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
|
||||||
|
objectValues, capturedHostNames, capturedHostValues, SafetyFlags>>
|
||||||
|
|
||||||
|
AllowLinkedRuntimeRename ==
|
||||||
|
/\ Mode = LinkedRuntimeRename
|
||||||
|
/\ online
|
||||||
|
/\ phase = "ReadyCandidate"
|
||||||
|
/\ candidatePolicy["A"] = "Host"
|
||||||
|
/\ candidatePolicy["B"] = "Isolated"
|
||||||
|
/\ hostNames["A"] = hostNames["B"]
|
||||||
|
/\ isolatedNames' = [isolatedNames EXCEPT !["B"] = CloneObject(hostNames["A"])]
|
||||||
|
/\ operation' = "LinkedRuntimeRename"
|
||||||
|
/\ result' = "Success"
|
||||||
|
/\ linkedRuntimeRenameAdmitted' = TRUE
|
||||||
|
/\ UNCHANGED <<phase, online, candidatePolicy, hostNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, splitCloneAliases,
|
||||||
|
mergedCloneObjects, crossBackingLinked,
|
||||||
|
unstableAliasCloneAdmitted>>
|
||||||
|
|
||||||
|
Crash ==
|
||||||
|
/\ online
|
||||||
|
/\ phase \in {"Planning", "Installed"}
|
||||||
|
/\ online' = FALSE
|
||||||
|
/\ UNCHANGED <<phase, candidatePolicy, hostNames, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>
|
||||||
|
|
||||||
|
Recover ==
|
||||||
|
/\ ~online
|
||||||
|
/\ online' = TRUE
|
||||||
|
/\ UNCHANGED <<phase, candidatePolicy, hostNames, isolatedNames, objectValues,
|
||||||
|
capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>
|
||||||
|
|
||||||
|
Next == SameBackingLink \/ HostWrite \/ BeginClone \/ MutateCapturedAlias
|
||||||
|
\/ MutateCapturedValue \/ InstallClone \/ InstallSplitAliases
|
||||||
|
\/ InstallMergedObjects \/ PublishClone \/ AbortUnstableClone
|
||||||
|
\/ PublishUnstableAliasClone \/ CrossBackingLinkAttempt
|
||||||
|
\/ AllowCrossBackingLink \/ LinkedRuntimeRenameAttempt
|
||||||
|
\/ AllowLinkedRuntimeRename \/ Crash \/ Recover
|
||||||
|
|
||||||
|
Spec == Init /\ [][Next]_vars
|
||||||
|
|
||||||
|
ReadyCloneTopology ==
|
||||||
|
phase = "ReadyCandidate" =>
|
||||||
|
\A left, right \in Names :
|
||||||
|
(candidatePolicy[left] = "Isolated" /\ candidatePolicy[right] = "Isolated")
|
||||||
|
=> ((capturedHostNames[left] = capturedHostNames[right])
|
||||||
|
<=> (isolatedNames[left] = isolatedNames[right]))
|
||||||
|
|
||||||
|
ReadyClonePayload ==
|
||||||
|
phase = "ReadyCandidate" =>
|
||||||
|
\A name \in Names : candidatePolicy[name] = "Isolated" =>
|
||||||
|
objectValues[isolatedNames[name]] = capturedHostValues[capturedHostNames[name]]
|
||||||
|
|
||||||
|
BackingIdentitySeparated ==
|
||||||
|
\A name \in Names : isolatedNames[name] \notin HostObjects
|
||||||
|
|
||||||
|
UnchangedHostAtPublication ==
|
||||||
|
phase = "ReadyCandidate" =>
|
||||||
|
/\ hostNames = capturedHostNames
|
||||||
|
/\ \A object \in HostObjects : objectValues[object] = capturedHostValues[object]
|
||||||
|
|
||||||
|
NoUnsafeOutcome ==
|
||||||
|
/\ ~splitCloneAliases
|
||||||
|
/\ ~mergedCloneObjects
|
||||||
|
/\ ~crossBackingLinked
|
||||||
|
/\ ~linkedRuntimeRenameAdmitted
|
||||||
|
/\ ~unstableAliasCloneAdmitted
|
||||||
|
|
||||||
|
LinkSafety == ReadyCloneTopology /\ ReadyClonePayload /\ BackingIdentitySeparated
|
||||||
|
/\ UnchangedHostAtPublication /\ NoUnsafeOutcome
|
||||||
|
|
||||||
|
=============================================================================
|
||||||
|
|
@ -702,6 +702,7 @@ class VerificationTests(unittest.TestCase):
|
||||||
self.assertEqual(
|
self.assertEqual(
|
||||||
{module.name for module, _ in VERIFY.MODEL_CONFIGURATIONS},
|
{module.name for module, _ in VERIFY.MODEL_CONFIGURATIONS},
|
||||||
{
|
{
|
||||||
|
"IgnoredWorkspaceHardlinkRouting.tla",
|
||||||
"IgnoredWorkspaceRouting.tla",
|
"IgnoredWorkspaceRouting.tla",
|
||||||
"Lazaret.tla",
|
"Lazaret.tla",
|
||||||
"PreparedLower.tla",
|
"PreparedLower.tla",
|
||||||
|
|
|
||||||
|
|
@ -24,6 +24,10 @@ MODEL_CONFIGURATIONS = (
|
||||||
ROOT / "docs/protocol/IgnoredWorkspaceRouting.tla",
|
ROOT / "docs/protocol/IgnoredWorkspaceRouting.tla",
|
||||||
ROOT / "docs/protocol/IgnoredWorkspaceRouting.cfg",
|
ROOT / "docs/protocol/IgnoredWorkspaceRouting.cfg",
|
||||||
),
|
),
|
||||||
|
(
|
||||||
|
ROOT / "docs/protocol/IgnoredWorkspaceHardlinkRouting.tla",
|
||||||
|
ROOT / "docs/protocol/IgnoredWorkspaceHardlinkRouting.cfg",
|
||||||
|
),
|
||||||
(ROOT / "docs/protocol/PreparedLower.tla", ROOT / "docs/protocol/PreparedLower.cfg"),
|
(ROOT / "docs/protocol/PreparedLower.tla", ROOT / "docs/protocol/PreparedLower.cfg"),
|
||||||
)
|
)
|
||||||
NEXTEST_COMMAND = (
|
NEXTEST_COMMAND = (
|
||||||
|
|
@ -816,7 +820,7 @@ def main() -> int:
|
||||||
prog="tools/verify",
|
prog="tools/verify",
|
||||||
description=(
|
description=(
|
||||||
"Run formatting, Clippy, cargo-nextest, documentation tests, dependency "
|
"Run formatting, Clippy, cargo-nextest, documentation tests, dependency "
|
||||||
"policy, process-control policy, and both TLA+ models. Cargo operations "
|
"policy, process-control policy, and all TLA+ models. Cargo operations "
|
||||||
"are offline and locked; tests use exact cargo-nextest 0.9.140 and "
|
"are offline and locked; tests use exact cargo-nextest 0.9.140 and "
|
||||||
"orchestration uses exact uv 0.11.28 with Python 3.11 or newer."
|
"orchestration uses exact uv 0.11.28 with Python 3.11 or newer."
|
||||||
)
|
)
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue