--------------------------- MODULE CompactionModel --------------------------
(***************************************************************************)
(* Standalone category-2a safety model for PER-0020: payload compaction *)
(* invalidates the hot tier so a stale payload_ref is never served. *)
(* *)
(* Kept OUT of the composed subject model (QrustyModel.tla): the composed *)
(* model has no payload-segment / compaction representation, so there is no *)
(* existing-variable observable to ground this on. Disjoint variables, so *)
(* direct TLC is sound and instant. *)
(* *)
(* compact_payloads() is three-phase (storage.rs): *)
(* phase 1 write live payloads into a new compacted segment (sources are *)
(* NOT deleted yet -- every existing ref still resolves); *)
(* phase 2 rewrite each message's payload_ref to the new segment in *)
(* RocksDB and durably flush; *)
(* PER-0020 CLEAR the hot tiers, so cached messages stop carrying the old *)
(* ref (the tier refills from RocksDB, which now has new refs); *)
(* phase 3 delete the sealed source segments. *)
(* The load-bearing ordering is clear-before-delete: the old segment is *)
(* unlinked only AFTER the refs are rewritten AND the hot tier is cleared, so *)
(* nothing servable still points at a segment about to vanish. Without the *)
(* clear, a cached message would reference a now-deleted segment -- the *)
(* "segment file missing" stale read PER-0020 prevents. *)
(* *)
(* `oldSeg` is the source segment (live | deleted); `refsRewritten` is phase *)
(* 2; `hotStale` is TRUE while the hot tier still holds a pre-compaction entry *)
(* carrying the OLD ref; `served` records the outcome of the most recent pop. *)
(***************************************************************************)
EXTENDS Integers
VARIABLES oldSeg, \* "live" | "deleted": the sealed source segment
refsRewritten, \* RocksDB payload_refs now point at the new segment
hotStale, \* hot tier holds a pre-compaction entry with the OLD ref
served \* "none" | "ok" | "stale": last pop's resolution
vars == <<oldSeg, refsRewritten, hotStale, served>>
\* Initially a message cached in the hot tier before compaction carries the old
\* ref; the source segment is live and refs are not yet rewritten.
Init == /\ oldSeg = "live"
/\ refsRewritten = FALSE
/\ hotStale = TRUE
/\ served = "none"
\* phase 2: rewrite payload_refs in RocksDB to the new compacted segment.
RewriteRefs == /\ ~refsRewritten
/\ refsRewritten' = TRUE
/\ UNCHANGED <<oldSeg, hotStale, served>>
\* PER-0020: clear the hot tier, so it no longer serves the old ref (it will
\* refill from RocksDB, which carries the rewritten refs).
ClearHot == /\ hotStale' = FALSE
/\ UNCHANGED <<oldSeg, refsRewritten, served>>
\* phase 3: unlink the sealed source segment -- ONLY after the refs are rewritten
\* AND the hot tier has been cleared (the clear-before-delete ordering). This is
\* the guard whose omission is exactly the bug PER-0020 fixes.
DeleteOld == /\ oldSeg = "live"
/\ refsRewritten
/\ ~hotStale
/\ oldSeg' = "deleted"
/\ UNCHANGED <<refsRewritten, hotStale, served>>
\* a pop served from the hot tier's pre-compaction entry: it carries the old ref,
\* which resolves fine while the source segment is live but is STALE (points at a
\* deleted segment) once the source has been unlinked.
PopHotStale == /\ hotStale
/\ served' = (IF oldSeg = "deleted" THEN "stale" ELSE "ok")
/\ UNCHANGED <<oldSeg, refsRewritten, hotStale>>
\* a pop served from RocksDB (or a post-clear refill): it uses the current ref,
\* which always points at a live segment under the compaction ordering.
PopFresh == /\ served' = "ok"
/\ UNCHANGED <<oldSeg, refsRewritten, hotStale>>
Next == RewriteRefs \/ ClearHot \/ DeleteOld \/ PopHotStale \/ PopFresh
\* Named CompactSpec, not Spec: provreq requires exactly one `Spec` in the subject
\* (QrustyModel's), so this standalone spec must not also define `Spec`.
CompactSpec == Init /\ [][Next]_vars
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
\* PER-0020 safety: a pop never serves a message whose payload_ref points at a
\* deleted segment. Because DeleteOld is guarded by ~hotStale (the hot tier is
\* cleared before the source is unlinked) and nothing re-staleifies the tier, a
\* hot-tier entry carrying the old ref can be served only while its segment is
\* still live -- so the "stale" outcome is unreachable.
NeverServesStale == served # "stale"
=============================================================================