---------------------------- MODULE QrustyModel ------------------------------
(***************************************************************************)
(* The subject-wide category-2a model for Qrusty. *)
(* *)
(* provreq's TLA+ world is single-`Spec` per subject: `verify` runs TLC on *)
(* the one module named `Spec` and checks each requirement's grounded *)
(* observable against it. Independent cat-2a requirements therefore share *)
(* one behaviour, composed here from disjoint sub-machines whose variables *)
(* do not overlap, so each requirement's invariant constrains only its own *)
(* part and stays exactly as valid as it was in isolation. *)
(* *)
(* Sub-machines currently modelled: *)
(* - Scan (PER-0022, #118): the bounded queue-scan loop returns only *)
(* in-range keys and terminates. Variables: store, pos, yielded, done. *)
(* - Count (SYS-0018, #123): the per-queue (available, locked) counter *)
(* cache tracks the true message population under every interleaving of *)
(* operations. Variables: msg, cA, cL. *)
(* - Life (DLV-0008, #125): one message's retry/DLQ lifecycle: bounded *)
(* retries and eventual termination. Variables: lifestate, rc. *)
(* - Atom (DLV-0018, #127): pop() atomicity. Concurrent consumers race *)
(* for one message; the per-queue mutex serialises the check-then-lock *)
(* read-modify-write, so at most one ever holds the lock (DLV-0011). *)
(* Variables: aphase, mutexOwner, msgLocked. *)
(* *)
(* A future cat-2a requirement adds its own disjoint variables, an action *)
(* disjunct in Next, and its observable below — it does not need a second *)
(* `Spec`. *)
(***************************************************************************)
EXTENDS Integers, FiniteSets
(***************************************************************************)
(* Scan sub-machine — PER-0022 (issue #118). *)
(* *)
(* RocksDB stores keys in one total order, modelled as naturals 0..MaxKey. *)
(* A scan for one queue is bounded to the half-open range [Lo, Hi). Store *)
(* contents are nondeterministic (every subset), so the properties hold for *)
(* all possible databases. *)
(***************************************************************************)
MaxKey == 6 \* keyspace is 0..MaxKey (finite, for TLC)
Lo == 2 \* inclusive lower bound = queue_prefix(q)
Hi == 5 \* exclusive upper bound = prefix_upper_bound(prefix), Hi > Lo
\* A key belongs to queue q iff it lies in q's bounded scan range. This is the
\* range/prefix equivalence the category-1 Kani proof establishes; here it is the
\* definition of "this queue's key", and the loop must return only these.
InRange(k) == (k >= Lo) /\ (k < Hi)
(***************************************************************************)
(* Count sub-machine — SYS-0018 (issue #123). *)
(* *)
(* A bounded set of message slots, each in one of *)
(* absent | available | locked | expired *)
(* (expired = lock deadline passed but the unlock-expired sweeper has not *)
(* yet reclaimed it -- still "locked" as far as truth and the cache are *)
(* concerned). cA/cL are the cached counts; each action mirrors exactly *)
(* one row of the SYS-0018 delta table. *)
(***************************************************************************)
Slots == 0..2 \* bounded message population for TLC (finite state space)
MaxRetries == 2 \* configurable per-message retry cap (DLV-0006); small for TLC
(***************************************************************************)
(* Atom sub-machine — DLV-0018 (issue #127), the cat-2a model of DLV-0011. *)
(* *)
(* A bounded set of consumers concurrently pop() one message on the same *)
(* queue. pop() is a read-modify-write: read the message's lock bit, and *)
(* if free, take it. The per-queue async mutex (RocksDB) / exclusive write *)
(* lock (in-memory) makes that RMW a critical section, so only one consumer *)
(* is inside it at a time -- which is the load-bearing fact: without it two *)
(* consumers could both read the bit as free and both take the message. *)
(***************************************************************************)
Consumers == 0..2 \* concurrent pop() callers on one queue (finite for TLC)
NoOwner == -1 \* sentinel: mutex free (kept an integer so TLC never
\* compares across types with a consumer id)
Actors == 0..1 \* consumers in the ownership machine: an owner plus one
\* stale contender is the minimal witness for a foreign-
\* finalize race across lock reassignment (DLV-0019)
VARIABLES store, \* scan: stored keys at scan time (fixed once opened)
pos, \* scan: iterator cursor: least key position still to consider
yielded, \* scan: keys the scan has returned so far
done, \* scan: the loop has finished
msg, \* count: msg[s] \in {"absent","available","locked","expired"}
cA, \* count: cached available count
cL, \* count: cached locked count
lifestate, \* life: "available" | "locked" | "acked" | "dlq"
rc, \* life: retry_count of the message
aphase, \* atom: aphase[c] \in {"idle","incs","holds"}
mutexOwner,\* atom: consumer in the pop critical section, or NoOwner
msgLocked, \* atom: the message's stored lock bit (the RMW target)
owner, \* own: current lock holder (locked_by), or NoOwner
mstate, \* own: "available" | "locked" | "done"
finalizedBy \* own: the actor that acked/nacked the message, or NoOwner
svars == <<store, pos, yielded, done>> \* scan variables
cvars == <<msg, cA, cL>> \* count variables
lvars == <<lifestate, rc>> \* lifecycle variables
avars == <<aphase, mutexOwner, msgLocked>> \* atomicity variables
ovars == <<owner, mstate, finalizedBy>> \* ownership variables
vars == <<store, pos, yielded, done, msg, cA, cL, lifestate, rc,
aphase, mutexOwner, msgLocked, owner, mstate, finalizedBy>>
(***************************************************************************)
(* Init. *)
(***************************************************************************)
ScanInit == /\ store \in SUBSET (0..MaxKey)
/\ pos = Lo
/\ yielded = {}
/\ done = FALSE
CountInit == /\ msg = [s \in Slots |-> "absent"]
/\ cA = 0
/\ cL = 0
LifeInit == /\ lifestate = "available"
/\ rc = 0
AtomInit == /\ aphase = [c \in Consumers |-> "idle"]
/\ mutexOwner = NoOwner
/\ msgLocked = FALSE
OwnInit == /\ owner = NoOwner
/\ mstate = "available"
/\ finalizedBy = NoOwner
Init == ScanInit /\ CountInit /\ LifeInit /\ AtomInit /\ OwnInit
(***************************************************************************)
(* Scan actions (leave count variables unchanged). *)
(***************************************************************************)
\* Stored keys at or after the cursor that the bounded iterator can still see
\* (upper bound Hi is what stops it -- keys >= Hi are never reachable).
Remaining(p) == { k \in store : (k >= p) /\ (k < Hi) }
\* Advance to the next in-range stored key (RocksDB yields ascending) and return it.
ScanStep == /\ ~done
/\ Remaining(pos) # {}
/\ LET k == CHOOSE k \in Remaining(pos) : \A j \in Remaining(pos) : k =< j
IN /\ yielded' = yielded \cup {k}
/\ pos' = k + 1
/\ UNCHANGED <<store, done>>
/\ UNCHANGED cvars
\* No stored key in [pos, Hi): the upper bound is reached, the scan stops.
ScanFinish == /\ ~done
/\ Remaining(pos) = {}
/\ done' = TRUE
/\ UNCHANGED <<store, pos, yielded>>
/\ UNCHANGED cvars
\* Once finished, the scan stutters. Without an explicit terminal step the
\* scan-only terminal state has no scan successor; this keeps the behaviour live.
ScanTerminating == done /\ UNCHANGED vars
ScanNext == ScanStep \/ ScanFinish \/ ScanTerminating
(***************************************************************************)
(* Count actions (leave scan variables unchanged). Each mirrors one row *)
(* of the SYS-0018 delta table. *)
(***************************************************************************)
\* push: absent -> available, available += 1
Push(s) == /\ msg[s] = "absent"
/\ msg' = [msg EXCEPT ![s] = "available"]
/\ cA' = cA + 1
/\ cL' = cL
/\ UNCHANGED svars
\* pop (fresh): available -> locked, available -= 1, locked += 1
PopFresh(s) == /\ msg[s] = "available"
/\ msg' = [msg EXCEPT ![s] = "locked"]
/\ cA' = cA - 1
/\ cL' = cL + 1
/\ UNCHANGED svars
\* lock deadline passes: locked -> expired, no counter change (still locked)
Expire(s) == /\ msg[s] = "locked"
/\ msg' = [msg EXCEPT ![s] = "expired"]
/\ cA' = cA
/\ cL' = cL
/\ UNCHANGED svars
\* pop (re-pop expired): expired -> locked, NO counter change. The slot is
\* already counted as locked; the new lock just replaces the expired one.
\* This is the SYS-0018 guard whose omission causes counter drift.
PopRepopExpired(s) == /\ msg[s] = "expired"
/\ msg' = [msg EXCEPT ![s] = "locked"]
/\ cA' = cA
/\ cL' = cL
/\ UNCHANGED svars
\* ack: locked -> absent, locked -= 1
Ack(s) == /\ msg[s] = "locked"
/\ msg' = [msg EXCEPT ![s] = "absent"]
/\ cA' = cA
/\ cL' = cL - 1
/\ UNCHANGED svars
\* nack (retry): locked -> available, locked -= 1, available += 1
NackRetry(s) == /\ msg[s] = "locked"
/\ msg' = [msg EXCEPT ![s] = "available"]
/\ cA' = cA + 1
/\ cL' = cL - 1
/\ UNCHANGED svars
\* nack (DLQ / drop): locked -> absent, locked -= 1
NackDlq(s) == /\ msg[s] = "locked"
/\ msg' = [msg EXCEPT ![s] = "absent"]
/\ cA' = cA
/\ cL' = cL - 1
/\ UNCHANGED svars
\* unlock_expired sweep: expired -> available, locked -= 1, available += 1
UnlockExpired(s) == /\ msg[s] = "expired"
/\ msg' = [msg EXCEPT ![s] = "available"]
/\ cA' = cA + 1
/\ cL' = cL - 1
/\ UNCHANGED svars
CountNext == \E s \in Slots :
\/ Push(s)
\/ PopFresh(s)
\/ Expire(s)
\/ PopRepopExpired(s)
\/ Ack(s)
\/ NackRetry(s)
\/ NackDlq(s)
\/ UnlockExpired(s)
(***************************************************************************)
(* Composed behaviour. Weak fairness on the scan's productive actions only *)
(* (as in the original PER-0022 model) so the scan runs to completion; the *)
(* counter machine needs no fairness (its obligation is pure safety). *)
(***************************************************************************)
(***************************************************************************)
(* Lifecycle sub-machine — DLV-0008 (issue #125), spanning DLV-0002/0006/ *)
(* 0007/0015. One message's fate: consume locks it and increments its *)
(* retry_count (DLV-0002); ack ends it; a nack or lock-expiry redelivers it *)
(* while retry_count < max (DLV-0007) or dead-letters it once retry_count *)
(* reaches max (DLV-0008 nack / DLV-0015 expiry). acked and dlq are *)
(* terminal. These actions touch only lvars; framing is at Next. *)
(***************************************************************************)
\* Names are Life-prefixed: the counter machine already defines Ack/NackRetry/
\* NackDlq (over slots), and TLA+ forbids reusing an operator name.
\* consume: available -> locked, retry_count++ (DLV-0002)
LifeConsume == /\ lifestate = "available"
/\ lifestate' = "locked"
/\ rc' = rc + 1
\* ack: the lock holder acks -> terminal
LifeAck == /\ lifestate = "locked"
/\ lifestate' = "acked"
/\ rc' = rc
\* nack under the cap: locked -> available for redelivery (DLV-0007)
LifeNackRetry == /\ lifestate = "locked"
/\ rc < MaxRetries
/\ lifestate' = "available"
/\ rc' = rc
\* nack at or over the cap: locked -> DLQ (DLV-0008)
LifeNackDlq == /\ lifestate = "locked"
/\ rc >= MaxRetries
/\ lifestate' = "dlq"
/\ rc' = rc
\* lock expiry under the cap: locked -> available for redelivery (DLV-0005/0007)
LifeExpireRetry == /\ lifestate = "locked"
/\ rc < MaxRetries
/\ lifestate' = "available"
/\ rc' = rc
\* lock expiry at or over the cap: locked -> DLQ (DLV-0015)
LifeExpireDlq == /\ lifestate = "locked"
/\ rc >= MaxRetries
/\ lifestate' = "dlq"
/\ rc' = rc
\* Terminal stutter so a terminated message's state has a successor.
LifeTerminating == lifestate \in {"acked", "dlq"} /\ UNCHANGED lvars
\* Progress actions (everything that advances the message; not ack, not the
\* terminal stutter). Under weak fairness these force the message toward a
\* terminal state (retry_count strictly increases on each consume and is capped,
\* so redelivery cannot recur forever -- it must reach the DLQ); that fairness
\* and the resulting liveness are checked over specs/LifecycleModel.tla, since
\* this composed Spec carries no fairness.
LifeStep == LifeConsume \/ LifeNackRetry \/ LifeNackDlq \/ LifeExpireRetry \/ LifeExpireDlq
LifeNext == LifeStep \/ LifeAck \/ LifeTerminating
(***************************************************************************)
(* Atom actions (DLV-0018). A consumer that decides to pop() acquires the *)
(* per-queue mutex when it is free, and inside the critical section does the *)
(* check-then-lock: if the message is free it takes it (becomes the holder) *)
(* and releases the mutex; if already locked it leaves empty-handed. The *)
(* holder later acks/nacks, clearing the lock. (The pre-acquire "waiting" *)
(* moment is abstracted away -- it does not bear on mutual exclusion.) These *)
(* actions touch only avars; framing is at Next. *)
(***************************************************************************)
\* a consumer decides to pop() and acquires the per-queue mutex -- only when
\* no other consumer holds it (this is the serialisation the property rests on)
AtomEnter(c) == /\ aphase[c] = "idle"
/\ mutexOwner = NoOwner
/\ mutexOwner' = c
/\ aphase' = [aphase EXCEPT ![c] = "incs"]
/\ UNCHANGED msgLocked
\* inside the critical section, message free: lock it, become holder, release mutex
AtomWin(c) == /\ aphase[c] = "incs"
/\ mutexOwner = c
/\ msgLocked = FALSE
/\ msgLocked' = TRUE
/\ mutexOwner' = NoOwner
/\ aphase' = [aphase EXCEPT ![c] = "holds"]
\* inside the critical section, message already locked: release mutex empty-handed
AtomLose(c) == /\ aphase[c] = "incs"
/\ mutexOwner = c
/\ msgLocked = TRUE
/\ mutexOwner' = NoOwner
/\ aphase' = [aphase EXCEPT ![c] = "idle"]
/\ UNCHANGED msgLocked
\* the holder acks/nacks: clear the lock and become ready to pop again
AtomFinish(c) == /\ aphase[c] = "holds"
/\ msgLocked' = FALSE
/\ aphase' = [aphase EXCEPT ![c] = "idle"]
/\ UNCHANGED mutexOwner
AtomNext == \E c \in Consumers :
\/ AtomEnter(c)
\/ AtomWin(c)
\/ AtomLose(c)
\/ AtomFinish(c)
(***************************************************************************)
(* Own actions — DLV-0019 (issue #128), the cat-2a model of DLV-0003/0004. *)
(* *)
(* A message records its lock holder in `owner` (the code's locked_by). A *)
(* consumer locks it when free; its lock may expire and be reassigned to *)
(* another consumer, leaving the first a STALE holder. ack/nack (modelled *)
(* as one `finalize`) is guarded by CURRENT ownership (owner = c), exactly *)
(* as storage.rs checks `msg.locked_by.as_deref() == Some(consumer_id)`, so *)
(* a stale holder can never finalise a message now owned by someone else. *)
(* These actions touch only ovars; framing is at Next. *)
(***************************************************************************)
\* a consumer acquires the free lock (pop): available -> locked, owner := c
OwnLock(c) == /\ mstate = "available"
/\ owner = NoOwner
/\ owner' = c
/\ mstate' = "locked"
/\ UNCHANGED finalizedBy
\* the lock deadline passes: the message becomes reclaimable and its owner is
\* cleared -- the previous holder is now stale (owner # it), so its later
\* finalise attempt fails the ownership guard below.
OwnExpire == /\ mstate = "locked"
/\ owner' = NoOwner
/\ mstate' = "available"
/\ UNCHANGED finalizedBy
\* ack/nack: ONLY the current owner may finalise (DLV-0003 ack / DLV-0004 nack)
OwnFinalize(c) == /\ mstate = "locked"
/\ owner = c
/\ mstate' = "done"
/\ owner' = NoOwner
/\ finalizedBy' = c
\* a finalised message is terminal
OwnTerminating == mstate = "done" /\ UNCHANGED ovars
OwnNext == \/ (\E c \in Actors : OwnLock(c) \/ OwnFinalize(c))
\/ OwnExpire
\/ OwnTerminating
(***************************************************************************)
(* Composed behaviour. Each sub-machine touches only its own variables; *)
(* the frame (UNCHANGED of the other machines' variables) is applied here, *)
(* so adding a machine is: its vars + its actions + one Next disjunct. *)
(***************************************************************************)
Next == \/ (ScanNext /\ UNCHANGED <<cvars, lvars, avars, ovars>>)
\/ (CountNext /\ UNCHANGED <<svars, lvars, avars, ovars>>)
\/ (LifeNext /\ UNCHANGED <<svars, cvars, avars, ovars>>)
\/ (AtomNext /\ UNCHANGED <<svars, cvars, lvars, ovars>>)
\/ (OwnNext /\ UNCHANGED <<svars, cvars, lvars, avars>>)
\* The composed subject spec is a PURE SAFETY model: no weak-fairness clauses.
\* Liveness (`leads_to`) over this composed Spec is intractable at the current
\* machine count -- its `holds` verdict could not be reproduced (re-verify timed
\* out), the stale-verdict gap from !140. The two liveness obligations therefore
\* live in standalone modules checked by direct TLC, each over its own machine
\* with its own fairness, where they are fast, reproducible, and falsifiable:
\* - scan termination (PER-0022) -> specs/ScanLivenessModel.tla
\* - lifecycle termination (DLV-0017) -> specs/LifecycleModel.tla
\* Dropping fairness here is safety-preserving: weak fairness constrains only
\* infinite suffixes, never the reachable-state set, so every `always` observable
\* grounded on this Spec keeps exactly the verdict it had -- and now verifies
\* faster, with no liveness tableau.
Spec == Init /\ [][Next]_vars
(***************************************************************************)
(* Grounded definitions. *)
(***************************************************************************)
\* PER-0022 safety: every key the scan returned is in this queue's range. (The
\* termination half -- scan_active leads_to scan_done -- is checked standalone by
\* direct TLC over specs/ScanLivenessModel.tla, not over this composed Spec.)
ScanYieldsOnlyInRange == \A k \in yielded : InRange(k)
\* SYS-0018 true population the cache must mirror. Expired slots are still
\* locked in truth until the sweeper reclaims them.
TrueAvail == Cardinality({s \in Slots : msg[s] = "available"})
TrueLocked == Cardinality({s \in Slots : msg[s] \in {"locked", "expired"}})
\* SYS-0018 safety: cached counts equal the true population -- no drift.
CountersMatchPopulation == (cA = TrueAvail) /\ (cL = TrueLocked)
\* SYS-0018 safety: cached counts never go negative under any interleaving.
CountersNonNegative == (cA >= 0) /\ (cL >= 0)
\* DLV-0005/0013 safety: the unlock-expired sweep is unconditionally available
\* on any expired lock. UnlockExpired(s) is guarded by `msg[s] = "expired"`
\* ALONE -- the stored `locked_until` deadline -- and never by any in-memory
\* index, so recovery can never be BLOCKED for an expired lock (in particular a
\* post-restart stranded lock absent from locked_index is still reclaimable).
\* This is the safety backbone of recovery; that the sweep eventually FIRES
\* (liveness) is model-checked separately over RecoveryModel.tla by direct TLC,
\* since liveness over the composed Spec is intractable.
SweepAlwaysEnabledForExpired ==
\A s \in Slots : (msg[s] = "expired") => ENABLED UnlockExpired(s)
\* DLV-0008 safety: retry_count never exceeds the configured cap -- a message
\* is never delivered more than MaxRetries times before dead-lettering. (The
\* liveness half -- message_active leads_to message_terminal -- is checked
\* standalone by direct TLC over specs/LifecycleModel.tla, not over this Spec.)
RetriesBounded == rc <= MaxRetries
\* DLV-0018 / DLV-0011 safety: the message is delivered to at most one consumer
\* at a time -- no concurrent pop() ever double-locks it. This is the property
\* the per-queue mutex exists to guarantee.
AtMostOneHolder == Cardinality({c \in Consumers : aphase[c] = "holds"}) <= 1
\* DLV-0018 coherence: the stored lock bit is set exactly while some consumer
\* holds the message -- the lock and the delivery never disagree.
LockMatchesHolder == msgLocked <=> (\E c \in Consumers : aphase[c] = "holds")
\* DLV-0019 / DLV-0003+DLV-0004 safety: a message is finalised (acked/nacked)
\* only ever by an actor -- and, because OwnFinalize is guarded by owner = c,
\* only by the actor that currently owns the lock. A stale holder whose lock
\* expired and was reassigned can never finalise: reaching "done" is possible
\* only through the current owner.
FinalizedOnlyByOwner == (mstate = "done") => (finalizedBy \in Actors)
\* DLV-0019 coherence: the message has a current lock owner exactly while it is
\* locked (available/done carry no owner) -- ownership and lock state agree.
OwnerMatchesLock == (mstate = "locked") <=> (owner \in Actors)
\* DLV-0016 safety backbone: the unlock-expired sweep reclaims a slot ONLY when
\* that slot is currently expired. UnlockExpired(s) is guarded by
\* `msg[s] = "expired"`, so the reclaiming transition (and its counter delta) can
\* never fire against an available/locked/absent slot -- reclamation acts only on
\* a genuinely-expired lock. This is the composed-model half of the race-safe
\* re-check: that the FINALIZE step is gated on the lock being expired at the
\* moment it acts. The other half -- that a two-phase sweep, which collects
\* candidates in phase 1 and finalizes them later, never acts on a candidate that
\* went STALE (acked, re-locked, or unlocked) between the phases -- is model-
\* checked by direct TLC over the standalone specs/RecheckModel.tla, because that
\* race needs a phase-separated sub-machine whose extra variables would multiply
\* the composed state space past tractability.
SweepActsOnlyOnExpired ==
\A s \in Slots : ENABLED UnlockExpired(s) => (msg[s] = "expired")
=============================================================================