Quicksort.tla

-------------------------- MODULE Quicksort --------------------------
(***************************************************************************)
(* Models a SET of fixed-size arrays with explicit per-cell                  *)
(* initialization tracking, then runs an iterative Lomuto quicksort over    *)
(* one designated TargetArray. Four worker processes each own a STATIC,     *)
(* disjoint slice of the array and sort that slice independently.           *)
(*                                                                           *)
(* Properties verified by TLC:                                              *)
(*   TypeOK             -- state shape                                       *)
(*   InitMonotonic      -- inited flags never go FALSE once TRUE             *)
(*   Sortedness         -- on AllDone, every slice is sorted                 *)
(*   Termination        -- []<>(every worker reaches Done)                   *)
(*   (deadlock-freedom)  -- TLC's built-in deadlock check                    *)
(*                                                                           *)
(* Two ADDITIONAL safety properties are enforced by TLC!Assert at every     *)
(* read or write site:                                                       *)
(*   NoUninitRead       -- every cell read is preceded by inited=TRUE        *)
(*   OwnsCell(self,i)   -- every cell access stays inside the worker's slice *)
(*                         => no two workers ever conflict                   *)
(* If a buggy variant is enabled, TLC aborts with the named Assert message  *)
(* and a counterexample trace.                                              *)
(***************************************************************************)
EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
  ArrayNames,    \* Set of array identifiers (the SET of arrays).
  ArraySize,     \* Cells per array (Nat, divisible by NumWorkers).
  NumWorkers,    \* Number of workers (= 4 in the default config).
  MaxValue,      \* Cell values are drawn from 0..MaxValue.
  TargetArray,   \* Which array the workers are sorting.
  UNDEF          \* Sentinel value for "uninitialized memory".

ASSUME NumWorkersPos    == NumWorkers \in Nat \ {0}
ASSUME ArraySizeOK      == ArraySize  \in Nat \ {0}
ASSUME ChunkClean       == ArraySize % NumWorkers = 0
ASSUME TargetArrayInSet == TargetArray \in ArrayNames
ASSUME MaxValueOK       == MaxValue \in Nat
ASSUME UndefDistinct    == UNDEF \notin (0..MaxValue)

----------------------------------------------------------------------------
(* Static structure of the partition. *)

Workers   == 1..NumWorkers
ChunkSize == ArraySize \div NumWorkers
MinIdx(w) == ChunkSize * (w - 1) + 1
MaxIdx(w) == ChunkSize * w
ProcRange(w) == MinIdx(w)..MaxIdx(w)

Indices == 1..ArraySize
Values  == 0..MaxValue

(* Strengthened: a cell is owned by w iff it is in w's range AND no other  *)
(* worker also claims it. Catches misconfigured (overlapping) slices       *)
(* immediately at the first read or write Assert.                          *)
OwnsCell(w, i) ==
  /\ i \in ProcRange(w)
  /\ \A q \in Workers \ {w} : i \notin ProcRange(q)

DisjointOwnership ==
  \A p, q \in Workers : p /= q => ProcRange(p) \cap ProcRange(q) = {}

(* THEOREM is informative; ASSUME forces TLC to evaluate the predicate at *)
(* startup so a misconfigured slice setup fails before any state is       *)
(* explored.                                                              *)
THEOREM DisjointPartition == DisjointOwnership
ASSUME DisjointPartitionCheck == DisjointOwnership

----------------------------------------------------------------------------
(* State variables.                                                         *)

VARIABLES
  arr,          \* [ArrayNames -> [Indices -> Values \cup {UNDEF}]]
  inited,       \* [ArrayNames -> [Indices -> BOOLEAN]]
  ctrl,         \* [Workers -> {"Init","Pop","ReadPivot","PartStep",
                \*              "PartFinal","Done"}]
  stack,        \* [Workers -> Seq([lo: Int, hi: Int])]
  lo, hi,       \* [Workers -> Int]   current interval bounds
  pivot,        \* [Workers -> Values \cup {UNDEF}]
  idxI, idxJ,   \* [Workers -> Int]   Lomuto cursors
  sliceInit     \* [Workers -> [Indices -> Values \cup {UNDEF}]]
                \* ghost: snapshot of TargetArray taken at FinishInit, used by
                \* the data-preservation invariant.

vars == <<arr, inited, ctrl, stack, lo, hi, pivot, idxI, idxJ, sliceInit>>

----------------------------------------------------------------------------
(* Type invariant. Index/cursor bounds are loose enough to admit terminal   *)
(* values such as idxI = lo - 1 and idxJ = hi just before PartExit.         *)

States   == {"Init", "Pop", "ReadPivot", "PartStep", "PartFinal", "Done"}
Cells    == [Indices -> Values \cup {UNDEF}]
InitMap  == [Indices -> BOOLEAN]
IntervalSet == [lo : 0..(ArraySize+1), hi : 0..(ArraySize+1)]

(* Tight bounds on cursor variables. Pushed-interval entries can hold      *)
(* idxI+2 = ArraySize+1 (vacuous interval, discarded by PopInterval), so   *)
(* IntervalSet remains 0..ArraySize+1; but lo[w], hi[w], idxI, idxJ are    *)
(* never assigned out of 0..ArraySize.                                     *)
TypeOK ==
  /\ arr       \in [ArrayNames -> Cells]
  /\ inited    \in [ArrayNames -> InitMap]
  /\ ctrl      \in [Workers    -> States]
  /\ stack     \in [Workers    -> Seq(IntervalSet)]
  /\ lo        \in [Workers    -> 0..ArraySize]
  /\ hi        \in [Workers    -> 0..ArraySize]
  /\ pivot     \in [Workers    -> Values \cup {UNDEF}]
  /\ idxI      \in [Workers    -> 0..ArraySize]
  /\ idxJ      \in [Workers    -> 0..ArraySize]
  /\ sliceInit \in [Workers    -> [Indices -> Values \cup {UNDEF}]]

----------------------------------------------------------------------------
(* Initial state: every cell of every array is UNDEF and uninited.          *)

Init ==
  /\ arr       = [a \in ArrayNames |-> [i \in Indices |-> UNDEF]]
  /\ inited    = [a \in ArrayNames |-> [i \in Indices |-> FALSE]]
  /\ ctrl      = [w \in Workers    |-> "Init"]
  /\ stack     = [w \in Workers    |-> << >>]
  /\ lo        = [w \in Workers    |-> 0]
  /\ hi        = [w \in Workers    |-> 0]
  /\ pivot     = [w \in Workers    |-> UNDEF]
  /\ idxI      = [w \in Workers    |-> 0]
  /\ idxJ      = [w \in Workers    |-> 0]
  /\ sliceInit = [w \in Workers    |-> [i \in Indices |-> UNDEF]]

----------------------------------------------------------------------------
(* Helpers. *)

NotInited(w) == { k \in ProcRange(w) : ~ inited[TargetArray][k] }

(* Smallest uninitialized index in worker w's slice. We pin init order to *)
(* a canonical (ascending) sequence so the init phase does not balloon the *)
(* state space with order permutations. The values themselves remain       *)
(* nondeterministic, exercising every initial array.                       *)
SmallestNotInited(w) ==
  CHOOSE k \in NotInited(w) : \A j \in NotInited(w) : k <= j

(* Two-cell swap on TargetArray. Both indices must be owned and inited. *)
DoSwap(w, i1, i2) ==
  /\ Assert(OwnsCell(w, i1), "swap: i1 not owned by worker")
  /\ Assert(OwnsCell(w, i2), "swap: i2 not owned by worker")
  /\ Assert(inited[TargetArray][i1], "swap: read of uninited cell at i1")
  /\ Assert(inited[TargetArray][i2], "swap: read of uninited cell at i2")
  /\ arr' = [arr EXCEPT
        ![TargetArray] = [@ EXCEPT
              ![i1] = arr[TargetArray][i2],
              ![i2] = arr[TargetArray][i1]]]

----------------------------------------------------------------------------
(* Phase 1: Initialization. Each worker writes its own slice with values    *)
(* drawn nondeterministically from Values, one cell per step.                *)

InitOneCell(w) ==
  /\ ctrl[w] = "Init"
  /\ NotInited(w) /= {}
  /\ LET k == SmallestNotInited(w) IN
       \E v \in Values :
         /\ Assert(OwnsCell(w, k), "Init wrote outside worker slice")
         /\ arr'    = [arr    EXCEPT ![TargetArray] = [@ EXCEPT ![k] = v]]
         /\ inited' = [inited EXCEPT ![TargetArray] = [@ EXCEPT ![k] = TRUE]]
  /\ UNCHANGED <<ctrl, stack, lo, hi, pivot, idxI, idxJ, sliceInit>>

FinishInit(w) ==
  /\ ctrl[w]   = "Init"
  /\ NotInited(w) = {}
  /\ ctrl'  = [ctrl  EXCEPT ![w] = "Pop"]
  /\ stack' = [stack EXCEPT
                 ![w] = << [lo |-> MinIdx(w), hi |-> MaxIdx(w)] >>]
  (* Snapshot ONLY this worker's own slice (other indices stay UNDEF).   *)
  (* This keeps sliceInit[w] a deterministic function of w's own init    *)
  (* choices, so it does not blow up the state space with cross-worker   *)
  (* timing variants.                                                     *)
  /\ sliceInit' = [sliceInit EXCEPT ![w] =
        [i \in Indices |-> IF i \in ProcRange(w)
                             THEN arr[TargetArray][i]
                             ELSE UNDEF]]
  /\ UNCHANGED <<arr, inited, lo, hi, pivot, idxI, idxJ>>

----------------------------------------------------------------------------
(* Phase 2: Iterative Lomuto quicksort. Per-worker stack of intervals.       *)

(* Pop the top interval. Empty/singleton intervals are discarded.            *)
PopInterval(w) ==
  /\ ctrl[w] = "Pop"
  /\ stack[w] /= << >>
  /\ LET top == Head(stack[w]) IN
       IF top.lo >= top.hi
       THEN /\ stack' = [stack EXCEPT ![w] = Tail(stack[w])]
            /\ UNCHANGED <<arr, inited, ctrl, lo, hi, pivot, idxI, idxJ,
                           sliceInit>>
       ELSE /\ Assert(OwnsCell(w, top.lo) /\ OwnsCell(w, top.hi),
                      "PopInterval popped interval outside slice")
            /\ stack' = [stack EXCEPT ![w] = Tail(stack[w])]
            /\ ctrl'  = [ctrl  EXCEPT ![w] = "ReadPivot"]
            /\ lo'    = [lo    EXCEPT ![w] = top.lo]
            /\ hi'    = [hi    EXCEPT ![w] = top.hi]
            /\ UNCHANGED <<arr, inited, pivot, idxI, idxJ, sliceInit>>

(* Stack drained -> worker finished. *)
WorkerFinish(w) ==
  /\ ctrl[w] = "Pop"
  /\ stack[w] = << >>
  /\ ctrl' = [ctrl EXCEPT ![w] = "Done"]
  /\ UNCHANGED <<arr, inited, stack, lo, hi, pivot, idxI, idxJ, sliceInit>>

(* Read pivot from arr[hi]. This is the FIRST read of the partition.        *)
ReadPivot(w) ==
  /\ ctrl[w] = "ReadPivot"
  /\ Assert(OwnsCell(w, hi[w]),
            "ReadPivot accessed cell outside slice")
  /\ Assert(inited[TargetArray][hi[w]],
            "ReadPivot read of uninited cell")
  /\ pivot' = [pivot EXCEPT ![w] = arr[TargetArray][hi[w]]]
  /\ idxI'  = [idxI  EXCEPT ![w] = lo[w] - 1]
  /\ idxJ'  = [idxJ  EXCEPT ![w] = lo[w]]
  /\ ctrl'  = [ctrl  EXCEPT ![w] = "PartStep"]
  /\ UNCHANGED <<arr, inited, stack, lo, hi, sliceInit>>

(* One iteration of the Lomuto inner loop: read arr[j], compare to pivot,    *)
(* possibly increment i and swap arr[i+1] with arr[j], then advance j.       *)
PartStep(w) ==
  /\ ctrl[w] = "PartStep"
  /\ idxJ[w] < hi[w]
  /\ Assert(OwnsCell(w, idxJ[w]),
            "PartStep accessed cell outside slice")
  /\ Assert(inited[TargetArray][idxJ[w]],
            "PartStep read of uninited cell")
  /\ LET v == arr[TargetArray][idxJ[w]] IN
       IF v <= pivot[w]
       THEN /\ DoSwap(w, idxI[w] + 1, idxJ[w])
            /\ idxI' = [idxI EXCEPT ![w] = @ + 1]
            /\ idxJ' = [idxJ EXCEPT ![w] = @ + 1]
            /\ UNCHANGED <<inited, ctrl, stack, lo, hi, pivot, sliceInit>>
       ELSE /\ idxJ' = [idxJ EXCEPT ![w] = @ + 1]
            /\ UNCHANGED <<arr, inited, ctrl, stack, lo, hi, pivot, idxI,
                           sliceInit>>

(* Inner loop terminated: do final pivot swap and push two sub-intervals.    *)
PartFinal(w) ==
  /\ ctrl[w] = "PartStep"
  /\ idxJ[w] >= hi[w]
  /\ DoSwap(w, idxI[w] + 1, hi[w])
  /\ stack' = [stack EXCEPT ![w] =
        << [lo |-> lo[w],          hi |-> idxI[w]],
           [lo |-> idxI[w] + 2,    hi |-> hi[w]] >> \o stack[w]]
  /\ ctrl'  = [ctrl EXCEPT ![w] = "Pop"]
  /\ UNCHANGED <<inited, lo, hi, pivot, idxI, idxJ, sliceInit>>

----------------------------------------------------------------------------
(* Per-worker step relation. *)

WorkerStep(w) ==
  \/ InitOneCell(w)
  \/ FinishInit(w)
  \/ PopInterval(w)
  \/ WorkerFinish(w)
  \/ ReadPivot(w)
  \/ PartStep(w)
  \/ PartFinal(w)

(* Stutter when every worker is Done. Without this, the system "deadlocks"  *)
(* in TLC's view at the terminal state. We want the terminal state to be    *)
(* reachable AND non-deadlocking. *)
TerminalStutter ==
  /\ \A w \in Workers : ctrl[w] = "Done"
  /\ UNCHANGED vars  \* vars already includes sliceInit

Next == (\E w \in Workers : WorkerStep(w)) \/ TerminalStutter

----------------------------------------------------------------------------
(* Specification: weak fairness on each worker so Termination is provable.   *)

Spec ==
  /\ Init
  /\ [][Next]_vars
  /\ \A w \in Workers : WF_vars(WorkerStep(w))

----------------------------------------------------------------------------
(* Properties.                                                              *)

AllDone == \A w \in Workers : ctrl[w] = "Done"

(* On AllDone, each worker's slice is sorted in TargetArray.                *)
(* Defensive: every read of arr is conjoined with the inited flag, so a    *)
(* buggy variant that reaches AllDone with uninited cells produces a clean *)
(* invariant violation rather than crashing TLC on UNDEF <= UNDEF.          *)
SliceSorted(w) ==
  /\ \A i \in ProcRange(w) : inited[TargetArray][i]
  /\ \A i, j \in ProcRange(w) :
       i < j => arr[TargetArray][i] <= arr[TargetArray][j]

Sortedness ==
  AllDone => \A w \in Workers : SliceSorted(w)

(* Data-preservation invariant: on AllDone, the multiset of values in     *)
(* every worker's slice equals the multiset captured at FinishInit. This  *)
(* catches bugs where DoSwap loses or fabricates values (e.g. zeroing a    *)
(* cell, double-writing a single source, reading the wrong cell).         *)
SliceCount(w, v) ==
  Cardinality({i \in ProcRange(w) : arr[TargetArray][i] = v})
SliceInitCount(w, v) ==
  Cardinality({i \in ProcRange(w) : sliceInit[w][i] = v})

PermutationPreserved ==
  AllDone =>
    \A w \in Workers : \A v \in Values :
      SliceCount(w, v) = SliceInitCount(w, v)

(* On AllDone, every cell of TargetArray is initialized. *)
AllTargetInited ==
  AllDone => \A i \in Indices : inited[TargetArray][i]

(* Inited flags are monotonic: once TRUE, never FALSE. *)
InitMonotonic ==
  [][\A a \in ArrayNames, i \in Indices :
        inited[a][i] => inited'[a][i]]_vars

(* Termination: under WF, every worker eventually reaches Done. *)
Termination == <>AllDone

----------------------------------------------------------------------------
(* Bug-injection demonstrations -- see README. To activate one, edit the    *)
(* indicated definition above. TLC will then report a violation.            *)
(*                                                                          *)
(*  BUG_VARIANT_1: read before init                                          *)
(*    In ReadPivot, delete the line                                          *)
(*       /\ Assert(inited[TargetArray][hi[w]], ... )                         *)
(*    AND replace FinishInit's NotInited(w) = {} guard with TRUE.            *)
(*    Result: TLC aborts on the Assert in DoSwap or PartStep when an         *)
(*    uninited cell is read.                                                 *)
(*                                                                          *)
(*  BUG_VARIANT_2: overlapping slices                                        *)
(*    Replace MaxIdx(w) ==  ChunkSize * w                                    *)
(*    with    MaxIdx(w) == IF w < NumWorkers                                 *)
(*                         THEN ChunkSize * w + 1                            *)
(*                         ELSE ChunkSize * w                                *)
(*    Result: ASSUME DisjointPartitionCheck fails at TLC startup with        *)
(*    "Assumption is false". TLC aborts before exploring any state.          *)
(*    Even if the ASSUME were removed, the strengthened OwnsCell             *)
(*    (which requires NO other worker to claim the cell) makes the           *)
(*    runtime Asserts in InitOneCell / DoSwap / ReadPivot / PartStep         *)
(*    fire on the first overlap-region access.                               *)
(*                                                                          *)
(*  BUG_VARIANT_3: skip initialization                                       *)
(*    In FinishInit, weaken the guard `NotInited(w) = {}` to `TRUE`.         *)
(*    Result: ReadPivot or PartStep fires before all cells inited; the       *)
(*    inited Assert aborts TLC with the named message.                      *)
(*                                                                          *)
(*  BUG_VARIANT_4: data corruption that preserves sortedness                 *)
(*    In DoSwap, replace                                                     *)
(*       ![i1] = arr[TargetArray][i2],                                       *)
(*       ![i2] = arr[TargetArray][i1]                                        *)
(*    with    ![i1] = 0, ![i2] = 0.                                          *)
(*    Sortedness still holds (final array is all zeros, trivially sorted).   *)
(*    PermutationPreserved fails -- the slice multiset has changed.          *)
(*    Demonstrates that Sortedness alone is insufficient and that the        *)
(*    data-preservation invariant is needed to catch silent corruption.     *)
(***************************************************************************)
=============================================================================