diff options
Diffstat (limited to 'formal/tla/SleepSort.tla')
| -rw-r--r-- | formal/tla/SleepSort.tla | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/formal/tla/SleepSort.tla b/formal/tla/SleepSort.tla new file mode 100644 index 0000000..45cc0e0 --- /dev/null +++ b/formal/tla/SleepSort.tla @@ -0,0 +1,108 @@ +------------------------------ MODULE SleepSort ------------------------------ +(***************************************************************************) +(* A TLA+ model of the sleep sort in sort/sleep.go. *) +(* *) +(* This verifies a *model*, not the Go source. It abstracts the goroutines *) +(* + WaitGroup + unbuffered channel of sleep.go into: *) +(* *) +(* - a global discrete clock (stand-in for wall-clock time / sleeps), *) +(* - one "timer" per input element that fires when the clock reaches *) +(* that element's value (a value-v element sleeps v seconds), and *) +(* - a single collector that receives one fired value at a time *) +(* (an unbuffered channel with one receiver hands off exactly one *) +(* value per rendezvous, with no buffering or reordering). *) +(* *) +(* Crucially, sortedness of the output is NOT baked in: it must *emerge* *) +(* from the timing mechanism. The only thing that enforces order is Tick's *) +(* urgency guard (time cannot pass while a fired-but-unreceived timer is *) +(* waiting). Remove that guard and TLC finds an unsorted counterexample -- *) +(* which is exactly what makes this a real check rather than a tautology. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANT Input \* the values to sort, as a sequence, e.g. <<3, 1, 2>> + +\* Concrete value for the model. TLC config files cannot parse a sequence +\* literal in a "CONSTANT Input = ..." assignment, so SleepSort.cfg overrides the +\* constant with this operator via "CONSTANT Input <- InputValue". +InputValue == <<3, 1, 4, 1, 2>> + +Idx == DOMAIN Input +Values == { Input[i] : i \in Idx } + +VARIABLES + clock, \* global time; the sleeps are measured against it + sent, \* sent[i] = TRUE once element i has been received + output \* the values collected so far, in arrival order + +vars == <<clock, sent, output>> + +\* Multiplicity of value v in a sequence s (compares the two as multisets). +Count(v, s) == Cardinality({ k \in DOMAIN s : s[k] = v }) + +TypeOK == + /\ clock \in Nat + /\ sent \in [Idx -> BOOLEAN] + /\ \A k \in DOMAIN output : output[k] \in Values + /\ Len(output) =< Cardinality(Idx) + +Init == + /\ clock = 0 + /\ sent = [i \in Idx |-> FALSE] + /\ output = << >> + +\* Element i's timer has fired (its sleep of Input[i] seconds has elapsed) and +\* it has not yet been received. +Ready(i) == /\ ~sent[i] + /\ clock >= Input[i] + +AllDone == \A i \in Idx : sent[i] + +\* The collector receives one ready value (channel rendezvous: exactly one +\* value transfers, chosen nondeterministically among those currently ready). +Receive == + /\ \E i \in Idx : + /\ Ready(i) + /\ sent' = [sent EXCEPT ![i] = TRUE] + /\ output' = Append(output, Input[i]) + /\ clock' = clock + +\* Time advances only when no fired timer is waiting to be received: every +\* not-yet-received element still has its deadline strictly in the future. +\* This urgency is what guarantees shorter sleeps deliver before longer ones. +Tick == + /\ ~AllDone + /\ \A i \in Idx : ~sent[i] => clock < Input[i] + /\ clock' = clock + 1 + /\ UNCHANGED <<sent, output>> + +\* Once everything has been collected, stutter (models the closed channel / +\* finished range loop) so termination is not mistaken for a deadlock. +Done == + /\ AllDone + /\ UNCHANGED vars + +Next == Receive \/ Tick \/ Done + +Spec == Init /\ [][Next]_vars /\ WF_vars(Receive) /\ WF_vars(Tick) + +----------------------------------------------------------------------------- +\* Properties checked by TLC (see SleepSort.cfg). + +\* SAFETY: whatever has been collected so far is always non-decreasing. +IsSorted(s) == \A a, b \in DOMAIN s : a < b => s[a] <= s[b] +OutputSorted == IsSorted(output) + +\* SAFETY: the output never invents or duplicates values, and once finished it +\* is exactly a permutation (multiset) of the input. +PermutationWhenDone == + AllDone => \A v \in Values : Count(v, output) = Count(v, Input) + +\* LIVENESS: the collector eventually receives every value (no deadlock, no +\* value left sleeping forever) -- i.e. the algorithm terminates. +Terminates == <>AllDone + +\* Note: the state space is already finite without a constraint -- Tick is +\* disabled once clock reaches the largest input value, so clock never grows +\* unbounded and TLC explores every reachable state. +============================================================================= |