--------------------------- MODULE RecoveryModel ----------------------------
(***************************************************************************)
(* Standalone category-2a liveness model for DLV-0005 / DLV-0013: *)
(* lock-expiry recovery. *)
(* *)
(* Kept OUT of the composed subject model (QrustyModel.tla) on purpose. *)
(* This property is a liveness obligation (`leads_to`), and liveness *)
(* model-checking cost grows with the whole composed state space. The *)
(* recovery property, however, is over this machine's variables ALONE -- *)
(* the other sub-machines are disjoint and can neither enable nor disable *)
(* RecSweep -- so composing them in would only multiply the state space *)
(* without changing the property's truth (and would, in practice, push *)
(* every liveness `verify` on the subject past tractability). It therefore *)
(* lives in its own module with its own `Spec`, checked by TLC directly. *)
(* *)
(* A single message's lock cycles available -> locked -> expired -> *)
(* available. `rindexed` records whether the lock is tracked by the *)
(* in-memory locked_index. A lock may be taken WITHOUT being indexed -- *)
(* the post-restart stranded case (DLV-0013): after startup queue_counters *)
(* is seeded from a full RocksDB scan but locked_index starts empty, so a *)
(* genuinely-locked message is untracked in memory. The unlock-expired *)
(* sweeper (`unlock_expired_messages`) reclaims an expired lock by its *)
(* stored `locked_until` deadline via a scan, so RecSweep is guarded by *)
(* expiry ALONE and never by `rindexed` -- that independence is what lets a *)
(* stranded lock still be recovered (DLV-0013). Weak fairness on RecSweep *)
(* makes recovery a liveness guarantee: an expired lock is ALWAYS EVENTUALLY *)
(* made available again (DLV-0005), so it can never stay counted-locked *)
(* forever. *)
(***************************************************************************)
VARIABLES rstate, \* "available" | "locked" | "expired"
rindexed \* whether the lock is tracked in the in-memory index
rvars == <<rstate, rindexed>>
RecInit == /\ rstate = "available"
/\ rindexed = FALSE
\* a consumer takes the lock (pop). The lock may or may not be indexed: an
\* un-indexed lock is the post-restart stranded case (DLV-0013).
RecLock == /\ rstate = "available"
/\ rstate' = "locked"
/\ rindexed' \in {TRUE, FALSE}
\* the lock deadline passes: the message is now reclaimable but not yet swept.
RecExpire == /\ rstate = "locked"
/\ rstate' = "expired"
/\ UNCHANGED rindexed
\* unlock_expired sweep: an expired lock is reclaimed and becomes available
\* again. Guarded by expiry ONLY -- never by rindexed -- so a stranded
\* (un-indexed) lock is recovered exactly as a tracked one is.
RecSweep == /\ rstate = "expired"
/\ rstate' = "available"
/\ rindexed' = FALSE
RecNext == RecLock \/ RecExpire \/ RecSweep
\* Weak fairness on RecSweep: while a lock is expired, RecSweep stays enabled
\* (only RecSweep leaves the "expired" state), so it must eventually fire.
\* Named RecSpec, not Spec: provreq requires exactly one `Spec` in the subject
\* (that is QrustyModel's), so this standalone spec must not also define `Spec`.
RecSpec == RecInit /\ [][RecNext]_rvars /\ WF_rvars(RecSweep)
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
\* DLV-0005/0013 liveness: an expired lock is always eventually reclaimed and
\* made available again. Because RecSweep is guarded by expiry alone (never
\* by rindexed), this holds equally for stranded, un-indexed locks (DLV-0013).
RecExpired == rstate = "expired"
RecAvailable == rstate = "available"
\* The liveness obligation itself, for the direct-TLC check (RecoveryModel.cfg):
\* an expired lock is always eventually reclaimed. Checked here rather than via
\* provreq because provreq runs the one composed subject Spec (QrustyModel), over
\* which liveness model-checking is intractable; this machine's variables are
\* disjoint from that Spec, so checking it standalone is sound and instant.
RecRecovers == RecExpired ~> RecAvailable
=============================================================================