blob: 16a67443e0d65066fd3c8d97e243a4bdccacaa54 (
plain)
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
|
# TLA+ model checks of the concurrent sorts
Two [TLA+](https://lamport.azurewebsites.net/tla/tla.html) models, checked
exhaustively by the TLC model checker:
- **`SleepSort.tla`** — the sleep sort in [`sort/sleep.go`](../../sort/sleep.go).
- **`ParallelSort.tla`** — the fork/join structure shared by
[`sort/parallelmerge.go`](../../sort/parallelmerge.go) and
[`sort/parallelquick.go`](../../sort/parallelquick.go): checks that
concurrently-writing tasks own **disjoint** array ranges (no data race) and
that the join always completes (termination). Removing the WaitGroup fence
(letting a parent merge before its children finish) makes TLC report
`Invariant NoDataRace is violated` — so the check has teeth. This model
complements the dynamic race detector (`make verify`) with an *exhaustive*
guarantee over the whole recursion tree.
The rest of this file documents `SleepSort.tla`.
## SleepSort
`SleepSort.tla` models the concurrent sleep sort in
[`sort/sleep.go`](../../sort/sleep.go).
## What this does and does NOT prove
Model checking verifies a **hand-written model**, not the Go source. TLC
explores *every* reachable state of the model and confirms:
- **`OutputSorted`** (safety) — the collected output is always non-decreasing.
- **`PermutationWhenDone`** (safety) — the output is a multiset permutation of
the input; nothing is dropped, duplicated, or invented.
- **`Terminates`** (liveness) — the collector eventually receives every value:
no deadlock and no value left sleeping forever.
The gap you keep responsibility for: that the model faithfully abstracts
`sleep.go`. The model represents the sleeps as a discrete clock and the
unbuffered channel + `WaitGroup` as an urgent single-value rendezvous — see the
header comment in `SleepSort.tla`.
Sortedness is **not** assumed. It emerges from one rule: time cannot pass while
a fired-but-unreceived timer waits (`Tick`'s urgency guard). Delete that guard
and TLC finds an unsorted counterexample — proof the check has teeth.
## Running
Needs Java and `tla2tools.jar` (download once):
```sh
mkdir -p ~/tools/tlaplus
curl -fsSL -o ~/tools/tlaplus/tla2tools.jar \
https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
```
Then, from the repository root:
```sh
make verify-model
```
or directly:
```sh
java -cp ~/tools/tlaplus/tla2tools.jar tlc2.TLC \
-config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla
```
Expected output ends with:
```
Model checking completed. No error has been found.
```
## The input
`SleepSort.cfg` checks the input `<<3, 1, 4, 1, 2>>` (defined as `InputValue`
in the module, because a `.cfg` cannot hold a sequence literal). It has a
duplicate and is out of order — enough to exercise ordering, ties, and
termination. Edit `InputValue` in `SleepSort.tla` to try others; the state space
stays small because the clock never exceeds the largest input value.
|
