diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | docs/case-study-bugs-found.md | 218 | ||||
| -rw-r--r-- | docs/case-study-hash-shift-bug.md | 157 | ||||
| -rw-r--r-- | docs/verification.md | 213 | ||||
| -rw-r--r-- | formal/README.md | 25 | ||||
| -rw-r--r-- | formal/selection.go | 48 | ||||
| -rw-r--r-- | formal/tla/ParallelSort.cfg | 13 | ||||
| -rw-r--r-- | formal/tla/ParallelSort.tla | 117 | ||||
| -rw-r--r-- | formal/tla/README.md | 25 | ||||
| -rw-r--r-- | queue/elementarypriority.go | 7 | ||||
| -rw-r--r-- | queue/property_test.go | 76 | ||||
| -rw-r--r-- | sort/sleep.go | 5 | ||||
| -rw-r--r-- | sort/sort_test.go | 17 |
13 files changed, 738 insertions, 191 deletions
@@ -16,15 +16,19 @@ verify: # (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md. verify-model: java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ - -metadir /tmp/tlc-algorithms \ + -metadir /tmp/tlc-sleepsort \ -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla + java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ + -metadir /tmp/tlc-parallelsort \ + -config formal/tla/ParallelSort.cfg formal/tla/ParallelSort.tla # verify-formal: machine-checked deductive proof of a monomorphized insertion # sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image. # See formal/README.md. verify-formal: podman run --rm -v $(PWD)/formal:/gobra/formal:z \ - ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go + ghcr.io/viperproject/gobra:latest \ + -i /gobra/formal/insertion.go /gobra/formal/selection.go bench: go test -run=xxx -bench=. ./... | tee bench.out sortbench: diff --git a/docs/case-study-bugs-found.md b/docs/case-study-bugs-found.md new file mode 100644 index 0000000..3f5f0a9 --- /dev/null +++ b/docs/case-study-bugs-found.md @@ -0,0 +1,218 @@ +# Case study: three latent bugs the verification harness found + +Adding the verification layers (see [`verification.md`](verification.md)) did not +just re-confirm working code — it surfaced **three real, pre-existing bugs**, all +invisible to the original test suite. Each is documented below with how it was +caught, why it is genuinely wrong, why the old tests missed it, and the fix. + +A theme runs through all three: the original tests were **too weak in a specific +dimension**, and the new checks are strong in exactly that dimension. + +| # | Location | Bug | Caught by | Old test's blind spot | +|---|----------|-----|-----------|-----------------------| +| 1 | `search/hash.go` | shift wider than a narrow key type → term is always 0 | `go vet` (in `make verify`) | only ever used 64-bit `int` keys | +| 2 | `queue/elementarypriority.go` | `max()` seeded at `0` → wrong for all-negative queues | queue permutation property | test data was never negative | +| 3 | `sort/sleep.go` | result built on a pre-sized slice → doubled length with leading zeros | sleep permutation property | only checked `.Sorted()`, not completeness | + +--- + +## Bug 1 — a shift wider than the key type (`search/hash.go`) + +### The offending code + +```go +func (h *Hash[K,V]) hash(key K) int { + i := key + key*2 + key<<10 + key>>2 + ... +} +``` + +`K` is constrained by `ds.Integer`, so it may be **any** width down to `int8`. +The `key<<10` term is meant to spread low bits into high bits. + +### What the tool reported + +``` +$ make verify +go vet ./... +search/hash.go:29:21: key (may be 8 bits) too small for shift of 10 +``` + +`go vet`'s shift analyzer is a lightweight formal check: for every shift it +computes a conservative lower bound on the left operand's bit width and flags any +shift count `>=` that width. The narrowest `K` can be is `int8` (8 bits), and +`10 >= 8`. + +### Why it is genuinely a bug (Go shift semantics) + +The Go spec defines non-constant left shifts operationally: *"Shifts behave as if +the left operand is shifted n times by 1 … There is no upper limit on the shift +count."* Shifting an 8-bit value ten times pushes every bit out of the value's +width, so for `K = int8`/`uint8`: + +``` +key<<10 == 0 // always, for every key +``` + +The intended high-bit mixing silently disappears. Note it is width-dependent +(fine for `int16`+), and it is a *distribution/quality* bug, not a Set-contract +violation — chaining keeps the table correct, but narrow-key instantiations +degrade toward `O(n)` per operation. Exactly the kind of silent rot no assertion +would flag. + +### Why the tests missed it + +Every test uses `int` keys (`test[int,int](NewHash[int,int](i*2), …)`), where +`int` is 64 bits and the shift is fine. The bug lives in the **type dimension**, +not the value dimension — no value-space test or fuzzer over `int` could reach +it; only a type-aware tool (or an actual `int8` instantiation) can. + +### The fix + +```go +func (h *Hash[K,V]) hash(key K) int { + // Mix the key in a full-width int64 rather than in K. ... + i := int64(key) + i = i + i*2 + i<<10 + i>>2 + ... +} +``` + +Widening to `int64` before the shift keeps the result **byte-identical for +64-bit `int` keys** (so all existing tests still pass unchanged) while making the +mixing well-defined for every width. It does not *suppress* the warning; it +removes the condition (`shift >= width`) that made it true. + +--- + +## Bug 2 — a maximum seeded at zero (`queue/elementarypriority.go`) + +### The offending code + +```go +func (q *ElementaryPriority[T]) max() (ind int, max T) { + for i, a := range q.a { + if a > max { // max starts at the zero value of T, i.e. 0 + ind, max = i, a + } + } + return ind, max +} +``` + +`max` is a named return, so it starts at `T`'s zero value, `0`. + +### How it was caught + +The new completeness/permutation property in `queue/property_test.go` drives +each queue with `testing/quick`, which generates **negative** values too. It +failed immediately for `ElementaryPriority` (and passed for `HeapPriority`): + +``` +ElementaryPriority violated ordered-permutation property: + #1: failed on input []int{-1881664299226649700, 1264358012858162353, ...} +``` + +### Why it is genuinely a bug + +If **every** element in the queue is negative, no element is `> 0`, so the loop +never updates and `max()` returns `(0, 0)` — reporting a maximum of `0`, a value +that is not even in the queue. `DeleteMax` then removes the wrong element (index +0) and returns a phantom `0`. Both the ordering and completeness of a drain +break. + +### Why the tests missed it + +The original queue test builds inputs with +`ds.NewRandomArrayList[int](l, -1)`, whose values come from `rand.Int()` — always +**non-negative**. And `queue_test.go` only checked that `DeleteMax` was +non-increasing; it never checked that all inserted elements come back. So a queue +of non-negative numbers, checked only for ordering, sailed through. + +### The fix + +```go + if len(q.a) == 0 { + return 0, 0 + } + ind, max = 0, q.a[0] // seed from a real element, not the zero value + for i, a := range q.a { + if a > max { ind, max = i, a } + } +``` + +Seeding from `q.a[0]` makes the scan correct for any value range. +(`HeapPriority` was already immune: it compares actual array elements and returns +`a[1]` as the max.) + +--- + +## Bug 3 — a sort that doubled its output (`sort/sleep.go`) + +### The offending code + +```go +func Sleep[V ds.Integer](a ds.ArrayList[V]) ds.ArrayList[V] { + sorted := ds.NewArrayList[V](len(a)) // slice of LENGTH len(a): len(a) zeros + ... + for num := range numCh { + sorted = append(sorted, num) // appends AFTER those zeros + } + return sorted +} +``` + +`ds.NewArrayList(len(a))` is `make(ArrayList, len(a))` — a slice of that +**length**, pre-filled with `len(a)` zeros. Appending then adds the real values +*after* them. + +### How it was caught + +`TestSleepSort`, strengthened to check permutation, failed: + +``` +Sleep sort output is not a permutation of input: + in =[1 1 2 8 8 7 3 0 6 7] (10 elements) + out=[0 0 0 0 0 0 0 0 0 0 0 1 1 2 3 6 7 7 8 8] (21 elements!) +``` + +The output is **eleven leading zeros followed by the ten real values** — more +than double the input length. + +### Why the tests missed it + +The original `TestSleepSort` only asserted `a.Sorted()`. Zeros followed by an +ascending sequence **is** sorted, so the wildly-wrong 21-element result passed. +This is the textbook case for the *permutation* invariant: ordering alone cannot +detect dropped, duplicated, or (here) invented elements. + +### The fix + +```go + // Start empty with capacity len(a): the received values are appended below. + sorted := make(ds.ArrayList[V], 0, len(a)) +``` + +Length `0`, capacity `len(a)`: the appends now fill it to exactly `len(a)` +elements with no spurious zeros. + +--- + +## The through-line + +Two independent lessons, each reinforced twice: + +1. **Ordering is not correctness.** Bugs 2 and 3 both produced *ordered* output + that was wrong (missing/extra elements). Only the **permutation / completeness** + invariant — added to the sort and queue property tests — catches them. This is + the single most valuable check added by this work. + +2. **Test data has blind spots the code doesn't.** Bugs 1 and 2 both hid behind + the test suite's fixed input distribution — always 64-bit, always + non-negative. `go vet` (reasoning over *types*) and `testing/quick` (sampling + the *whole* value range, negatives included) each see past a blind spot that + hand-picked or `rand.Int()` data does not. + +None of these required the heavy layers (TLA+, Gobra). The cheapest checks — +`go vet` and a stronger property assertion — found all three. Breadth first; +depth where it earns its keep. diff --git a/docs/case-study-hash-shift-bug.md b/docs/case-study-hash-shift-bug.md deleted file mode 100644 index 6ec4f7d..0000000 --- a/docs/case-study-hash-shift-bug.md +++ /dev/null @@ -1,157 +0,0 @@ -# Case study: a latent bug the verification harness caught - -This documents a real defect that the verification work found **on the very -first run** of the new `make verify` target — before any of the heavier layers -(TLA+, Gobra) were even involved. It is a good illustration of *why* wiring -these checks into a gate pays off: the bug had been sitting in the repository -undetected because the existing tests could never trigger it. - -## TL;DR - -- **Where:** `search/hash.go`, the `Hash.hash` method. -- **What:** `key << 10`, where `key` has a generic integer type, silently - evaluates to `0` for narrow key types (`int8`/`uint8`), discarding a whole - term of the hash mix. -- **Who found it:** `go vet`'s shift analyzer, run as part of `make verify`. -- **Why the tests missed it:** every test instantiates the hash with 64-bit - `int` keys, where the shift is perfectly fine — so the bug is *latent*. -- **Fix:** compute the mix in a full-width `int64`. - -## The offending code - -Before: - -```go -func (h *Hash[K,V]) hash(key K) int { - i := key + key*2 + key<<10 + key>>2 - if i < 0 { - i = -i - } - return int(i) % h.capacity -} -``` - -`K` is a type parameter constrained by `ds.Integer` (`ds/types.go`), which -embeds `constraints.Integer` — i.e. `K` may be **any** of `int, int8, int16, -int32, int64, uint, uint8, …`. The intent of `key<<10` is clearly to spread the -key's low bits up into the high bits so that keys differing only in their low -bits land in different buckets. - -## What the tool reported - -``` -$ make verify -go vet ./... -search/hash.go:29:21: key (may be 8 bits) too small for shift of 10 -``` - -`go vet` bundles a *shift* analyzer that is, in effect, a lightweight formal -check: for every shift expression it computes a conservative lower bound on the -bit width of the left operand and flags any shift whose count is `>=` that -width. Here the narrowest type `K` can take is `int8` (8 bits), and `10 >= 8`, -so the analyzer proves that *for at least one legal instantiation* the shift is -degenerate. - -## Why it is genuinely a bug (Go shift semantics) - -This is not a false positive. The Go specification defines non-constant left -shifts operationally: - -> Shifts behave as if the left operand is shifted `n` times by 1 for a shift -> count of `n`. […] There is no upper limit on the shift count. - -For an 8-bit value, shifting "one bit at a time" ten times pushes **every** -original bit out of the value's width. The result is therefore always `0`. So -for `K = int8`/`uint8`: - -``` -key<<10 == 0 // always, for every key -``` - -and the hash silently collapses to `key + key*2 + key>>2` — the high-bit mixing -the author intended is simply gone. - -Two subtleties worth recording: - -1. **It is width-dependent, not universally broken.** For `int16` the count - `10 < 16`, so the term is fine; for 32-/64-bit types it is obviously fine. - `go vet` still (correctly) flags the expression because it must be sound for - *all* instantiations, and `int8` is in the constraint set. The narrowest - type is what governs safety. - -2. **It is a quality/portability bug, not a memory-safety or a Set-contract - violation.** The hash table stays *functionally correct* even for `int8` - keys: `Put`, `Get`, and `Del` all call the same `hash`, and collisions are - resolved by chaining in the per-bucket `Elementary` list. What degrades is - the *distribution* — more keys collide into the same bucket, turning the - intended O(1) operations toward O(n). So the failure mode is silent - performance rot for narrow-key instantiations, exactly the kind of thing that - never shows up as a failing assertion. - -## Why no test caught it - -Every instantiation in the test suite uses `int` keys: - -```go -test[int,int](NewHash[int,int](i*2), i, t) // search/search_test.go -``` - -`int` is 64 bits on this platform, so `key<<10` behaves as intended and all -tests pass. There is no `Hash[int8, …]` anywhere, so the degenerate path is -never exercised. A property test or a fuzz run over `int` keys would *also* miss -it — the bug lives in the *type dimension*, not the value dimension, and only a -tool that reasons about the type (like `go vet`) or an actual narrow-type -instantiation can surface it. This is precisely the class of latent defect that -static analysis is good at and dynamic testing is blind to. - -## The fix - -Perform the mixing in a full-width `int64`, then reduce: - -```go -func (h *Hash[K,V]) hash(key K) int { - // Mix the key in a full-width int64 rather than in K. K is any ds.Integer, - // so for a narrow type (e.g. int8) the "key<<10" term would shift past the - // type width and vanish to 0, destroying the intended high-bit mixing (and - // go vet rightly flags it). Widening to int64 first keeps the result - // identical for 64-bit int keys while making the mix well-defined for every - // integer width. - i := int64(key) - i = i + i*2 + i<<10 + i>>2 - if i < 0 { - i = -i - } - return int(i) % h.capacity -} -``` - -Why this is the right fix: - -- **Behavior-preserving for the code that exists.** For `K = int` (64-bit), the - arithmetic is byte-for-byte identical to before — `int64(key)` is a no-op - widening, and every operation stays in 64 bits — so every existing test still - passes unchanged. -- **Correct for the code that might exist.** For narrow `K`, the key is widened - *before* the shift, so `i<<10` now mixes real bits instead of vanishing. The - hash finally does for `int8` keys what it always did for `int` keys. -- **It silences the analyzer for the right reason.** `int64` is 64 bits, `10 < - 64`, so the shift is provably well-defined for the actual operand type. We are - not suppressing the warning; we are removing the condition that made it true. - -An `int64` cast rather than the value's own width also documents intent: "this -mixing is meant to happen in a wide register, independent of the key type." - -> Residual note, left as-is: `if i < 0 { i = -i }` still has the classic -> `-math.MinInt64` overflow corner. It predates this change, is astronomically -> unlikely for these inputs, and is out of scope here — recorded for honesty. - -## How this maps to the verification layers - -This defect was caught by **Layer 2** of the harness (see -[`verification.md`](verification.md)) — `go vet` inside `make verify`. It is the -cheapest layer, and it found a bug that the paper proofs (Layer 0, which focus -on the sorts) and the property tests (Layer 1, which only ever run `int`) did -not. The lesson is the ordering of the layers is not the ordering of their -value: a one-line static check surfaced a real, shipped-in latent bug that no -amount of value-space testing would have. Cheap, broad checks first; deep proofs -where they earn their keep. diff --git a/docs/verification.md b/docs/verification.md index 3959e5b..e845d79 100644 --- a/docs/verification.md +++ b/docs/verification.md @@ -1,21 +1,28 @@ # Hand-written correctness proofs This document contains human-written (paper) correctness proofs for the -algorithms in this repository, derived by reading the actual source. Each proof -is a Hoare-style argument: a **precondition**, a **postcondition**, one **loop -invariant** per loop, a **termination measure**, and — for the sorts — a -**permutation argument**. +algorithms in this repository, derived by reading the actual source. It covers +the **sorts**, the **search/set structures**, and the **priority queues**. Each +proof is a Hoare-style argument: a **precondition**, a **postcondition**, the +relevant **invariant** (loop invariant, BST order, heap order, …), a +**termination measure**, and — where relevant — a **permutation argument**. These proofs are the human-readable source of truth. They are *human-checked*, not machine-checked; the automated layers corroborate them: -- `sort/property_test.go` checks *ordering* **and** *permutation* on thousands - of random inputs (empirical corroboration — see the "permutation" note below). -- `make verify` runs `go vet`, `staticcheck`, and the race detector. This layer - already paid off: it caught a latent bug in `search/hash.go` on its first run - — see [`case-study-hash-shift-bug.md`](case-study-hash-shift-bug.md). -- `formal/tla/SleepSort.tla` exhaustively model-checks the concurrent sleep sort. -- `formal/insertion.go` is a machine-checked (Gobra) proof of insertion sort. +- `sort/property_test.go` and `queue/property_test.go` check *ordering* **and** + *permutation* on thousands of random inputs; `search/search_test.go` + oracle-checks the set contract against Go's `map`. +- `make verify` runs `go vet`, `staticcheck`, and the race detector. +- `formal/tla/` exhaustively model-checks the concurrent sorts. +- `formal/` holds machine-checked (Gobra) proofs of the actual source. + +**These checks have already found three latent bugs** that the pre-existing +tests missed (all documented in +[`case-study-bugs-found.md`](case-study-bugs-found.md)): a width-dependent shift +in `hash()`, a zero-seed maximum in `ElementaryPriority`, and a double-length +result in `Sleep`. The last two were caught precisely by the *permutation* +invariant added here — the pre-existing tests only checked ordering. ## Common notation and lemmas @@ -237,7 +244,9 @@ operate on **disjoint** subranges: Given disjointness + the `WaitGroup` join fence, the parallel executions compute the same result as their sequential counterparts, whose correctness is proven above. The **race detector** (`make verify`) corroborates the disjointness claim -dynamically. ∎ +dynamically, and `formal/tla/ParallelSort.tla` model-checks it **exhaustively** +over the whole recursion tree (no two concurrently-writing tasks overlap; the +join always completes). ∎ ## Sleep sort — `sort/sleep.go:9` @@ -253,3 +262,183 @@ termination without deadlock) — is **not** something a paper proof can settle convincingly. It is instead model-checked exhaustively in `formal/tla/SleepSort.tla`, which is the appropriate tool for this coordination logic. See that model and its README for the machine-checked result. + +Separately from the timing/coordination, the *result assembly* must return +exactly the received values. The collector starts from an **empty** slice and +appends each received value, so `perm(out, a₀)` holds and `len(out) = len(a)`. +(This is what the fixed double-length bug violated — see the case study — and +what `TestSleepSort`'s permutation check now guards.) ∎ + +----------------------------------------------------------------------------- + +# Part II — Search / set structures + +Every type in `search/` implements the same `Set[K,V]` interface +(`search/set.go`): a partial map from keys to values with `Put`, `Get`, `Del`, +`Size`, `Empty`. The **contract** each must satisfy — its shared postcondition — +is that it behaves as a finite map: + +- after `Put(k, v)`, `Get(k) = (v, nil)`; +- if `k` was never put (or was deleted), `Get(k) = (0, NotFound)`; +- `Del(k)` removes `k` (subsequent `Get(k) = NotFound`) and returns its value; +- `Size` counts the live keys, `Empty ≡ Size = 0`. + +`search/search_test.go` verifies exactly this contract by running each structure +in lockstep against Go's built-in `map` (an oracle). The proofs below establish +the **structural invariant** that makes each structure meet the contract. + +## GoMap — `search/gomap.go` + +A thin wrapper over Go's built-in `map[K]V`. `Put`/`Get`/`Del`/`Size` delegate +directly to the runtime map, so correctness is inherited from Go's map +semantics. Serves as the reference oracle in spirit. ∎ + +## Elementary (unordered linked list) — `search/elementary.go` + +**Invariant:** the singly-linked list rooted at `s.root` contains exactly one +node per live key, and `s.size` equals the node count. + +- `Put` (`elementary.go:30`): scans; on a key match, overwrites `val` (no size + change — invariant preserved: same key set); on reaching the tail, links a new + node and increments `size`. Loop measure: position advances toward the tail. +- `Get` (`elementary.go:53`): linear scan; returns the value at the matching + node or `NotFound`. Correct by the membership invariant. +- `Del` (`elementary.go:66`): unlinks the matching node (head case via the + deferred `s.root = s.root.next`; interior case by splicing `elem.next`), + decrements `size`. Preserves the one-node-per-key invariant. + +Termination: every loop walks a finite list. Correctness follows because "key is +in the set" ⟺ "a node with that key is in the list". ∎ + +## Hash (separate chaining) — `search/hash.go` + +**Invariant:** key `k` is stored **iff** it appears in the Elementary list at +`buckets[hash(k)]`. + +Because `hash` (`hash.go:28`) is a deterministic total function `K → [0, +capacity)`, `Put`, `Get`, and `Del` all probe the **same** bucket for a given +key, so each reduces to the corresponding Elementary operation *within one +bucket* — already proven correct above. Collisions are resolved by chaining, so +correctness holds for **any** deterministic `hash`; the specific mixing function +affects only the distribution (performance), not correctness. + +Caveat established by the verification harness: `hash` must be *well-defined for +every key width*. The original `key<<10` degenerated to `0` for narrow key types +(fixed to mix in `int64`); this changed distribution, never the contract. See +[`case-study-bugs-found.md`](case-study-bugs-found.md). ∎ + +## BST (unbalanced binary search tree) — `search/bst.go` + +**Invariant (BST order):** for every node `n`, all keys in `n.left` are `< n.key` +and all keys in `n.right` are `> n.key`. + +- `search` (`bst.go:125`) walks the tree by the invariant — left when `key < + n.key`, right when `key > n.key`, match on equality — and returns either the + node or the `**node` slot where a missing key *would* attach. This is correct + by the ordering invariant: if `key` exists it lies on exactly this path. +- `Put` (`bst.go:55`) inserts a new leaf at that empty slot, which by + construction sits in the correct ordered position, preserving the invariant; + an existing key is left unchanged. +- `Del` (`bst.go:83`) does **Hibbard deletion**: leaf → detach; one child → + splice the child up; two children → replace the node with its **successor** + (the minimum of the right subtree, extracted by `deleteMin`), rewiring the + successor's children to `n`'s. The successor is greater than everything in + `n.left` and less than the rest of `n.right`, so BST order is preserved. + +Termination: `search`/`min` descend strictly toward the leaves; the tree height +is finite. No balancing is performed, so height may be `O(n)` — a *performance* +property, not a correctness one. ∎ + +## RedBlackBST (left-leaning red-black tree) — `search/redblackbst.go` + +The LLRB adds balancing on top of BST order. **Invariants:** + +1. **BST order** (as above), on `key`. +2. **Left-leaning:** no right-leaning red link (`isRed(n.right) ⇒ isRed(n.left)` + is disallowed at rest). +3. **No two reds in a row:** a red link's child link is not also red. +4. **Perfect black balance:** every root-to-leaf path crosses the same number of + black links. + +`put` (`redblackbst.go:100`) inserts the new node **red** at the bottom (as in +the BST), then re-establishes the invariants bottom-up on the return path with +three fix-ups (`redblackbst.go:119`): + +- `rotateLeft` when the right child is red and the left is not (repairs a + right-leaning red, invariant 2); +- `rotateRight` when the left child *and* its left child are red (repairs two + reds in a row, invariant 3); +- `flipColors` when both children are red (splits a temporary 4-node, pushing + redness up while preserving invariant 4). + +`Put` (`redblackbst.go:95`) recolours the root black afterwards. These are +exactly Sedgewick's LLRB transformations; each rotation/flip preserves BST order +and black-balance while removing one local violation, so by induction on the +return path the whole tree satisfies invariants 1–4 after every `Put`. The +`capacity` field is maintained as the subtree size (`1 + left.Capacity() + +right.Capacity()`) and correctly transferred by the rotations +(`x.capacity = n.capacity`, then `n` recomputed). The invariants bound the +height at `≤ 2·log₂(n)`, giving logarithmic `Get`/`Put`. + +**Deletion is lazy (tombstoning)** and deliberately *not* the full LLRB delete — +the source notes it is "not fully implemented in lecture." `Del` +(`redblackbst.go:158`) locates the node and sets `deleted = true`, decrements +`size`, and zeroes `val`; `Get` (`redblackbst.go:136`) returns `NotFound` for a +tombstoned node. This satisfies the **Set contract** (a deleted key reads as +absent, `Size` is accurate) but leaves the node in the tree: space is not +reclaimed and balance is unchanged (structure is untouched). Termination: +`get`/`put`/`del` recurse strictly downward. ∎ + +----------------------------------------------------------------------------- + +# Part III — Priority queues + +Both queues implement `PriorityQueue` (`queue/priority.go`) over `int`. The +**contract**: `Insert` adds an element; `Max` returns a current maximum; +`DeleteMax` removes and returns a current maximum; and draining a queue by +repeated `DeleteMax` yields the inserted elements in **non-increasing order** +and returns **exactly the multiset** inserted (completeness). The last part is +the *permutation* invariant now checked by `queue/property_test.go`. + +## ElementaryPriority (unordered slice) — `queue/elementarypriority.go` + +**Invariant:** `q.a` holds exactly the current multiset of elements (in +arbitrary order); `Size = len(q.a)`. + +- `Insert` (`elementarypriority.go:17`) appends — trivially preserves the + invariant. +- `max` (`elementarypriority.go:52`) returns the index and value of a maximum by + a linear scan. **This must seed from an actual element**, `q.a[0]`, not the + zero value of `T`: an all-negative queue has no element `> 0`, so a zero seed + reports a phantom `(0, 0)`. This was the fixed bug — see + [`case-study-bugs-found.md`](case-study-bugs-found.md). +- `DeleteMax` (`elementarypriority.go:26`) removes the max element (shifting the + tail left by one) and returns it — multiset minus one maximum. + +Draining is non-increasing because each step removes *a* current maximum from +the remaining multiset. Completeness holds because `Insert` and `DeleteMax` only +add/remove single elements. Termination: `Size` strictly decreases per +`DeleteMax`. ∎ + +## HeapPriority (binary max-heap) — `queue/heappriority.go` + +A binary heap in `q.a` with index `0` unused, so `a[1]` is the root and node +`k`'s children are `2k`, `2k+1`. **Invariant (heap order):** for every +`2 ≤ k ≤ Size`, `a[k/2] ≥ a[k]` (each parent ≥ its children). It follows that +`a[1]` is a maximum of the whole heap. + +- `Insert` (`heappriority.go:29`) appends the new element at the end and + `swim`s it: while it exceeds its parent, swap upward. **swim invariant:** heap + order holds everywhere except possibly between `k` and its parent; the loop + restores it. Measure: `k` halves toward the root. +- `DeleteMax` (`heappriority.go:42`) returns `a[1]` (a maximum, by the + invariant), moves the last element to the root, truncates, and `sink`s it: + while a child is larger, swap with the **larger** child. **sink invariant:** + heap order holds except possibly between `k` and its children. Measure: `2k` + grows toward `Size`. +- `Max` (`heappriority.go:34`) returns `a[1]` without modification. + +Completeness: `swim`/`sink` mutate only via `Swap` (multiset-preserving, Lemma +S), and `DeleteMax` removes exactly one element; so a full drain returns the +inserted multiset, in non-increasing order. Termination: both `swim` and `sink` +strictly move `k` toward their bound. ∎ diff --git a/formal/README.md b/formal/README.md index f667bdf..1bbb7e0 100644 --- a/formal/README.md +++ b/formal/README.md @@ -1,22 +1,24 @@ -# Gobra deductive proof +# Gobra deductive proofs -`insertion.go` is a **machine-checked** proof that an insertion sort is correct, -verified by [Gobra](https://github.com/viperproject/gobra) — ETH Zurich's -deductive verifier for Go, which translates annotated Go to the Viper -intermediate language and discharges the proof obligations with the Z3 SMT +`insertion.go` and `selection.go` are **machine-checked** proofs that these +sorts are correct, verified by [Gobra](https://github.com/viperproject/gobra) — +ETH Zurich's deductive verifier for Go, which translates annotated Go to the +Viper intermediate language and discharges the proof obligations with the Z3 SMT solver. -Unlike the TLA+ model (which checks a hand-written abstraction) and the property -tests (which sample inputs), this verifies the **actual Go source** for **all** -inputs. Gobra proves two things about `Insertion`: +Unlike the TLA+ models (which check a hand-written abstraction) and the property +tests (which sample inputs), these verify the **actual Go source** for **all** +inputs. Gobra proves two things about each sort: 1. **Memory safety** — every index access is in bounds. The permission invariants `forall k :: 0 <= k < len(a) ==> acc(&a[k])` carry write access to every element through both loops; Go itself cannot prove the absence of index-out-of-range panics, Gobra can. 2. **Ordering** — on return `a` is sorted ascending - (`forall p < q :: a[p] <= a[q]`), established via the two insertion-sort loop - invariants in the annotations. + (`forall p < q :: a[p] <= a[q]`), established via the loop invariants in the + annotations. Selection sort needs the stronger "every prefix element ≤ every + suffix element" invariant; insertion sort uses a "sorted except at the + in-flight index" invariant. The **permutation** half of full correctness (output is a rearrangement of the input) is intentionally left to the property tests and the paper proof in @@ -45,7 +47,8 @@ or directly: ```sh podman run --rm -v "$PWD/formal:/gobra/formal:z" \ - ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go + ghcr.io/viperproject/gobra:latest \ + -i /gobra/formal/insertion.go /gobra/formal/selection.go ``` Expected output ends with: diff --git a/formal/selection.go b/formal/selection.go new file mode 100644 index 0000000..1a9028d --- /dev/null +++ b/formal/selection.go @@ -0,0 +1,48 @@ +package formal + +// Selection sorts a in ascending order, in place. This is a monomorphized +// (non-generic, plain []int, inlined swap, no `continue`) copy of +// sort.Selection, annotated so Gobra proves memory safety AND that the result +// is sorted ascending, for all inputs. +// +// Selection sort's proof needs a stronger outer invariant than insertion sort: +// not only is the prefix a[0..i) sorted, but every element of that prefix is +// <= every element of the unsorted suffix a[i..len). That second invariant is +// what lets the newly selected minimum extend the sorted prefix. +// +//@ requires forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) +//@ ensures forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) +//@ ensures forall p, q int :: 0 <= p && p < q && q < len(a) ==> a[p] <= a[q] +func Selection(a []int) { + i := 0 + //@ invariant 0 <= i && i <= len(a) + //@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) + // a[0..i) is sorted... + //@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q] + // ...and every prefix element is <= every suffix element. + //@ invariant forall p, q int :: 0 <= p && p < i && i <= q && q < len(a) ==> a[p] <= a[q] + for i < len(a) { + min := i + j := i + 1 + //@ invariant i < len(a) && i+1 <= j && j <= len(a) + //@ invariant i <= min && min < len(a) + //@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) + // a[min] is the smallest of the scanned suffix a[i..j). + //@ invariant forall k int :: i <= k && k < j ==> a[min] <= a[k] + // The outer invariants still hold (the inner loop reads only). + //@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q] + //@ invariant forall p, q int :: 0 <= p && p < i && i <= q && q < len(a) ==> a[p] <= a[q] + for j < len(a) { + if a[j] < a[min] { + min = j + } + j = j + 1 + } + if min != i { + tmp := a[i] + a[i] = a[min] + a[min] = tmp + } + i = i + 1 + } +} diff --git a/formal/tla/ParallelSort.cfg b/formal/tla/ParallelSort.cfg new file mode 100644 index 0000000..b60c298 --- /dev/null +++ b/formal/tla/ParallelSort.cfg @@ -0,0 +1,13 @@ +\* TLC configuration for the ParallelSort fork/join model. +\* N=4, Threshold=1 gives a full recursion tree of 7 nodes (root -> 2 -> 4 +\* leaves), enough to exercise siblings, cousins, and multi-level joins. Integer +\* constants can be assigned directly in a .cfg. +CONSTANT N = 4 +CONSTANT Threshold = 1 + +SPECIFICATION Spec + +INVARIANT TypeOK +INVARIANT NoDataRace + +PROPERTY Terminates diff --git a/formal/tla/ParallelSort.tla b/formal/tla/ParallelSort.tla new file mode 100644 index 0000000..c4dee79 --- /dev/null +++ b/formal/tla/ParallelSort.tla @@ -0,0 +1,117 @@ +----------------------------- MODULE ParallelSort ----------------------------- +(***************************************************************************) +(* A TLA+ model of the fork/join structure shared by ParallelMerge *) +(* (sort/parallelmerge.go) and ParallelQuick (sort/parallelquick.go). *) +(* *) +(* Both sorts recursively split an array range into two halves, sort them *) +(* in two goroutines over DISJOINT index sub-ranges, join on a WaitGroup, *) +(* and (for merge) combine. The correctness of the *parallelization* — as *) +(* argued on paper in docs/verification.md — reduces to two claims: *) +(* *) +(* 1. No data race: no two concurrently-writing tasks touch overlapping *) +(* array indices. *) +(* 2. Termination: the join structure always completes (no deadlock). *) +(* *) +(* This model checks both EXHAUSTIVELY over the whole recursion tree. We *) +(* model each task's index range as the resource it writes. A parent only *) +(* writes its full range (the merge step) AFTER both children have joined *) +(* (reached "done"); until then it is "waiting" and writes nothing. This is *) +(* the WaitGroup fence. Remove that fence (let a parent merge while its *) +(* children still run) and TLC finds a data race — see the README. *) +(* *) +(* Modeling the parent's post-join merge as writing the whole [lo,hi) range *) +(* is the *stronger* case (merge sort). Quicksort does no work after the *) +(* join, so if this race-free model holds, quicksort's is race-free too. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + N, \* array length (indices 0..N-1) + Threshold \* ranges of size <= Threshold are sorted sequentially (leaves) + +\* The recursion tree: node id 1 owns [0,N); a non-leaf id owns [lo,hi) and its +\* children 2*id, 2*id+1 own the two halves. Ranges of size <= Threshold are +\* leaves. The set of nodes is finite because ranges strictly shrink. +RECURSIVE TreeFrom(_, _, _) +TreeFrom(id, lo, hi) == + IF hi - lo <= Threshold + THEN { [id |-> id, lo |-> lo, hi |-> hi, leaf |-> TRUE] } + ELSE LET mid == (lo + hi) \div 2 + IN { [id |-> id, lo |-> lo, hi |-> hi, leaf |-> FALSE] } + |