Specify fenced activation and source credential contracts
Define bounded reservation recovery, exact activation replay fencing, immutable source identities, and deployment-owned secret and target policy boundaries. Align the OpenAPI contract and add a split-store activation safety refinement.
This commit is contained in:
parent
3881514e4b
commit
033cfeaac6
1 changed files with 877 additions and 49 deletions
307
docs/protocol/RemoraClaimActivation.tla
Normal file
307
docs/protocol/RemoraClaimActivation.tla
Normal file
|
|
@ -0,0 +1,307 @@
|
|||
---------------------- MODULE RemoraClaimActivation ----------------------
|
||||
EXTENDS Naturals
|
||||
|
||||
\* Split-store refinement of the atomic JobProtocol ActivateAttempt action.
|
||||
\* Durable execution is the linearization point; lease creation alone is not authority.
|
||||
|
||||
CONSTANTS
|
||||
Claims, Fences, Workers, Operations,
|
||||
NoWorker, NoOwner, NoRequest, NoResponse, Accepted, Rejected
|
||||
|
||||
RequestKeys == Claims \X Fences \X Workers
|
||||
|
||||
ASSUME /\ Claims # {}
|
||||
/\ Fences # {}
|
||||
/\ Workers # {}
|
||||
/\ Operations # {}
|
||||
/\ NoWorker \notin Workers
|
||||
/\ NoRequest \notin RequestKeys
|
||||
|
||||
Authorized == "Authorized"
|
||||
Executing == "Executing"
|
||||
Reaped == "Reaped"
|
||||
DurableStates == {Authorized, Executing, Reaped}
|
||||
|
||||
Idle == "Idle"
|
||||
Validated == "Validated"
|
||||
LeaseCreated == "LeaseCreated"
|
||||
Committed == "Committed"
|
||||
Finished == "Finished"
|
||||
ActivationStages == {Idle, Validated, LeaseCreated, Committed, Finished}
|
||||
|
||||
Activator == "Activator"
|
||||
Recovery == "Recovery"
|
||||
LockOwners == {NoOwner, Activator, Recovery}
|
||||
Responses == {NoResponse, Accepted, Rejected}
|
||||
|
||||
VARIABLES
|
||||
durableState, attemptFence, attemptWorker, reservation, lease,
|
||||
activationStage, durableLock, operationRequest, operationResponse,
|
||||
conflictRequest, activationEffectCount
|
||||
|
||||
vars == <<durableState, attemptFence, attemptWorker, reservation, lease,
|
||||
activationStage, durableLock, operationRequest, operationResponse,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
Request(c, f, w) == <<c, f, w>>
|
||||
ExactRequest(c) == Request(c, attemptFence[c], attemptWorker[c])
|
||||
|
||||
Init ==
|
||||
/\ durableState = [c \in Claims |-> Authorized]
|
||||
/\ attemptFence \in [Claims -> Fences]
|
||||
/\ attemptWorker \in [Claims -> Workers]
|
||||
/\ reservation = attemptWorker
|
||||
/\ lease = [c \in Claims |-> NoWorker]
|
||||
/\ activationStage = [c \in Claims |-> Idle]
|
||||
/\ durableLock = [c \in Claims |-> NoOwner]
|
||||
/\ operationRequest = [op \in Operations |-> NoRequest]
|
||||
/\ operationResponse = [op \in Operations |-> NoResponse]
|
||||
/\ conflictRequest = [op \in Operations |-> NoRequest]
|
||||
/\ activationEffectCount = [c \in Claims |-> 0]
|
||||
|
||||
BindOperation(op, c, f, w) ==
|
||||
/\ operationRequest[op] = NoRequest
|
||||
/\ operationRequest' =
|
||||
[operationRequest EXCEPT ![op] = Request(c, f, w)]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, activationStage, durableLock, operationResponse,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
RejectOperationReuse(op, c, f, w) ==
|
||||
/\ operationRequest[op] # NoRequest
|
||||
/\ operationRequest[op] # Request(c, f, w)
|
||||
/\ conflictRequest' =
|
||||
[conflictRequest EXCEPT ![op] = Request(c, f, w)]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, activationStage, durableLock, operationRequest,
|
||||
operationResponse, activationEffectCount>>
|
||||
|
||||
StartActivation(op, c, f, w) ==
|
||||
/\ operationRequest[op] = Request(c, f, w)
|
||||
/\ operationResponse[op] = NoResponse
|
||||
/\ Request(c, f, w) = ExactRequest(c)
|
||||
/\ activationStage[c] = Idle
|
||||
/\ durableState[c] = Authorized
|
||||
/\ reservation[c] = w
|
||||
/\ activationStage' = [activationStage EXCEPT ![c] = Validated]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, durableLock, operationRequest, operationResponse,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
CreateLease(c) ==
|
||||
LET w == attemptWorker[c]
|
||||
IN /\ activationStage[c] = Validated
|
||||
/\ durableState[c] = Authorized
|
||||
/\ reservation[c] = w
|
||||
/\ lease[c] = NoWorker
|
||||
/\ lease' = [lease EXCEPT ![c] = w]
|
||||
/\ activationStage' = [activationStage EXCEPT ![c] = LeaseCreated]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
durableLock, operationRequest, operationResponse,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
AcquireActivationLock(c) ==
|
||||
/\ activationStage[c] = LeaseCreated
|
||||
/\ durableState[c] = Authorized
|
||||
/\ durableLock[c] = NoOwner
|
||||
/\ durableLock' = [durableLock EXCEPT ![c] = Activator]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, activationStage, operationRequest,
|
||||
operationResponse, conflictRequest,
|
||||
activationEffectCount>>
|
||||
|
||||
LoseActivatorLock(c) ==
|
||||
/\ durableLock[c] = Activator
|
||||
/\ durableLock' = [durableLock EXCEPT ![c] = NoOwner]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, activationStage, operationRequest,
|
||||
operationResponse, conflictRequest,
|
||||
activationEffectCount>>
|
||||
|
||||
CommitActivation(c) ==
|
||||
LET w == attemptWorker[c]
|
||||
IN /\ activationStage[c] = LeaseCreated
|
||||
/\ durableLock[c] = Activator
|
||||
/\ durableState[c] = Authorized
|
||||
/\ reservation[c] = w
|
||||
/\ lease[c] = w
|
||||
/\ durableState' = [durableState EXCEPT ![c] = Executing]
|
||||
/\ reservation' = [reservation EXCEPT ![c] = NoWorker]
|
||||
/\ activationStage' = [activationStage EXCEPT ![c] = Committed]
|
||||
/\ durableLock' = [durableLock EXCEPT ![c] = NoOwner]
|
||||
/\ activationEffectCount' =
|
||||
[activationEffectCount EXCEPT ![c] = @ + 1]
|
||||
/\ UNCHANGED <<attemptFence, attemptWorker, lease,
|
||||
operationRequest, operationResponse, conflictRequest>>
|
||||
|
||||
ReplayActivation(op, c, f, w) ==
|
||||
/\ operationRequest[op] = Request(c, f, w)
|
||||
/\ Request(c, f, w) = ExactRequest(c)
|
||||
/\ durableState[c] = Executing
|
||||
/\ lease[c] = w
|
||||
/\ activationEffectCount[c] = 1
|
||||
/\ operationResponse' =
|
||||
[operationResponse EXCEPT ![op] = Accepted]
|
||||
/\ activationStage' = [activationStage EXCEPT ![c] = Finished]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, durableLock, operationRequest, conflictRequest,
|
||||
activationEffectCount>>
|
||||
|
||||
RejectPrecondition(op, c, f, w) ==
|
||||
/\ operationRequest[op] = Request(c, f, w)
|
||||
/\ operationResponse[op] = NoResponse
|
||||
/\ \/ Request(c, f, w) # ExactRequest(c)
|
||||
\/ durableState[c] = Reaped
|
||||
\/ /\ durableState[c] = Executing
|
||||
/\ lease[c] # w
|
||||
/\ operationResponse' =
|
||||
[operationResponse EXCEPT ![op] = Rejected]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, activationStage, durableLock, operationRequest,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
ExpireReservation(c) ==
|
||||
/\ durableState[c] = Authorized
|
||||
/\ reservation[c] # NoWorker
|
||||
/\ lease[c] = NoWorker
|
||||
/\ reservation' = [reservation EXCEPT ![c] = NoWorker]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, lease,
|
||||
activationStage, durableLock, operationRequest,
|
||||
operationResponse, conflictRequest,
|
||||
activationEffectCount>>
|
||||
|
||||
ExpireLease(c) ==
|
||||
/\ durableState[c] = Executing
|
||||
/\ lease[c] = attemptWorker[c]
|
||||
/\ lease' = [lease EXCEPT ![c] = NoWorker]
|
||||
/\ operationResponse' =
|
||||
[op \in Operations |->
|
||||
IF operationResponse[op] = Accepted
|
||||
/\ operationRequest[op][1] = c
|
||||
THEN NoResponse ELSE operationResponse[op]]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
activationStage, durableLock, operationRequest,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
AcquireRecoveryLock(c) ==
|
||||
/\ durableState[c] = Authorized
|
||||
/\ durableLock[c] = NoOwner
|
||||
/\ durableLock' = [durableLock EXCEPT ![c] = Recovery]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
lease, activationStage, operationRequest,
|
||||
operationResponse, conflictRequest,
|
||||
activationEffectCount>>
|
||||
|
||||
FinishRecovery(c) ==
|
||||
/\ durableLock[c] = Recovery
|
||||
/\ durableState[c] = Authorized
|
||||
/\ durableState' = [durableState EXCEPT ![c] = Reaped]
|
||||
/\ reservation' = [reservation EXCEPT ![c] = NoWorker]
|
||||
/\ lease' = [lease EXCEPT ![c] = NoWorker]
|
||||
/\ durableLock' = [durableLock EXCEPT ![c] = NoOwner]
|
||||
/\ UNCHANGED <<attemptFence, attemptWorker, activationStage,
|
||||
operationRequest, operationResponse, conflictRequest,
|
||||
activationEffectCount>>
|
||||
|
||||
CompensateRejectedActivation(c) ==
|
||||
LET w == attemptWorker[c]
|
||||
IN /\ durableState[c] = Reaped
|
||||
/\ activationStage[c] \in {Validated, LeaseCreated}
|
||||
/\ lease[c] \in {NoWorker, w}
|
||||
/\ lease' = [lease EXCEPT ![c] = NoWorker]
|
||||
/\ activationStage' = [activationStage EXCEPT ![c] = Finished]
|
||||
/\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
|
||||
durableLock, operationRequest, operationResponse,
|
||||
conflictRequest, activationEffectCount>>
|
||||
|
||||
Done ==
|
||||
/\ \A c \in Claims : durableState[c] \in {Executing, Reaped}
|
||||
/\ UNCHANGED vars
|
||||
|
||||
Next ==
|
||||
\/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
|
||||
BindOperation(op, c, f, w)
|
||||
\/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
|
||||
RejectOperationReuse(op, c, f, w)
|
||||
\/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
|
||||
StartActivation(op, c, f, w)
|
||||
\/ \E c \in Claims : CreateLease(c)
|
||||
\/ \E c \in Claims : AcquireActivationLock(c)
|
||||
\/ \E c \in Claims : LoseActivatorLock(c)
|
||||
\/ \E c \in Claims : CommitActivation(c)
|
||||
\/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
|
||||
ReplayActivation(op, c, f, w)
|
||||
\/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
|
||||
RejectPrecondition(op, c, f, w)
|
||||
\/ \E c \in Claims : ExpireReservation(c)
|
||||
\/ \E c \in Claims : ExpireLease(c)
|
||||
\/ \E c \in Claims : AcquireRecoveryLock(c)
|
||||
\/ \E c \in Claims : FinishRecovery(c)
|
||||
\/ \E c \in Claims : CompensateRejectedActivation(c)
|
||||
\/ Done
|
||||
|
||||
Spec == Init /\ [][Next]_vars
|
||||
|
||||
TypeOK ==
|
||||
/\ durableState \in [Claims -> DurableStates]
|
||||
/\ attemptFence \in [Claims -> Fences]
|
||||
/\ attemptWorker \in [Claims -> Workers]
|
||||
/\ reservation \in [Claims -> Workers \cup {NoWorker}]
|
||||
/\ lease \in [Claims -> Workers \cup {NoWorker}]
|
||||
/\ activationStage \in [Claims -> ActivationStages]
|
||||
/\ durableLock \in [Claims -> LockOwners]
|
||||
/\ operationRequest \in [Operations -> RequestKeys \cup {NoRequest}]
|
||||
/\ operationResponse \in [Operations -> Responses]
|
||||
/\ conflictRequest \in [Operations -> RequestKeys \cup {NoRequest}]
|
||||
/\ activationEffectCount \in [Claims -> 0..1]
|
||||
|
||||
LiveLeaseMatchesAuthority ==
|
||||
\A c \in Claims :
|
||||
lease[c] # NoWorker => lease[c] = attemptWorker[c]
|
||||
|
||||
ExecutingIsCommitted ==
|
||||
\A c \in Claims :
|
||||
durableState[c] = Executing =>
|
||||
/\ reservation[c] = NoWorker
|
||||
/\ activationStage[c] \in {Committed, Finished}
|
||||
/\ activationEffectCount[c] = 1
|
||||
|
||||
AcceptedResponseIsExactReplay ==
|
||||
\A op \in Operations :
|
||||
operationResponse[op] = Accepted =>
|
||||
\E c \in Claims :
|
||||
/\ operationRequest[op] = ExactRequest(c)
|
||||
/\ durableState[c] = Executing
|
||||
/\ lease[c] = attemptWorker[c]
|
||||
/\ activationEffectCount[c] = 1
|
||||
|
||||
ConflictIsChangedRequest ==
|
||||
\A op \in Operations :
|
||||
conflictRequest[op] # NoRequest =>
|
||||
/\ operationRequest[op] # NoRequest
|
||||
/\ conflictRequest[op] # operationRequest[op]
|
||||
|
||||
ReapedClaimHasNoActivationEffect ==
|
||||
\A c \in Claims :
|
||||
durableState[c] = Reaped => activationEffectCount[c] = 0
|
||||
|
||||
ReapedCoordinationIsClean ==
|
||||
\A c \in Claims :
|
||||
durableState[c] = Reaped =>
|
||||
/\ reservation[c] = NoWorker
|
||||
/\ lease[c] = NoWorker
|
||||
|
||||
ActivationAppliesAtMostOnceAction ==
|
||||
\A c \in Claims :
|
||||
activationEffectCount[c] = 1 => activationEffectCount'[c] = 1
|
||||
|
||||
ActivationAppliesAtMostOnce == [][ActivationAppliesAtMostOnceAction]_vars
|
||||
|
||||
OperationRequestIsImmutableAction ==
|
||||
\A op \in Operations :
|
||||
operationRequest[op] # NoRequest =>
|
||||
operationRequest'[op] = operationRequest[op]
|
||||
|
||||
OperationRequestIsImmutable == [][OperationRequestIsImmutableAction]_vars
|
||||
|
||||
=============================================================================
|
||||
Loading…
Reference in a new issue