----------------------------- 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) == <> 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) == <> 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 <> ObjectStoreFailureFenceAction == (~objectStoreUp /\ ~objectStoreUp') => UNCHANGED <> 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) =============================================================================