314 lines
12 KiB
Text
314 lines
12 KiB
Text
|
------------------ 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
|
||
|
|
|
||
|
|
=============================================================================
|