From 3f906d03262150892e2297e621bfc56e425ef142 Mon Sep 17 00:00:00 2001 From: Paul Buetow Date: Mon, 6 Jul 2026 10:32:34 +0300 Subject: Close verification-coverage gaps; harness finds two more bugs Extends the verification harness from sorts-only to the whole repo, and in doing so surfaces two further latent bugs (on top of the earlier hash-shift one): Bugs found and fixed: - queue/elementarypriority.go: max() seeded at the zero value, so an all-negative queue reported a phantom max of 0 and DeleteMax returned/removed the wrong element. Caught by the new queue permutation property (testing/quick generates negatives; the old test data never did). Seed from a[0] instead. - sort/sleep.go: result built on NewArrayList(len(a)) -- a slice of that LENGTH (len(a) zeros) -- then appended to, yielding double-length output with leading zeros. The old .Sorted()-only test passed because zeros-then-ascending is sorted. Caught by the new Sleep permutation check. Build from an empty slice. Coverage added: - queue/property_test.go: ordering + permutation (completeness) for both queues. - TestSleepSort now also checks permutation, not just Sorted(). - docs/verification.md: paper proofs for all search/set structures (Elementary, Hash, BST, red-black BST invariants, GoMap) and both priority queues. - formal/tla/ParallelSort.tla: exhaustive fork/join model of ParallelMerge/ ParallelQuick -- disjoint write-ranges (no data race) + termination. Wired into make verify-model. - formal/selection.go: second Gobra proof (memory safety + sortedness). Wired into make verify-formal. - docs/case-study-bugs-found.md: extensive write-up of all three bugs, how each was caught, why the old tests missed it, and the fix (supersedes the earlier single-bug case study). Co-Authored-By: Claude Opus 4.8 --- formal/tla/README.md | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) (limited to 'formal/tla/README.md') 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 -- cgit v1.2.3