------------------------------ MODULE RoostApplyBatch ------------------------------ (***************************************************************************) (* A batch of record writes over several single-writer shards, where a *) (* transaction cannot span shards, and where the server mints every id. *) (* *) (* A batch is a sequence of ops: a create on a shard (the id is not the *) (* client's to choose) or a delete of a pre-existing id on a shard. Some *) (* op may be rejected by validation or a before-trigger; that outcome is a *) (* property of the op, so it is the same on every attempt. *) (* *) (* The design under test runs in four phases: *) (* Plan walk the ops in order, deciding what each would write; the *) (* first rejection ends the batch with nothing written *) (* Claim write the ids the creates will use under the batch's *) (* request key, one row, before anything commits *) (* Commit one transaction per shard, applying all of that shard's ops *) (* Finish audit each committed op *) (* A crash may hit between any two steps; a retry re-runs the same batch *) (* against whatever landed. With the claim kept across the retry the same *) (* ids are used again, so a create that already landed is the same record *) (* and not a second one. The mutant that does not keep the claim *) (* (Claiming = FALSE: fresh ids on every attempt, which is what minting at *) (* commit time without a stored claim amounts to) creates a record twice *) (* when the crash falls after a commit. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Shards, \* the shards a batch may touch Old, \* ids of records that may exist before the batch (deletes name these) Fresh, \* the ids the server may mint N, \* ops per batch Claiming \* TRUE: the claim survives a retry; FALSE: the mutant ASSUME Old \cap Fresh = {} Kinds == {"create", "delete"} Ops == [kind : {"create"}, shard : Shards, id : {"none"}] \cup [kind : {"delete"}, shard : Shards, id : Old] Idx == 1..N Phases == {"plan", "claim", "commit", "finish", "done", "rejected", "crashed"} (* A record: its id and which op created it (0 = it was there before). *) Records == [id : Old \cup Fresh, src : 0..N] VARIABLES ops, \* Idx -> Ops, the batch rejects, \* Idx -> BOOLEAN, which ops validation refuses db0, \* Shards -> SUBSET Old, the ids there before the batch db, \* Shards -> SUBSET Records, the data now dbStart, \* the data when the current attempt started planning claim, \* Idx -> Fresh \cup {"none"}, the ids claimed for the creates phase, i, \* next op to plan committed, \* shards committed in this attempt ever, \* shards committed in any attempt audit \* ops audited vars == <> TypeOK == /\ ops \in [Idx -> Ops] /\ rejects \in [Idx -> BOOLEAN] /\ db0 \in [Shards -> SUBSET Old] /\ db \in [Shards -> SUBSET Records] /\ dbStart \in [Shards -> SUBSET Records] /\ claim \in [Idx -> Fresh \cup {"none"}] /\ phase \in Phases /\ i \in 1..(N + 1) /\ committed \subseteq Shards /\ ever \subseteq Shards /\ audit \subseteq Idx Before(D) == [s \in Shards |-> {[id |-> x, src |-> 0] : x \in D[s]}] Init == /\ ops \in [Idx -> Ops] /\ rejects \in [Idx -> BOOLEAN] /\ db0 \in [Shards -> SUBSET Old] /\ db = Before(db0) /\ dbStart = db /\ claim = [k \in Idx |-> "none"] /\ phase = "plan" /\ i = 1 /\ committed = {} /\ ever = {} /\ audit = {} (* ---------------------------------------------------------------- helpers *) Creates == {k \in Idx : ops[k].kind = "create"} (* The op's effect: a create adds the claimed id (a set, so the same id twice is one record: the plan-time existence check), a delete removes the named id. *) Apply(S, k) == IF ops[k].kind = "create" THEN S \cup {[id |-> claim[k], src |-> k]} ELSE {r \in S : r.id # ops[k].id} (* The content of shard s after ops 1..k are applied in order. *) RECURSIVE ApplyUpTo(_, _, _) ApplyUpTo(S, s, k) == IF k = 0 THEN S ELSE LET P == ApplyUpTo(S, s, k - 1) IN IF ops[k].shard = s THEN Apply(P, k) ELSE P Rejected == \E k \in Idx : rejects[k] UsedIds == UNION {{r.id : r \in db[s]} : s \in Shards} \cup ({claim[k] : k \in Idx} \ {"none"}) Unclaimed == {k \in Creates : claim[k] = "none"} (* ------------------------------------------------------------------ steps *) Plan == /\ phase = "plan" /\ i <= N /\ IF rejects[i] THEN phase' = "rejected" /\ UNCHANGED i ELSE /\ i' = i + 1 /\ phase' = IF i = N THEN "claim" ELSE "plan" /\ UNCHANGED <> (* Fresh, distinct ids for the creates that have none yet; creates that were claimed on an earlier attempt keep theirs. One row, one step. *) Claim == /\ phase = "claim" /\ \E f \in [Unclaimed -> Fresh \ UsedIds] : /\ \A j, k \in Unclaimed : j # k => f[j] # f[k] /\ claim' = [k \in Idx |-> IF k \in Unclaimed THEN f[k] ELSE claim[k]] /\ phase' = "commit" /\ UNCHANGED <> Commit(s) == /\ phase = "commit" /\ s \notin committed /\ db' = [db EXCEPT ![s] = ApplyUpTo(db[s], s, N)] /\ committed' = committed \cup {s} /\ ever' = ever \cup {s} /\ phase' = IF committed' = Shards THEN "finish" ELSE "commit" /\ UNCHANGED <> Finish(k) == /\ phase = "finish" /\ k \notin audit /\ ops[k].shard \in committed /\ audit' = audit \cup {k} /\ phase' = IF audit' = Idx THEN "done" ELSE "finish" /\ UNCHANGED <> Crash == /\ phase \in {"plan", "claim", "commit", "finish"} /\ phase' = "crashed" /\ UNCHANGED <> (* The client retries the whole batch against whatever landed. The claim is a row under the request key: it survives, unless this is the mutant. *) Retry == /\ phase = "crashed" /\ phase' = "plan" /\ i' = 1 /\ committed' = {} /\ dbStart' = db /\ claim' = IF Claiming THEN claim ELSE [k \in Idx |-> "none"] /\ UNCHANGED <> Next == \/ Plan \/ Claim \/ \E s \in Shards : Commit(s) \/ \E k \in Idx : Finish(k) \/ Crash \/ Retry Spec == Init /\ [][Next]_vars (***************************************************************************) (* Invariants *) (***************************************************************************) (* A shard holds either what it had when the attempt started or the whole batch applied: never some of the batch's ops for that shard. *) NoPartialShard == \A s \in Shards : db[s] = dbStart[s] \/ db[s] = ApplyUpTo(dbStart[s], s, N) (* A rejected batch changed nothing. *) RejectedBatchWritesNothing == phase = "rejected" => db = dbStart (* Audit rows exist only for ops whose shard committed. *) AuditOnlyCommitted == \A k \in audit : ops[k].shard \in ever (* No create ever produces two records, whatever the crashes. *) AtMostOnePerCreate == \A k \in Creates : Cardinality({r \in UNION {db[s] : s \in Shards} : r.src = k}) <= 1 (* However many crashes and retries, a batch that completes leaves each shard with the records that were there minus the batch's deletes, plus exactly one record per create on that shard, under its claimed id. *) DeletedOn(s) == {ops[k].id : k \in {k \in Idx : ops[k].kind = "delete" /\ ops[k].shard = s}} Expected(s) == {[id |-> x, src |-> 0] : x \in db0[s] \ DeletedOn(s)} \cup {[id |-> claim[k], src |-> k] : k \in {k \in Creates : ops[k].shard = s}} RetryConverges == phase = "done" => \A s \in Shards : db[s] = Expected(s) =============================================================================