--------------------------- MODULE LockOrderModel ---------------------------
(***************************************************************************)
(* Standalone category-2a safety model for DLV-0012: deadlock-freedom via *)
(* a canonical lock-acquisition order. *)
(* *)
(* Kept OUT of the composed subject model (QrustyModel.tla) on purpose: the *)
(* composed model carries no representation of the storage backend's internal *)
(* locks, so there is no existing-variable observable to ground this on, and *)
(* a lock-hierarchy machine would in any case multiply the composed state *)
(* space (the DLV-0021 wall). This machine's variables are disjoint, so *)
(* checking it standalone by direct TLC is sound and instant. *)
(* *)
(* The in-memory backend holds six internal locks, acquired in one fixed *)
(* documented order (DLV-0012): *)
(* 1 data 2 locked_index 3 locked_id_index *)
(* 4 payload_sets 5 queue_configs 6 queue_counters *)
(* "No code path shall acquire a lock at a lower ordinal while holding a *)
(* lock at a higher ordinal." We model concurrent operations as processes *)
(* that each acquire an arbitrary ordered subset of the six locks -- always *)
(* requesting a HIGHER ordinal than any they already hold (the canonical *)
(* discipline) -- then release everything and repeat. This over-approximates *)
(* every real operation (each of which acquires some specific subset in this *)
(* order), so deadlock-freedom here implies it for all of them. *)
(* *)
(* Deadlock-freedom is established two independent ways: *)
(* - TLC's native deadlock check: no reachable state is a total deadlock *)
(* (every process blocked). Restart keeps a finished process live, so the *)
(* only action-free state would be a genuine deadlock. *)
(* - Invariant NoWaitCycle: along every wait-for edge (p waits for a lock *)
(* held by q) the holder's highest-held ordinal strictly exceeds the *)
(* waiter's. maxHeld is thus a ranking function that strictly increases *)
(* around any wait-for path, so no wait-for CYCLE can exist -- ruling out *)
(* partial deadlocks the engine's total-deadlock check would miss. *)
(* Falsifiability: drop the `l > maxHeld[p]` guard in Request (allow grabbing a *)
(* lower lock while holding a higher one) and TLC finds an ABBA deadlock. *)
(***************************************************************************)
EXTENDS Integers
NLocks == 6 \* the six internal locks, by acquisition ordinal
Locks == 1..NLocks
Procs == 0..2 \* concurrent operations (finite for TLC)
NoOwner == -1 \* a lock is free / a process holds none
VARIABLES held, \* held[l] = the process holding lock l, or NoOwner
maxHeld, \* maxHeld[p] = highest lock ordinal p currently holds (0 = none)
req, \* req[p] = lock p is currently trying to acquire, or 0
pstate \* pstate[p] \in {"running","done"}
vars == <<held, maxHeld, req, pstate>>
Init == /\ held = [l \in Locks |-> NoOwner]
/\ maxHeld = [p \in Procs |-> 0]
/\ req = [p \in Procs |-> 0]
/\ pstate = [p \in Procs |-> "running"]
\* a running process decides to acquire its next lock -- always one of a HIGHER
\* ordinal than any it already holds (the canonical order). It does not hold
\* this lock yet (l > maxHeld[p]), so it becomes a pending request.
Request(p, l) == /\ pstate[p] = "running"
/\ req[p] = 0
/\ l > maxHeld[p]
/\ req' = [req EXCEPT ![p] = l]
/\ UNCHANGED <<held, maxHeld, pstate>>
\* the requested lock is free: take it. Because req[p] > maxHeld[p], acquiring
\* it raises p's highest-held ordinal to req[p]. (If the lock is held, p simply
\* stays in its request state -- it is blocked/waiting, modelled as no action.)
Acquire(p) == /\ req[p] # 0
/\ held[req[p]] = NoOwner
/\ held' = [held EXCEPT ![req[p]] = p]
/\ maxHeld' = [maxHeld EXCEPT ![p] = req[p]]
/\ req' = [req EXCEPT ![p] = 0]
/\ UNCHANGED pstate
\* the operation completes: release every lock it holds and finish. (Holding
\* all locks until completion is the conservative case for contention; the
\* acquisition ORDER is what deadlock-freedom turns on.)
Finish(p) == /\ pstate[p] = "running"
/\ req[p] = 0
/\ held' = [l \in Locks |-> IF held[l] = p THEN NoOwner ELSE held[l]]
/\ maxHeld' = [maxHeld EXCEPT ![p] = 0]
/\ pstate' = [pstate EXCEPT ![p] = "done"]
/\ UNCHANGED req
\* a finished operation starts another (keeps the system live so the only
\* action-free state is a real total deadlock).
Restart(p) == /\ pstate[p] = "done"
/\ pstate' = [pstate EXCEPT ![p] = "running"]
/\ UNCHANGED <<held, maxHeld, req>>
Next == \E p \in Procs :
\/ \E l \in Locks : Request(p, l)
\/ Acquire(p)
\/ Finish(p)
\/ Restart(p)
\* Named LockSpec, not Spec: provreq requires exactly one `Spec` in the subject
\* (QrustyModel's), so this standalone spec must not also define `Spec`.
LockSpec == Init /\ [][Next]_vars
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
\* p is waiting for a lock currently held by another process q.
WaitsFor(p, q) == /\ req[p] # 0
/\ held[req[p]] = q
/\ q # p
\* DLV-0012 deadlock-freedom: along every wait-for edge the holder's highest-held
\* ordinal strictly exceeds the waiter's. maxHeld is therefore a ranking function
\* that strictly increases around any chain of waits, so the wait-for graph is
\* acyclic -- no set of processes can be cyclically blocked. This is exactly the
\* classic theorem that totally-ordered lock acquisition cannot deadlock.
NoWaitCycle == \A p \in Procs : \A q \in Procs :
WaitsFor(p, q) => (maxHeld[q] > maxHeld[p])
\* DLV-0012 discipline: no process ever requests a lock at or below the highest
\* ordinal it already holds -- locks are only ever acquired in increasing order.
LockOrderRespected == \A p \in Procs : (req[p] # 0) => (req[p] > maxHeld[p])
\* The full safety obligation for the direct-TLC check (LockOrderModel.cfg),
\* checked alongside TLC's native deadlock detection.
DeadlockFree == NoWaitCycle /\ LockOrderRespected
=============================================================================