diff options
Diffstat (limited to 'formal/tla/README.md')
| -rw-r--r-- | formal/tla/README.md | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/formal/tla/README.md b/formal/tla/README.md index a80c687..16a6744 100644 --- a/formal/tla/README.md +++ b/formal/tla/README.md @@ -1,8 +1,25 @@ -# TLA+ model check of sleep sort +# TLA+ model checks of the concurrent sorts -`SleepSort.tla` is a [TLA+](https://lamport.azurewebsites.net/tla/tla.html) -model of the concurrent sleep sort in [`sort/sleep.go`](../../sort/sleep.go), -checked exhaustively by the TLC model checker. +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 |