1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
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.
=============================================================================
|
