---------------------------- MODULE RecheckModel ----------------------------
(***************************************************************************)
(* Standalone category-2a safety model for DLV-0016: the race-safe re-check *)
(* before unlocking an expired lock. *)
(* *)
(* Kept OUT of the composed subject model (QrustyModel.tla) on purpose. *)
(* Modelling the property faithfully needs a PHASE-SEPARATED sub-machine: *)
(* `unlock_expired_messages` collects candidate keys in phase 1, then *)
(* finalizes each one later in phase 2. That temporal gap (and the extra *)
(* variables carrying it) is exactly what multiplies the composed state *)
(* space past tractability -- the same wall DLV-0020 hit. This machine's *)
(* variables are disjoint from the composed Spec, so checking it standalone *)
(* by direct TLC is sound and instant. The composed model still carries the *)
(* safety BACKBONE over existing variables (observable SweepActsOnlyOnExpired *)
(* in QrustyModel.tla): that the finalize step is gated on the lock being *)
(* expired at the moment it acts. This module proves the harder half -- a *)
(* candidate that went STALE between the two phases is never acted upon. *)
(* *)
(* One message's true lock state cycles through: *)
(* lockedExpired -- collected as a candidate because it looks reclaimable *)
(* gone -- a concurrent ack removed it *)
(* lockedFresh -- a concurrent pop re-locked it with a new deadline *)
(* unlocked -- a concurrent force-unlock cleared it *)
(* (gone/lockedFresh/unlocked are the three "stale candidate" cases the code *)
(* `match msg.locked_until { Some(lu) if lu <= now => act, _ => skip }` *)
(* treats identically.) A re-locked message's fresh deadline may pass again *)
(* (lockedFresh -> lockedExpired), so the re-check can act on the CURRENT *)
(* expired lock, never the stale candidate from phase 1. *)
(* *)
(* Phase 1 (RkCollect) is separated in time from an atomic phase-2 re-read + *)
(* guarded act (RkFinalize); the concurrent ops fire in between. rkobs *)
(* records what the re-read OBSERVED and is frozen once finalize runs, so the *)
(* outcome is judged against the state at finalize time -- not one a later *)
(* concurrent op produces. This mirrors `finalize_expired_message`, which *)
(* re-reads the message under the write path and acts only if it is still *)
(* locked with `locked_until <= now`. *)
(***************************************************************************)
VARIABLES rkstate, \* true current lock state the phase-2 re-read observes
rkphase, \* sweeper progress: "idle" | "collected" | "done"
rkout, \* finalize outcome: "none" | "reclaimed" | "skipped"
rkobs \* state the re-read observed, frozen at finalize:
\* "none" | "expired" | "stale"
rvars == <<rkstate, rkphase, rkout, rkobs>>
RkInit == /\ rkstate = "lockedExpired"
/\ rkphase = "idle"
/\ rkout = "none"
/\ rkobs = "none"
\* phase 1: a candidate is collected BECAUSE it currently looks expired.
RkCollect == /\ rkphase = "idle"
/\ rkstate = "lockedExpired"
/\ rkphase' = "collected"
/\ UNCHANGED <<rkstate, rkout, rkobs>>
\* concurrent ack by the holder removes the message after collection.
RkAck == /\ rkstate = "lockedExpired"
/\ rkstate' = "gone"
/\ UNCHANGED <<rkphase, rkout, rkobs>>
\* concurrent pop re-locks the expired message with a fresh deadline
\* (repop-expired): still locked, but NO longer expired -- a stale candidate.
RkRenew == /\ rkstate = "lockedExpired"
/\ rkstate' = "lockedFresh"
/\ UNCHANGED <<rkphase, rkout, rkobs>>
\* concurrent force-unlock clears the lock after collection.
RkForceUnlock == /\ rkstate = "lockedExpired"
/\ rkstate' = "unlocked"
/\ UNCHANGED <<rkphase, rkout, rkobs>>
\* a re-locked message's fresh deadline passes again: it becomes a genuine
\* expired lock once more, so the re-check may act on this CURRENT lock.
RkReExpire == /\ rkstate = "lockedFresh"
/\ rkstate' = "lockedExpired"
/\ UNCHANGED <<rkphase, rkout, rkobs>>
\* phase 2: atomic re-read + guarded act. Reclaim ONLY if the re-read still
\* sees it locked-and-expired; otherwise skip and leave the message untouched.
RkFinalize == /\ rkphase = "collected"
/\ rkphase' = "done"
/\ IF rkstate = "lockedExpired"
THEN /\ rkstate' = "unlocked"
/\ rkout' = "reclaimed"
/\ rkobs' = "expired"
ELSE /\ UNCHANGED rkstate
/\ rkout' = "skipped"
/\ rkobs' = "stale"
\* a finalized sweep is terminal for this candidate.
RkTerminating == rkphase = "done" /\ UNCHANGED rvars
RkNext == \/ RkCollect
\/ RkAck \/ RkRenew \/ RkForceUnlock \/ RkReExpire
\/ RkFinalize
\/ RkTerminating
\* Named RkSpec, not Spec: provreq requires exactly one `Spec` in the subject
\* (QrustyModel's), so this standalone spec must not also define `Spec`.
RkSpec == RkInit /\ [][RkNext]_rvars
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
\* DLV-0016 safety: the reclaimer reclaims a candidate ONLY when its phase-2
\* re-read observed the lock still expired -- never a stale candidate.
ReclaimOnlyWhenExpired == (rkout = "reclaimed") => (rkobs = "expired")
\* DLV-0016 safety: whenever the reclaimer skipped a candidate, its re-read had
\* observed a stale (non-expired) lock, so that candidate is left untouched.
SkipOnlyWhenStale == (rkout = "skipped") => (rkobs = "stale")
\* The full safety obligation for the direct-TLC check (RecheckModel.cfg):
\* the two-phase sweep acts on a candidate only as its re-read classified it,
\* so a candidate that went stale between phase-1 collection and phase-2
\* finalization is never reclaimed.
RecheckSafe == ReclaimOnlyWhenExpired /\ SkipOnlyWhenStale
=============================================================================