662 lines
22 KiB
Text
662 lines
22 KiB
Text
----------------------------- MODULE Nuthatch -----------------------------
|
|
EXTENDS FiniteSets, Naturals, TLC
|
|
|
|
\* This model covers authorized one-key mutations within one idempotency epoch;
|
|
\* lost bodies are not resumed and settle from the observed object state.
|
|
|
|
CONSTANTS
|
|
Users, OperationIds, EnabledKinds, PersonalKeyNames, SharedKeys, Contents,
|
|
MaxObjectSize, PersonalLimit, SharedLimit,
|
|
MaxPostgresLosses, MaxObjectStoreLosses,
|
|
SharedPool, NoObject, NoRecord, NoOwner, NoObservation
|
|
|
|
ASSUME
|
|
/\ Users # {}
|
|
/\ OperationIds # {}
|
|
/\ EnabledKinds # {}
|
|
/\ EnabledKinds \subseteq {"put", "delete"}
|
|
/\ PersonalKeyNames # {}
|
|
/\ SharedKeys # {}
|
|
/\ (Users \X PersonalKeyNames) \cap SharedKeys = {}
|
|
/\ Contents # {}
|
|
/\ SharedPool \notin Users
|
|
/\ NoObject \notin Contents
|
|
/\ MaxObjectSize \in Nat \ {0}
|
|
/\ PersonalLimit \in Nat
|
|
/\ SharedLimit \in Nat
|
|
/\ MaxPostgresLosses \in Nat
|
|
/\ MaxObjectStoreLosses \in Nat
|
|
|
|
PersonalKeys == Users \X PersonalKeyNames
|
|
Keys == PersonalKeys \cup SharedKeys
|
|
Pools == Users \cup {SharedPool}
|
|
Kinds == EnabledKinds
|
|
Identities == Users \X Kinds \X OperationIds
|
|
Sizes == 1..MaxObjectSize
|
|
|
|
ObjectValues ==
|
|
{NoObject} \cup
|
|
[size : Sizes, content : Contents]
|
|
|
|
Requests ==
|
|
[user : Users,
|
|
operation : OperationIds,
|
|
kind : Kinds,
|
|
key : Keys,
|
|
size : 0..MaxObjectSize,
|
|
content : Contents \cup {NoObject}]
|
|
|
|
ValidRequests ==
|
|
{request \in Requests :
|
|
/\ \/ request.key \in SharedKeys
|
|
\/ /\ request.key \in PersonalKeys
|
|
/\ request.key[1] = request.user
|
|
/\ IF request.kind = "put"
|
|
THEN /\ request.size \in Sizes
|
|
/\ request.content \in Contents
|
|
ELSE /\ request.size = 0
|
|
/\ request.content = NoObject}
|
|
|
|
RecordStates == {"prepared", "applying", "succeeded", "failed", "rejected"}
|
|
ActiveStates == {"prepared", "applying"}
|
|
TerminalStates == {"succeeded", "failed", "rejected"}
|
|
ExternalStates == {"idle", "pending", "settled"}
|
|
|
|
RecordValues ==
|
|
[request : ValidRequests,
|
|
prior : ObjectValues,
|
|
state : RecordStates]
|
|
|
|
Results == {"pending", "succeeded", "failed", "rejected", "conflict"}
|
|
Dispositions == {"first", "replay", "conflict"}
|
|
|
|
Observations ==
|
|
[request : ValidRequests,
|
|
result : Results,
|
|
disposition : Dispositions]
|
|
|
|
VARIABLES
|
|
objects,
|
|
usedBytes,
|
|
reservedBytes,
|
|
keyOwner,
|
|
records,
|
|
externalState,
|
|
uploadBodyAvailable,
|
|
postgresUp,
|
|
objectStoreUp,
|
|
postgresLosses,
|
|
objectStoreLosses,
|
|
observation
|
|
|
|
\* externalState is environmental truth: "settled" means no issued request can
|
|
\* later mutate its key. Process loss does not erase a pending store request.
|
|
|
|
vars == <<
|
|
objects,
|
|
usedBytes,
|
|
reservedBytes,
|
|
keyOwner,
|
|
records,
|
|
externalState,
|
|
uploadBodyAvailable,
|
|
postgresUp,
|
|
objectStoreUp,
|
|
postgresLosses,
|
|
objectStoreLosses,
|
|
observation
|
|
>>
|
|
|
|
Identity(request) == <<request.user, request.kind, request.operation>>
|
|
|
|
PoolOf(key) ==
|
|
IF key \in PersonalKeys THEN key[1] ELSE SharedPool
|
|
|
|
PoolKeys(pool) ==
|
|
IF pool = SharedPool
|
|
THEN SharedKeys
|
|
ELSE {key \in PersonalKeys : key[1] = pool}
|
|
|
|
Limit(pool) ==
|
|
IF pool = SharedPool THEN SharedLimit ELSE PersonalLimit
|
|
|
|
ObjectSize(object) ==
|
|
IF object = NoObject THEN 0 ELSE object.size
|
|
|
|
DesiredObject(request) ==
|
|
IF request.kind = "delete"
|
|
THEN NoObject
|
|
ELSE [size |-> request.size, content |-> request.content]
|
|
|
|
Growth(prior, desired) ==
|
|
IF ObjectSize(desired) > ObjectSize(prior)
|
|
THEN ObjectSize(desired) - ObjectSize(prior)
|
|
ELSE 0
|
|
|
|
RequestFingerprint(request) ==
|
|
<<request.kind, PoolOf(request.key), request.key,
|
|
request.size, request.content>>
|
|
|
|
RECURSIVE ObjectBytes(_, _)
|
|
|
|
ObjectBytes(objectMap, keys) ==
|
|
IF keys = {}
|
|
THEN 0
|
|
ELSE LET key == CHOOSE candidate \in keys : TRUE
|
|
IN ObjectSize(objectMap[key]) +
|
|
ObjectBytes(objectMap, keys \ {key})
|
|
|
|
Active(identity) ==
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state \in ActiveStates
|
|
|
|
Terminal(identity) ==
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state \in TerminalStates
|
|
|
|
Reservation(identity) ==
|
|
IF Active(identity)
|
|
THEN Growth(records[identity].prior,
|
|
DesiredObject(records[identity].request))
|
|
ELSE 0
|
|
|
|
RECURSIVE ReservationTotal(_, _)
|
|
|
|
ReservationTotal(identities, pool) ==
|
|
IF identities = {}
|
|
THEN 0
|
|
ELSE LET identity == CHOOSE candidate \in identities : TRUE
|
|
remainder == identities \ {identity}
|
|
amount ==
|
|
IF Active(identity) /\
|
|
PoolOf(records[identity].request.key) = pool
|
|
THEN Reservation(identity)
|
|
ELSE 0
|
|
IN amount + ReservationTotal(remainder, pool)
|
|
|
|
StateResult(state) ==
|
|
CASE state \in ActiveStates -> "pending"
|
|
[] state = "succeeded" -> "succeeded"
|
|
[] state = "failed" -> "failed"
|
|
[] state = "rejected" -> "rejected"
|
|
|
|
CanAdmit(request) ==
|
|
LET pool == PoolOf(request.key)
|
|
prior == objects[request.key]
|
|
desired == DesiredObject(request)
|
|
IN /\ keyOwner[request.key] = NoOwner
|
|
/\ usedBytes[pool] + reservedBytes[pool] +
|
|
Growth(prior, desired) <= Limit(pool)
|
|
|
|
Init ==
|
|
/\ objects \in [Keys -> ObjectValues]
|
|
/\ \A pool \in Pools :
|
|
ObjectBytes(objects, PoolKeys(pool)) <= Limit(pool)
|
|
/\ usedBytes =
|
|
[pool \in Pools |-> ObjectBytes(objects, PoolKeys(pool))]
|
|
/\ reservedBytes = [pool \in Pools |-> 0]
|
|
/\ keyOwner = [key \in Keys |-> NoOwner]
|
|
/\ records = [identity \in Identities |-> NoRecord]
|
|
/\ externalState = [identity \in Identities |-> "idle"]
|
|
/\ uploadBodyAvailable = [identity \in Identities |-> FALSE]
|
|
/\ postgresUp = TRUE
|
|
/\ objectStoreUp = TRUE
|
|
/\ postgresLosses = 0
|
|
/\ objectStoreLosses = 0
|
|
/\ observation = NoObservation
|
|
|
|
FirstRequest(request) ==
|
|
LET identity == Identity(request)
|
|
pool == PoolOf(request.key)
|
|
prior == objects[request.key]
|
|
desired == DesiredObject(request)
|
|
admitted == CanAdmit(request)
|
|
nextState == IF admitted THEN "prepared" ELSE "rejected"
|
|
record ==
|
|
[request |-> request, prior |-> prior, state |-> nextState]
|
|
growth == Growth(prior, desired)
|
|
IN /\ postgresUp
|
|
/\ records[identity] = NoRecord
|
|
/\ records' = [records EXCEPT ![identity] = record]
|
|
/\ reservedBytes' =
|
|
IF admitted
|
|
THEN [reservedBytes EXCEPT ![pool] = @ + growth]
|
|
ELSE reservedBytes
|
|
/\ keyOwner' =
|
|
IF admitted
|
|
THEN [keyOwner EXCEPT ![request.key] = identity]
|
|
ELSE keyOwner
|
|
/\ uploadBodyAvailable' =
|
|
[uploadBodyAvailable EXCEPT
|
|
![identity] = admitted /\ request.kind = "put"]
|
|
/\ observation' =
|
|
[request |-> request,
|
|
result |-> IF admitted THEN "pending" ELSE "rejected",
|
|
disposition |-> "first"]
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, externalState,
|
|
postgresUp, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
ReplayRequest(request) ==
|
|
LET identity == Identity(request)
|
|
record == records[identity]
|
|
IN /\ postgresUp
|
|
/\ record # NoRecord
|
|
/\ record.request = request
|
|
/\ observation' =
|
|
[request |-> request,
|
|
result |-> StateResult(record.state),
|
|
disposition |-> "replay"]
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
externalState, uploadBodyAvailable,
|
|
postgresUp, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
ConflictRequest(request) ==
|
|
LET identity == Identity(request)
|
|
record == records[identity]
|
|
IN /\ postgresUp
|
|
/\ record # NoRecord
|
|
/\ RequestFingerprint(record.request) # RequestFingerprint(request)
|
|
/\ observation' =
|
|
[request |-> request,
|
|
result |-> "conflict",
|
|
disposition |-> "conflict"]
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
externalState, uploadBodyAvailable,
|
|
postgresUp, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
PrepareEffect(identity) ==
|
|
/\ postgresUp
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state = "prepared"
|
|
/\ records' = [records EXCEPT ![identity].state = "applying"]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, externalState,
|
|
uploadBodyAvailable,
|
|
postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
DispatchEffect(identity) ==
|
|
/\ postgresUp
|
|
/\ objectStoreUp
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state = "applying"
|
|
/\ externalState[identity] = "idle"
|
|
/\ (records[identity].request.kind = "delete" \/
|
|
uploadBodyAvailable[identity])
|
|
/\ externalState' =
|
|
[externalState EXCEPT ![identity] = "pending"]
|
|
/\ uploadBodyAvailable' =
|
|
[uploadBodyAvailable EXCEPT ![identity] = FALSE]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
LoseUploadBody(identity) ==
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].request.kind = "put"
|
|
/\ Active(identity)
|
|
/\ externalState[identity] = "idle"
|
|
/\ uploadBodyAvailable[identity]
|
|
/\ uploadBodyAvailable' =
|
|
[uploadBodyAvailable EXCEPT ![identity] = FALSE]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records, externalState,
|
|
postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
SettleLostUpload(identity) ==
|
|
/\ postgresUp
|
|
/\ objectStoreUp
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state = "applying"
|
|
/\ records[identity].request.kind = "put"
|
|
/\ externalState[identity] = "idle"
|
|
/\ ~uploadBodyAvailable[identity]
|
|
/\ externalState' =
|
|
[externalState EXCEPT ![identity] = "settled"]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
uploadBodyAvailable,
|
|
postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
ExternalEffectApplied(identity) ==
|
|
LET request == records[identity].request
|
|
IN /\ objectStoreUp
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state = "applying"
|
|
/\ externalState[identity] = "pending"
|
|
/\ objects' =
|
|
[objects EXCEPT ![request.key] = DesiredObject(request)]
|
|
/\ externalState' =
|
|
[externalState EXCEPT ![identity] = "settled"]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
usedBytes, reservedBytes, keyOwner, records,
|
|
uploadBodyAvailable,
|
|
postgresUp, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
ExternalEffectNotApplied(identity) ==
|
|
/\ objectStoreUp
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state = "applying"
|
|
/\ externalState[identity] = "pending"
|
|
/\ externalState' =
|
|
[externalState EXCEPT ![identity] = "settled"]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
uploadBodyAvailable,
|
|
postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
FinalizeSuccess(identity) ==
|
|
LET record == records[identity]
|
|
request == record.request
|
|
key == request.key
|
|
pool == PoolOf(key)
|
|
priorSize == ObjectSize(record.prior)
|
|
desired == DesiredObject(request)
|
|
desiredSize == ObjectSize(desired)
|
|
growth == Growth(record.prior, desired)
|
|
IN /\ postgresUp
|
|
/\ objectStoreUp
|
|
/\ record # NoRecord
|
|
/\ record.state = "applying"
|
|
/\ externalState[identity] = "settled"
|
|
/\ objects[key] = desired
|
|
/\ records' = [records EXCEPT ![identity].state = "succeeded"]
|
|
/\ usedBytes' =
|
|
[usedBytes EXCEPT ![pool] = (@ - priorSize) + desiredSize]
|
|
/\ reservedBytes' =
|
|
[reservedBytes EXCEPT ![pool] = @ - growth]
|
|
/\ keyOwner' = [keyOwner EXCEPT ![key] = NoOwner]
|
|
/\ externalState' =
|
|
[externalState EXCEPT ![identity] = "idle"]
|
|
/\ uploadBodyAvailable' =
|
|
[uploadBodyAvailable EXCEPT ![identity] = FALSE]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, postgresUp, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
FinalizeFailure(identity) ==
|
|
LET record == records[identity]
|
|
request == record.request
|
|
key == request.key
|
|
pool == PoolOf(key)
|
|
desired == DesiredObject(request)
|
|
growth == Growth(record.prior, desired)
|
|
IN /\ postgresUp
|
|
/\ objectStoreUp
|
|
/\ record # NoRecord
|
|
/\ record.state = "applying"
|
|
/\ externalState[identity] = "settled"
|
|
/\ objects[key] = record.prior
|
|
/\ record.prior # desired
|
|
/\ records' = [records EXCEPT ![identity].state = "failed"]
|
|
/\ reservedBytes' =
|
|
[reservedBytes EXCEPT ![pool] = @ - growth]
|
|
/\ keyOwner' = [keyOwner EXCEPT ![key] = NoOwner]
|
|
/\ externalState' =
|
|
[externalState EXCEPT ![identity] = "idle"]
|
|
/\ uploadBodyAvailable' =
|
|
[uploadBodyAvailable EXCEPT ![identity] = FALSE]
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, postgresUp, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
LosePostgres ==
|
|
/\ postgresUp
|
|
/\ postgresLosses < MaxPostgresLosses
|
|
/\ postgresUp' = FALSE
|
|
/\ postgresLosses' = postgresLosses + 1
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
externalState, uploadBodyAvailable,
|
|
objectStoreUp, objectStoreLosses
|
|
>>
|
|
|
|
RestorePostgres ==
|
|
/\ ~postgresUp
|
|
/\ postgresUp' = TRUE
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
externalState, uploadBodyAvailable, objectStoreUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
LoseObjectStore ==
|
|
/\ objectStoreUp
|
|
/\ objectStoreLosses < MaxObjectStoreLosses
|
|
/\ objectStoreUp' = FALSE
|
|
/\ objectStoreLosses' = objectStoreLosses + 1
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
externalState, uploadBodyAvailable, postgresUp, postgresLosses
|
|
>>
|
|
|
|
RestoreObjectStore ==
|
|
/\ ~objectStoreUp
|
|
/\ objectStoreUp' = TRUE
|
|
/\ observation' = NoObservation
|
|
/\ UNCHANGED <<
|
|
objects, usedBytes, reservedBytes, keyOwner, records,
|
|
externalState, uploadBodyAvailable, postgresUp,
|
|
postgresLosses, objectStoreLosses
|
|
>>
|
|
|
|
ControllerAdvance(identity) ==
|
|
\/ PrepareEffect(identity)
|
|
\/ DispatchEffect(identity)
|
|
\/ LoseUploadBody(identity)
|
|
\/ SettleLostUpload(identity)
|
|
\/ FinalizeSuccess(identity)
|
|
\/ FinalizeFailure(identity)
|
|
|
|
StoreSettlement(identity) ==
|
|
\/ ExternalEffectApplied(identity)
|
|
\/ ExternalEffectNotApplied(identity)
|
|
|
|
Next ==
|
|
\/ \E request \in ValidRequests : FirstRequest(request)
|
|
\/ \E request \in ValidRequests : ReplayRequest(request)
|
|
\/ \E request \in ValidRequests : ConflictRequest(request)
|
|
\/ \E identity \in Identities : ControllerAdvance(identity)
|
|
\/ \E identity \in Identities : StoreSettlement(identity)
|
|
\/ LosePostgres
|
|
\/ RestorePostgres
|
|
\/ LoseObjectStore
|
|
\/ RestoreObjectStore
|
|
|
|
Fairness ==
|
|
/\ WF_vars(RestorePostgres)
|
|
/\ WF_vars(RestoreObjectStore)
|
|
/\ \A identity \in Identities :
|
|
/\ WF_vars(ControllerAdvance(identity))
|
|
/\ WF_vars(StoreSettlement(identity))
|
|
|
|
Spec == Init /\ [][Next]_vars /\ Fairness
|
|
|
|
TypeOK ==
|
|
/\ objects \in [Keys -> ObjectValues]
|
|
/\ usedBytes \in [Pools -> Nat]
|
|
/\ reservedBytes \in [Pools -> Nat]
|
|
/\ keyOwner \in [Keys -> Identities \cup {NoOwner}]
|
|
/\ records \in [Identities -> RecordValues \cup {NoRecord}]
|
|
/\ externalState \in [Identities -> ExternalStates]
|
|
/\ uploadBodyAvailable \in [Identities -> BOOLEAN]
|
|
/\ postgresUp \in BOOLEAN
|
|
/\ objectStoreUp \in BOOLEAN
|
|
/\ postgresLosses \in 0..MaxPostgresLosses
|
|
/\ objectStoreLosses \in 0..MaxObjectStoreLosses
|
|
/\ observation \in Observations \cup {NoObservation}
|
|
|
|
RecordIdentityConsistent ==
|
|
\A identity \in Identities :
|
|
records[identity] # NoRecord =>
|
|
Identity(records[identity].request) = identity
|
|
|
|
PersonalRequestsUseOwnPool ==
|
|
\A request \in ValidRequests :
|
|
request.key \in PersonalKeys =>
|
|
PoolOf(request.key) = request.user
|
|
|
|
PersonalPoolsDisjoint ==
|
|
\A first, second \in Users :
|
|
first # second =>
|
|
PoolKeys(first) \cap PoolKeys(second) = {}
|
|
|
|
FingerprintBindsRequest ==
|
|
\A first, second \in ValidRequests :
|
|
Identity(first) = Identity(second) /\
|
|
RequestFingerprint(first) = RequestFingerprint(second)
|
|
=> first = second
|
|
|
|
ReservationsConsistent ==
|
|
\A pool \in Pools :
|
|
reservedBytes[pool] = ReservationTotal(Identities, pool)
|
|
|
|
LocksConsistent ==
|
|
\A key \in Keys :
|
|
\/ /\ keyOwner[key] = NoOwner
|
|
/\ ~\E identity \in Identities :
|
|
Active(identity) /\
|
|
records[identity].request.key = key
|
|
\/ /\ keyOwner[key] \in Identities
|
|
/\ Active(keyOwner[key])
|
|
/\ records[keyOwner[key]].request.key = key
|
|
/\ \A identity \in Identities :
|
|
Active(identity) /\
|
|
records[identity].request.key = key
|
|
=> identity = keyOwner[key]
|
|
|
|
ActiveObjectConsistent ==
|
|
\A identity \in Identities :
|
|
Active(identity) =>
|
|
LET record == records[identity]
|
|
key == record.request.key
|
|
IN objects[key] \in
|
|
{record.prior, DesiredObject(record.request)}
|
|
|
|
ExternalStateConsistent ==
|
|
\A identity \in Identities :
|
|
/\ (externalState[identity] # "idle" =>
|
|
/\ records[identity] # NoRecord
|
|
/\ records[identity].state = "applying")
|
|
/\ (records[identity] # NoRecord /\
|
|
records[identity].state # "applying" =>
|
|
externalState[identity] = "idle")
|
|
|
|
UploadBodyConsistent ==
|
|
\A identity \in Identities :
|
|
uploadBodyAvailable[identity] =>
|
|
/\ Active(identity)
|
|
/\ records[identity].request.kind = "put"
|
|
/\ externalState[identity] = "idle"
|
|
|
|
QuotaReservationBound ==
|
|
\A pool \in Pools :
|
|
usedBytes[pool] + reservedBytes[pool] <= Limit(pool)
|
|
|
|
ObjectStateCovered ==
|
|
\A pool \in Pools :
|
|
ObjectBytes(objects, PoolKeys(pool)) <=
|
|
usedBytes[pool] + reservedBytes[pool]
|
|
|
|
ObjectQuotaBound ==
|
|
\A pool \in Pools :
|
|
ObjectBytes(objects, PoolKeys(pool)) <= Limit(pool)
|
|
|
|
AccountingAtQuiescence ==
|
|
\A pool \in Pools :
|
|
(~\E identity \in Identities :
|
|
Active(identity) /\
|
|
PoolOf(records[identity].request.key) = pool) =>
|
|
usedBytes[pool] = ObjectBytes(objects, PoolKeys(pool))
|
|
|
|
ObservationConsistent ==
|
|
observation # NoObservation =>
|
|
LET identity == Identity(observation.request)
|
|
record == records[identity]
|
|
IN /\ record # NoRecord
|
|
/\ CASE observation.disposition = "first" ->
|
|
/\ record.request = observation.request
|
|
/\ observation.result = StateResult(record.state)
|
|
[] observation.disposition = "replay" ->
|
|
/\ record.request = observation.request
|
|
/\ observation.result = StateResult(record.state)
|
|
[] observation.disposition = "conflict" ->
|
|
/\ RequestFingerprint(record.request) #
|
|
RequestFingerprint(observation.request)
|
|
/\ observation.result = "conflict"
|
|
|
|
RecordsNeverForgottenAction ==
|
|
\A identity \in Identities :
|
|
records[identity] # NoRecord => records'[identity] # NoRecord
|
|
|
|
RequestBindingsStableAction ==
|
|
\A identity \in Identities :
|
|
records[identity] # NoRecord =>
|
|
records'[identity].request = records[identity].request
|
|
|
|
TerminalRecordsStableAction ==
|
|
\A identity \in Identities :
|
|
Terminal(identity) => records'[identity] = records[identity]
|
|
|
|
PostgresFailureFenceAction ==
|
|
(~postgresUp /\ ~postgresUp') =>
|
|
UNCHANGED <<usedBytes, reservedBytes, keyOwner, records>>
|
|
|
|
ObjectStoreFailureFenceAction ==
|
|
(~objectStoreUp /\ ~objectStoreUp') =>
|
|
UNCHANGED <<objects, externalState>>
|
|
|
|
SettledEffectsDoNotMutateAction ==
|
|
\A identity \in Identities :
|
|
Active(identity) /\ externalState[identity] = "settled" =>
|
|
LET key == records[identity].request.key
|
|
IN objects'[key] = objects[key]
|
|
|
|
RecordsNeverForgotten == [][RecordsNeverForgottenAction]_vars
|
|
RequestBindingsStable == [][RequestBindingsStableAction]_vars
|
|
TerminalRecordsStable == [][TerminalRecordsStableAction]_vars
|
|
PostgresFailureFencesDurableState == [][PostgresFailureFenceAction]_vars
|
|
ObjectStoreFailureFencesObjects == [][ObjectStoreFailureFenceAction]_vars
|
|
SettledEffectsDoNotMutate == [][SettledEffectsDoNotMutateAction]_vars
|
|
|
|
UnfinishedEventuallyTerminal ==
|
|
\A identity \in Identities :
|
|
Active(identity) ~> Terminal(identity)
|
|
|
|
LostUploadEventuallyTerminal ==
|
|
\A identity \in Identities :
|
|
(Active(identity) /\
|
|
records[identity].request.kind = "put" /\
|
|
~uploadBodyAvailable[identity] /\
|
|
externalState[identity] = "idle")
|
|
~> Terminal(identity)
|
|
|
|
=============================================================================
|