---------------------------- MODULE InitGateModel ---------------------------
(***************************************************************************)
(* Standalone category-2a safety model for SYS-0024: the startup gate. *)
(* *)
(* While the server is initialising (the `initializing` flag is set), every *)
(* mutating operation is rejected with 503; only once initialisation is *)
(* complete and the flag is cleared are mutations admitted. The safety *)
(* property is that NO mutation is ever applied to storage while the cache is *)
(* still being rebuilt -- a request that arrives mid-initialisation cannot *)
(* race the rebuild and corrupt counters/indexes; it is either rejected (503) *)
(* or, if it is still pending when initialisation finishes, admitted only *)
(* afterwards. *)
(* *)
(* Kept OUT of the composed subject model (QrustyModel.tla): the composed *)
(* model has no initialisation phase, so there is no existing-variable *)
(* observable to ground this on. Disjoint variables, so direct TLC is sound *)
(* and instant. *)
(* *)
(* `ready` is the cleared-flag (initialisation complete); it is ONE-WAY *)
(* (FALSE -> TRUE, never back), mirroring the flag set once at startup and *)
(* cleared once the rebuild finishes. A mutation request `pending` may arrive *)
(* at any time, including during initialisation; the gate (GateAdmit, guarded *)
(* by `ready`) is the startup_gate middleware. `everApplied` records that a *)
(* mutation was ever applied to storage -- the quantity the invariant ties to *)
(* `ready`. *)
(***************************************************************************)
EXTENDS Integers
VARIABLES ready, \* initialisation complete + flag cleared (one-way)
pending, \* a mutation request is in flight, awaiting the gate
everApplied \* some mutation has been applied to storage
vars == <<ready, pending, everApplied>>
Init == /\ ready = FALSE
/\ pending = FALSE
/\ everApplied = FALSE
\* a mutation request arrives -- at any time, including mid-initialisation.
Arrive == /\ ~pending
/\ pending' = TRUE
/\ UNCHANGED <<ready, everApplied>>
\* the cache rebuild finishes and the initializing flag is cleared. One-way:
\* `ready` never returns to FALSE.
InitComplete == /\ ~ready
/\ ready' = TRUE
/\ UNCHANGED <<pending, everApplied>>
\* the startup gate admits a pending mutation -- ONLY when initialisation is
\* complete (ready). Applying it marks storage as mutated.
GateAdmit == /\ pending
/\ ready
/\ everApplied' = TRUE
/\ pending' = FALSE
/\ UNCHANGED ready
\* the startup gate rejects a pending mutation with 503 while still
\* initialising: the request is dropped, storage is untouched.
GateReject == /\ pending
/\ ~ready
/\ pending' = FALSE
/\ UNCHANGED <<ready, everApplied>>
Next == Arrive \/ InitComplete \/ GateAdmit \/ GateReject
\* Named GateSpec, not Spec: provreq requires exactly one `Spec` in the subject
\* (QrustyModel's), so this standalone spec must not also define `Spec`.
GateSpec == Init /\ [][Next]_vars
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
\* SYS-0024 safety: a mutation is applied only after initialisation is complete.
\* Because `ready` is one-way and GateAdmit is guarded by it, `everApplied` can
\* become TRUE only once `ready` is already TRUE and stays TRUE -- so no mutation
\* is ever applied while the server is still initialising, however a request
\* interleaves with the completion of the rebuild.
MutationsGatedByInit == everApplied => ready
=============================================================================