docs: record tier 5.7 runtime coupling model
This commit is contained in:
parent
6c3aeca239
commit
9ee90df968
2 changed files with 446 additions and 41 deletions
|
|
@ -58,6 +58,11 @@ INVARIANTS
|
|||
SandboxNamespaceIsolation
|
||||
OrderedNetworkStartup
|
||||
PublishedDomainsReady
|
||||
DomainLockLifetime
|
||||
RuntimeCausalEdgeArmedBeforeSandbox
|
||||
RuntimeCausalEdgeOwnerPresent
|
||||
SandboxRunningImpliesCoordinatorPresent
|
||||
PublishedRuntimeAuthorityPresent
|
||||
ExclusiveBootstrapOwnership
|
||||
TeardownNotJoinable
|
||||
RegisteredSessionsConnected
|
||||
|
|
|
|||
|
|
@ -111,6 +111,8 @@ DomainPhases == {
|
|||
CoordinatorStates == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
|
||||
MountStates == {"Unmounted", "Mounted"}
|
||||
ResourceStates == {"Stopped", "Ready", "Failed"}
|
||||
PhysicalProcessStates == {"Absent", "Starting", "Alive", "Stopped", "Dead"}
|
||||
RuntimeCausalEdgeStates == {"Unarmed", "Armed"}
|
||||
SessionPhases == {
|
||||
"New", "Waiting", "Registering", "Attached", "Prompting",
|
||||
"HostExecuting", "Closed", "Failed"
|
||||
|
|
@ -228,7 +230,13 @@ VARIABLES
|
|||
requestPhase,
|
||||
approvalSource,
|
||||
approvedCommand,
|
||||
hostRunning
|
||||
hostRunning,
|
||||
domainLockHeld,
|
||||
hostCoordinatorProc,
|
||||
runtimeSupervisorProc,
|
||||
attachedRunscProc,
|
||||
runtimeCausalEdge,
|
||||
runtimeFaultsRemaining
|
||||
|
||||
vars == <<
|
||||
domainPhase,
|
||||
|
|
@ -248,7 +256,13 @@ vars == <<
|
|||
requestPhase,
|
||||
approvalSource,
|
||||
approvedCommand,
|
||||
hostRunning
|
||||
hostRunning,
|
||||
domainLockHeld,
|
||||
hostCoordinatorProc,
|
||||
runtimeSupervisorProc,
|
||||
attachedRunscProc,
|
||||
runtimeCausalEdge,
|
||||
runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
Dom(s) == SessionDomain[s]
|
||||
|
|
@ -256,10 +270,39 @@ ReqSession(r) == RequestSession[r]
|
|||
ReqDomain(r) == Dom(ReqSession(r))
|
||||
IsTerminalRequest(r) == requestPhase[r] \in TerminalRequestPhases
|
||||
|
||||
RuntimeIdentityTupleReady(d) ==
|
||||
ProcessPresent(state) == state \in {"Alive", "Stopped"}
|
||||
|
||||
ProcessResponsive(state) == state = "Alive"
|
||||
|
||||
RuntimeLogicalAuthorityPresent(d) ==
|
||||
\/ ProcessPresent(hostCoordinatorProc[d])
|
||||
\/ ProcessPresent(runtimeSupervisorProc[d])
|
||||
\/ ProcessPresent(attachedRunscProc[d])
|
||||
|
||||
RuntimeAuthorityResponsive(d) ==
|
||||
\/ ProcessResponsive(hostCoordinatorProc[d])
|
||||
\/ ProcessResponsive(runtimeSupervisorProc[d])
|
||||
\/ ProcessResponsive(attachedRunscProc[d])
|
||||
|
||||
RuntimeGenerationAbsent(d) ==
|
||||
/\ ~domainLockHeld[d]
|
||||
/\ hostCoordinatorProc[d] = "Absent"
|
||||
/\ runtimeSupervisorProc[d] = "Absent"
|
||||
/\ attachedRunscProc[d] = "Absent"
|
||||
/\ runtimeCausalEdge[d] = "Unarmed"
|
||||
|
||||
ConsumeRuntimeFault(d) ==
|
||||
/\ runtimeFaultsRemaining[d] > 0
|
||||
/\ runtimeFaultsRemaining' =
|
||||
[runtimeFaultsRemaining EXCEPT ![d] = @ - 1]
|
||||
|
||||
RuntimeIdentityTupleAuthorized(d) ==
|
||||
/\ trustReady[d]
|
||||
/\ domainPhase[d] = "Ready"
|
||||
/\ d \in published
|
||||
/\ sidecarState[d] = "Ready"
|
||||
/\ sandboxState[d] = "Ready"
|
||||
/\ RuntimeLogicalAuthorityPresent(d)
|
||||
/\ CoordinatorCertificateValid[d]
|
||||
/\ SidecarCertificateValid[d]
|
||||
/\ SandboxCertificateValid[d]
|
||||
|
|
@ -269,6 +312,11 @@ RuntimeIdentityTupleReady(d) ==
|
|||
DomainSandboxIdentity[d]
|
||||
}) = 3
|
||||
|
||||
RuntimeIdentityTupleReady(d) ==
|
||||
/\ RuntimeIdentityTupleAuthorized(d)
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ RuntimeAuthorityResponsive(d)
|
||||
|
||||
SessionIdentityTupleRegistered(s) ==
|
||||
/\ s \in registered[Dom(s)]
|
||||
/\ s \in connected[Dom(s)]
|
||||
|
|
@ -320,6 +368,12 @@ Init ==
|
|||
/\ approvalSource = [r \in Requests |-> NoApproval]
|
||||
/\ approvedCommand = [r \in Requests |-> NoCommand]
|
||||
/\ hostRunning = {}
|
||||
/\ domainLockHeld = [d \in Domains |-> FALSE]
|
||||
/\ hostCoordinatorProc = [d \in Domains |-> "Absent"]
|
||||
/\ runtimeSupervisorProc = [d \in Domains |-> "Absent"]
|
||||
/\ attachedRunscProc = [d \in Domains |-> "Absent"]
|
||||
/\ runtimeCausalEdge = [d \in Domains |-> "Unarmed"]
|
||||
/\ runtimeFaultsRemaining = [d \in Domains |-> 2]
|
||||
|
||||
(***************************************************************************
|
||||
Domain and Session lifecycle
|
||||
|
|
@ -330,20 +384,26 @@ StartNewDomain(s) ==
|
|||
/\ sessionPhase[s] = "New"
|
||||
/\ ConfigSafe[d]
|
||||
/\ domainPhase[d] = "Absent"
|
||||
/\ RuntimeGenerationAbsent(d)
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = s]
|
||||
/\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
|
||||
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, trustReady, published,
|
||||
registered, connected, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StartReadySession(s) ==
|
||||
LET d == Dom(s) IN
|
||||
/\ sessionPhase[s] = "New"
|
||||
/\ domainPhase[d] = "Ready"
|
||||
/\ d \in published
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
||||
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
|
||||
/\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
|
||||
|
|
@ -351,7 +411,8 @@ StartReadySession(s) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
terminalRoute, activeRequest, requestPhase, approvalSource,
|
||||
approvedCommand, hostRunning
|
||||
approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
WaitForDomain(s) ==
|
||||
|
|
@ -363,7 +424,8 @@ WaitForDomain(s) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
RestartWaitingDomain(s) ==
|
||||
|
|
@ -371,31 +433,38 @@ RestartWaitingDomain(s) ==
|
|||
/\ sessionPhase[s] = "Waiting"
|
||||
/\ ConfigSafe[d]
|
||||
/\ domainPhase[d] = "Absent"
|
||||
/\ RuntimeGenerationAbsent(d)
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = s]
|
||||
/\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, trustReady, published,
|
||||
registered, connected, sessionPhase, terminalRoute, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, runtimeSupervisorProc, attachedRunscProc,
|
||||
runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
MountStateAnchor(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ coordinatorState[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ stateAnchorState[d] = "Unmounted"
|
||||
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Mounted"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
|
||||
lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
CreateTrustAnchor(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ coordinatorState[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ ~trustReady[d]
|
||||
/\ CoordinatorCertificateValid[d]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = TRUE]
|
||||
|
|
@ -403,11 +472,13 @@ CreateTrustAnchor(d) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StartSidecar(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ stateAnchorState[d] = "Mounted"
|
||||
/\ trustReady[d]
|
||||
/\ SidecarCertificateValid[d]
|
||||
|
|
@ -417,26 +488,66 @@ StartSidecar(d) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sandboxState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StartRuntimeSupervisor(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ sidecarState[d] = "Ready"
|
||||
/\ runtimeSupervisorProc[d] = "Absent"
|
||||
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, hostCoordinatorProc, attachedRunscProc,
|
||||
runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
ArmRuntimeCausalEdge(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ runtimeSupervisorProc[d] = "Alive"
|
||||
/\ attachedRunscProc[d] = "Absent"
|
||||
/\ runtimeCausalEdge[d] = "Unarmed"
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Armed"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StartSandbox(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ runtimeSupervisorProc[d] = "Alive"
|
||||
/\ runtimeCausalEdge[d] = "Armed"
|
||||
/\ sidecarState[d] = "Ready"
|
||||
/\ sandboxState[d] = "Stopped"
|
||||
/\ attachedRunscProc[d] = "Absent"
|
||||
/\ SandboxIsolationSafe[d]
|
||||
/\ SandboxCertificateValid[d]
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
||||
hostCoordinatorProc, runtimeSupervisorProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
PublishDomain(d) ==
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ coordinatorState[d] = "Starting"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ RuntimeAuthorityResponsive(d)
|
||||
/\ stateAnchorState[d] = "Mounted"
|
||||
/\ sidecarState[d] = "Ready"
|
||||
/\ sandboxState[d] = "Ready"
|
||||
|
|
@ -449,13 +560,16 @@ PublishDomain(d) ==
|
|||
stateAnchorState, sidecarState, sandboxState, trustReady, registered,
|
||||
connected, sessionPhase, terminalRoute, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
AdvanceWaitingSession(s) ==
|
||||
LET d == Dom(s) IN
|
||||
/\ sessionPhase[s] = "Waiting"
|
||||
/\ domainPhase[d] = "Ready"
|
||||
/\ d \in published
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
||||
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
|
||||
/\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
|
||||
|
|
@ -463,7 +577,8 @@ AdvanceWaitingSession(s) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
terminalRoute, activeRequest, requestPhase, approvalSource,
|
||||
approvedCommand, hostRunning
|
||||
approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
RejectConfigurationMismatch(s) ==
|
||||
|
|
@ -478,7 +593,8 @@ RejectConfigurationMismatch(s) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
RegisterSession(s) ==
|
||||
|
|
@ -486,6 +602,8 @@ RegisterSession(s) ==
|
|||
/\ sessionPhase[s] = "Registering"
|
||||
/\ connectionState[s] = "Connected"
|
||||
/\ domainPhase[d] = "Ready"
|
||||
/\ d \in published
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
||||
/\ CliCertificateValid[s]
|
||||
/\ registered' = [registered EXCEPT ![d] = @ \cup {s}]
|
||||
|
|
@ -496,7 +614,8 @@ RegisterSession(s) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
DisconnectSession(s) ==
|
||||
|
|
@ -530,11 +649,13 @@ DisconnectSession(s) ==
|
|||
/\ published' = IF leaderLost THEN published \ {d} ELSE published
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, approvalSource,
|
||||
approvedCommand
|
||||
approvedCommand, domainLockHeld, hostCoordinatorProc,
|
||||
runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
BeginTeardown(d) ==
|
||||
/\ domainPhase[d] = "Ready"
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ Interested(d) = {}
|
||||
/\ registered[d] = {}
|
||||
/\ connected[d] = {}
|
||||
|
|
@ -545,18 +666,23 @@ BeginTeardown(d) ==
|
|||
stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
|
||||
registered, connected, sessionPhase, terminalRoute, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StopSandbox(d) ==
|
||||
/\ domainPhase[d] = "Stopping"
|
||||
/\ RuntimeAuthorityResponsive(d)
|
||||
/\ sandboxState[d] = "Ready"
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
||||
hostCoordinatorProc, runtimeSupervisorProc, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StopSidecar(d) ==
|
||||
|
|
@ -568,7 +694,8 @@ StopSidecar(d) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sandboxState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
UnmountStateAnchor(d) ==
|
||||
|
|
@ -581,7 +708,8 @@ UnmountStateAnchor(d) ==
|
|||
domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
|
||||
lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
FinishTeardown(d) ==
|
||||
|
|
@ -593,11 +721,16 @@ FinishTeardown(d) ==
|
|||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = FALSE]
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Absent"]
|
||||
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Absent"]
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, published, registered,
|
||||
connected, sessionPhase, terminalRoute, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
(***************************************************************************
|
||||
|
|
@ -624,7 +757,8 @@ ReceiveEscalation(r) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, approvalSource,
|
||||
approvedCommand, hostRunning
|
||||
approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
AutoApprove(r) ==
|
||||
|
|
@ -637,7 +771,8 @@ AutoApprove(r) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
QueuePrompt(r) ==
|
||||
|
|
@ -648,7 +783,8 @@ QueuePrompt(r) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
BeginPrompt(r) ==
|
||||
|
|
@ -662,7 +798,8 @@ BeginPrompt(r) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, requestPhase, approvalSource,
|
||||
approvedCommand, hostRunning
|
||||
approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
DeveloperApprove(r, cmd) ==
|
||||
|
|
@ -678,7 +815,8 @@ DeveloperApprove(r, cmd) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
DeveloperDeny(r) ==
|
||||
|
|
@ -693,7 +831,8 @@ DeveloperDeny(r) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StartHostExecution(r) ==
|
||||
|
|
@ -712,7 +851,9 @@ StartHostExecution(r) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, approvalSource, approvedCommand
|
||||
connectionState, activeRequest, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
CompleteHostExecution(r) ==
|
||||
|
|
@ -726,7 +867,9 @@ CompleteHostExecution(r) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, approvalSource, approvedCommand
|
||||
connectionState, activeRequest, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
TimeoutRequest(r) ==
|
||||
|
|
@ -740,7 +883,9 @@ TimeoutRequest(r) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, approvalSource, approvedCommand
|
||||
connectionState, activeRequest, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
CancelRequest(r) ==
|
||||
|
|
@ -757,7 +902,9 @@ CancelRequest(r) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, approvalSource, approvedCommand
|
||||
connectionState, activeRequest, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
FailHostExecution(r) ==
|
||||
|
|
@ -772,7 +919,9 @@ FailHostExecution(r) ==
|
|||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
connectionState, activeRequest, approvalSource, approvedCommand
|
||||
connectionState, activeRequest, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
DeliverResult(r) ==
|
||||
|
|
@ -788,7 +937,8 @@ DeliverResult(r) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, approvalSource,
|
||||
approvedCommand, hostRunning
|
||||
approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
(***************************************************************************
|
||||
|
|
@ -821,7 +971,188 @@ FailDomain(d) ==
|
|||
/\ hostRunning' = hostRunning \ RequestsForDomain(d)
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, approvalSource,
|
||||
approvedCommand
|
||||
approvedCommand, domainLockHeld, hostCoordinatorProc,
|
||||
runtimeSupervisorProc, attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
HardLoseHostCoordinator(d) ==
|
||||
/\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
|
||||
/\ ProcessPresent(hostCoordinatorProc[d])
|
||||
/\ ConsumeRuntimeFault(d)
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ published' = published \ {d}
|
||||
/\ registered' = [registered EXCEPT ![d] = {}]
|
||||
/\ connected' = [connected EXCEPT ![d] = {}]
|
||||
/\ sessionPhase' = [s \in Sessions |->
|
||||
IF Dom(s) = d /\ sessionPhase[s] \notin {"New", "Closed"}
|
||||
THEN "Failed"
|
||||
ELSE sessionPhase[s]]
|
||||
/\ terminalRoute' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN "Detached" ELSE terminalRoute[s]]
|
||||
/\ connectionState' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN "Disconnected" ELSE connectionState[s]]
|
||||
/\ activeRequest' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN NoRequest ELSE activeRequest[s]]
|
||||
/\ requestPhase' = [r \in Requests |->
|
||||
IF ReqDomain(r) = d /\ requestPhase[r] # "Unused" /\ ~IsTerminalRequest(r)
|
||||
THEN "Failed"
|
||||
ELSE requestPhase[r]]
|
||||
/\ hostRunning' = hostRunning \ RequestsForDomain(d)
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Dead"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, approvalSource,
|
||||
approvedCommand, domainLockHeld, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge
|
||||
>>
|
||||
|
||||
HardLoseRuntimeSupervisor(d) ==
|
||||
/\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
|
||||
/\ ProcessPresent(runtimeSupervisorProc[d])
|
||||
/\ ConsumeRuntimeFault(d)
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ published' = published \ {d}
|
||||
/\ registered' = [registered EXCEPT ![d] = {}]
|
||||
/\ connected' = [connected EXCEPT ![d] = {}]
|
||||
/\ sessionPhase' = [s \in Sessions |->
|
||||
IF Dom(s) = d /\ sessionPhase[s] \notin {"New", "Closed"}
|
||||
THEN "Failed"
|
||||
ELSE sessionPhase[s]]
|
||||
/\ terminalRoute' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN "Detached" ELSE terminalRoute[s]]
|
||||
/\ connectionState' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN "Disconnected" ELSE connectionState[s]]
|
||||
/\ activeRequest' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN NoRequest ELSE activeRequest[s]]
|
||||
/\ requestPhase' = [r \in Requests |->
|
||||
IF ReqDomain(r) = d /\ requestPhase[r] # "Unused" /\ ~IsTerminalRequest(r)
|
||||
THEN "Failed"
|
||||
ELSE requestPhase[r]]
|
||||
/\ hostRunning' = hostRunning \ RequestsForDomain(d)
|
||||
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT
|
||||
![d] = IF runtimeCausalEdge[d] = "Armed" THEN "Dead" ELSE @]
|
||||
/\ sandboxState' = [sandboxState EXCEPT
|
||||
![d] = IF runtimeCausalEdge[d] = "Armed" THEN "Stopped" ELSE @]
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc
|
||||
>>
|
||||
|
||||
HardLoseAttachedRunsc(d) ==
|
||||
/\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
|
||||
/\ ProcessPresent(attachedRunscProc[d])
|
||||
/\ ConsumeRuntimeFault(d)
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ published' = published \ {d}
|
||||
/\ registered' = [registered EXCEPT ![d] = {}]
|
||||
/\ connected' = [connected EXCEPT ![d] = {}]
|
||||
/\ sessionPhase' = [s \in Sessions |->
|
||||
IF Dom(s) = d /\ sessionPhase[s] \notin {"New", "Closed"}
|
||||
THEN "Failed"
|
||||
ELSE sessionPhase[s]]
|
||||
/\ terminalRoute' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN "Detached" ELSE terminalRoute[s]]
|
||||
/\ connectionState' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN "Disconnected" ELSE connectionState[s]]
|
||||
/\ activeRequest' = [s \in Sessions |->
|
||||
IF Dom(s) = d THEN NoRequest ELSE activeRequest[s]]
|
||||
/\ requestPhase' = [r \in Requests |->
|
||||
IF ReqDomain(r) = d /\ requestPhase[r] # "Unused" /\ ~IsTerminalRequest(r)
|
||||
THEN "Failed"
|
||||
ELSE requestPhase[r]]
|
||||
/\ hostRunning' = hostRunning \ RequestsForDomain(d)
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Dead"]
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, approvalSource, approvedCommand,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc
|
||||
>>
|
||||
|
||||
StopHostCoordinatorProcess(d) ==
|
||||
/\ domainPhase[d] \in {"Starting", "Ready", "Stopping", "Failed"}
|
||||
/\ hostCoordinatorProc[d] = "Alive"
|
||||
/\ ConsumeRuntimeFault(d)
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Stopped"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, runtimeSupervisorProc, attachedRunscProc,
|
||||
runtimeCausalEdge
|
||||
>>
|
||||
|
||||
ResumeHostCoordinatorProcess(d) ==
|
||||
/\ hostCoordinatorProc[d] = "Stopped"
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, runtimeSupervisorProc, attachedRunscProc,
|
||||
runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StopRuntimeSupervisorProcess(d) ==
|
||||
/\ runtimeSupervisorProc[d] = "Alive"
|
||||
/\ ConsumeRuntimeFault(d)
|
||||
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Stopped"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, hostCoordinatorProc, attachedRunscProc,
|
||||
runtimeCausalEdge
|
||||
>>
|
||||
|
||||
ResumeRuntimeSupervisorProcess(d) ==
|
||||
/\ runtimeSupervisorProc[d] = "Stopped"
|
||||
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, hostCoordinatorProc, attachedRunscProc,
|
||||
runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
StopAttachedRunscProcess(d) ==
|
||||
/\ attachedRunscProc[d] = "Alive"
|
||||
/\ ConsumeRuntimeFault(d)
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Stopped"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
runtimeCausalEdge
|
||||
>>
|
||||
|
||||
ResumeAttachedRunscProcess(d) ==
|
||||
/\ attachedRunscProc[d] = "Stopped"
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, registered, connected,
|
||||
sessionPhase, terminalRoute, connectionState, activeRequest,
|
||||
requestPhase, approvalSource, approvedCommand, hostRunning,
|
||||
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
BeginRecovery(d) ==
|
||||
|
|
@ -831,22 +1162,28 @@ BeginRecovery(d) ==
|
|||
/\ hostRunning \cap RequestsForDomain(d) = {}
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Recovering"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Stopping"]
|
||||
/\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = TRUE]
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Alive"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
|
||||
published, registered, connected, sessionPhase, terminalRoute,
|
||||
connectionState, activeRequest, requestPhase, approvalSource,
|
||||
approvedCommand, hostRunning
|
||||
approvedCommand, hostRunning, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
RecoverSandbox(d) ==
|
||||
/\ domainPhase[d] = "Recovering"
|
||||
/\ sandboxState[d] # "Stopped"
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Dead"]
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld,
|
||||
hostCoordinatorProc, runtimeSupervisorProc, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
RecoverSidecar(d) ==
|
||||
|
|
@ -858,7 +1195,8 @@ RecoverSidecar(d) ==
|
|||
domainPhase, coordinatorState, stateAnchorState, sandboxState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
RecoverStateAnchor(d) ==
|
||||
|
|
@ -871,7 +1209,8 @@ RecoverStateAnchor(d) ==
|
|||
domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
|
||||
lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
approvalSource, approvedCommand, hostRunning, domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
|
||||
attachedRunscProc, runtimeCausalEdge, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
FinishRecovery(d) ==
|
||||
|
|
@ -882,17 +1221,25 @@ FinishRecovery(d) ==
|
|||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
||||
/\ domainLockHeld' = [domainLockHeld EXCEPT ![d] = FALSE]
|
||||
/\ hostCoordinatorProc' = [hostCoordinatorProc EXCEPT ![d] = "Absent"]
|
||||
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Absent"]
|
||||
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
|
||||
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, trustReady, published,
|
||||
stateAnchorState, sidecarState, sandboxState, published,
|
||||
registered, connected, sessionPhase, terminalRoute, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
hostRunning, runtimeFaultsRemaining
|
||||
>>
|
||||
|
||||
DomainProgress(d) ==
|
||||
\/ MountStateAnchor(d)
|
||||
\/ CreateTrustAnchor(d)
|
||||
\/ StartSidecar(d)
|
||||
\/ StartRuntimeSupervisor(d)
|
||||
\/ ArmRuntimeCausalEdge(d)
|
||||
\/ StartSandbox(d)
|
||||
\/ PublishDomain(d)
|
||||
\/ BeginTeardown(d)
|
||||
|
|
@ -905,6 +1252,20 @@ DomainProgress(d) ==
|
|||
\/ RecoverSidecar(d)
|
||||
\/ RecoverStateAnchor(d)
|
||||
\/ FinishRecovery(d)
|
||||
\/ ResumeHostCoordinatorProcess(d)
|
||||
\/ ResumeRuntimeSupervisorProcess(d)
|
||||
\/ ResumeAttachedRunscProcess(d)
|
||||
|
||||
RuntimePhysicalInterleaving(d) ==
|
||||
\/ HardLoseHostCoordinator(d)
|
||||
\/ HardLoseRuntimeSupervisor(d)
|
||||
\/ HardLoseAttachedRunsc(d)
|
||||
\/ StopHostCoordinatorProcess(d)
|
||||
\/ ResumeHostCoordinatorProcess(d)
|
||||
\/ StopRuntimeSupervisorProcess(d)
|
||||
\/ ResumeRuntimeSupervisorProcess(d)
|
||||
\/ StopAttachedRunscProcess(d)
|
||||
\/ ResumeAttachedRunscProcess(d)
|
||||
|
||||
SessionProgress(s) ==
|
||||
\/ StartNewDomain(s)
|
||||
|
|
@ -936,6 +1297,8 @@ Next ==
|
|||
RegisterSession(s) \/ DisconnectSession(s))
|
||||
\/ (\E d \in Domains :
|
||||
DomainProgress(d) \/ FailDomain(d))
|
||||
\/ (\E d \in Domains :
|
||||
RuntimePhysicalInterleaving(d))
|
||||
\/ (\E r \in Requests :
|
||||
ReceiveEscalation(r) \/ RequestProgress(r))
|
||||
|
||||
|
|
@ -969,6 +1332,12 @@ TypeOK ==
|
|||
/\ approvalSource \in [Requests -> ApprovalSources]
|
||||
/\ approvedCommand \in [Requests -> Commands \cup {NoCommand}]
|
||||
/\ hostRunning \subseteq Requests
|
||||
/\ domainLockHeld \in [Domains -> BOOLEAN]
|
||||
/\ hostCoordinatorProc \in [Domains -> PhysicalProcessStates]
|
||||
/\ runtimeSupervisorProc \in [Domains -> PhysicalProcessStates]
|
||||
/\ attachedRunscProc \in [Domains -> PhysicalProcessStates]
|
||||
/\ runtimeCausalEdge \in [Domains -> RuntimeCausalEdgeStates]
|
||||
/\ runtimeFaultsRemaining \in [Domains -> 0..2]
|
||||
|
||||
ConfigurationConfinement ==
|
||||
\A d \in Domains : domainPhase[d] # "Absent" => ConfigSafe[d]
|
||||
|
|
@ -988,6 +1357,32 @@ PublishedDomainsReady ==
|
|||
/\ sandboxState[d] = "Ready"
|
||||
/\ trustReady[d]
|
||||
|
||||
DomainLockLifetime ==
|
||||
\A d \in Domains :
|
||||
/\ (domainPhase[d] = "Absent" => ~domainLockHeld[d])
|
||||
/\ (domainPhase[d] # "Absent" => domainLockHeld[d])
|
||||
/\ (~domainLockHeld[d] => RuntimeGenerationAbsent(d))
|
||||
|
||||
RuntimeCausalEdgeArmedBeforeSandbox ==
|
||||
\A d \in Domains :
|
||||
sandboxState[d] = "Ready" =>
|
||||
/\ runtimeCausalEdge[d] = "Armed"
|
||||
/\ ProcessPresent(attachedRunscProc[d])
|
||||
|
||||
RuntimeCausalEdgeOwnerPresent ==
|
||||
\A d \in Domains :
|
||||
runtimeCausalEdge[d] = "Armed" =>
|
||||
/\ domainLockHeld[d]
|
||||
/\ ProcessPresent(runtimeSupervisorProc[d])
|
||||
|
||||
SandboxRunningImpliesCoordinatorPresent ==
|
||||
\A d \in Domains :
|
||||
sandboxState[d] = "Ready" => RuntimeLogicalAuthorityPresent(d)
|
||||
|
||||
PublishedRuntimeAuthorityPresent ==
|
||||
\A d \in published :
|
||||
RuntimeLogicalAuthorityPresent(d)
|
||||
|
||||
ExclusiveBootstrapOwnership ==
|
||||
\A d \in Domains : lockOwner[d] # NoSession =>
|
||||
/\ domainPhase[d] = "Starting"
|
||||
|
|
@ -1043,7 +1438,7 @@ RegisteredSessionIdentityUniqueness ==
|
|||
LiveRequestIdentityAuthorized ==
|
||||
\A r \in Requests :
|
||||
requestPhase[r] \notin {"Unused"} \cup TerminalRequestPhases =>
|
||||
/\ RuntimeIdentityTupleReady(ReqDomain(r))
|
||||
/\ RuntimeIdentityTupleAuthorized(ReqDomain(r))
|
||||
/\ SessionIdentityTupleRegistered(ReqSession(r))
|
||||
|
||||
DeveloperApprovalAuthenticated ==
|
||||
|
|
@ -1112,6 +1507,11 @@ Safety ==
|
|||
/\ SandboxNamespaceIsolation
|
||||
/\ OrderedNetworkStartup
|
||||
/\ PublishedDomainsReady
|
||||
/\ DomainLockLifetime
|
||||
/\ RuntimeCausalEdgeArmedBeforeSandbox
|
||||
/\ RuntimeCausalEdgeOwnerPresent
|
||||
/\ SandboxRunningImpliesCoordinatorPresent
|
||||
/\ PublishedRuntimeAuthorityPresent
|
||||
/\ ExclusiveBootstrapOwnership
|
||||
/\ TeardownNotJoinable
|
||||
/\ RegisteredSessionsConnected
|
||||
|
|
|
|||
Loading…
Reference in a new issue