Queue M30: survey how much algorithm correctness can be machine-checked

CHECKLIST.md

@@ -185,6 +185,105 @@ written before it was stated.
   function pointer, which is exactly where such a path would be. Depends on M22.1's
   classification.
 
+## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked
+
+Rationale: [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued).
+
+- [ ] **M30.1** -- Survey the workspace for algorithms whose correctness is currently argued rather
+  than checked, and match each to the class of tool that could check it.
+
+  Candidates, not exhaustive: `reserving_mpsc`'s packed claim word and its reservation admission rule;
+  `slotwise_mpsc`'s per-slot sequence protocol; the experimental permit claim; the doorbell's mirror
+  flag against `SetEvent`/`ResetEvent`; `windows-file-watcher`'s contract state machine;
+  `windows-ioring-sys`' submission/completion ring.
+
+  Tool classes to match against: TLA+/PlusCal, loom, a bounded proof such as kani, and `const`
+  assertions. What each can and cannot see is in the rationale.
+
+  Done when: a table exists with one row per algorithm, each naming a tool class or "none fits" and
+  why. The "none fits" rows count as output, not as gaps in the survey.
+
+- [ ] **M30.2** -- Pilot exactly one: `reserving_mpsc`'s claim-position recurrence (`SH-14.1`).
+
+  **`SH-14.1` is a live defect in the shipping protocol, not a hypothetical**, and that inverts the
+  usual shape of a success criterion. A faithful model of the shipping claim protocol, at a position
+  width small enough to wrap, *must* find it. A green run on that model is therefore evidence the
+  model is **unfaithful**, not evidence the protocol is sound.
+
+  Done when all three hold:
+
+  1. **The refinement is stated.** Which constants were shrunk, why the protocol is uniform in each,
+     and what a counterexample at the reduced width implies at the shipping width. If it cannot be
+     argued, the result is reported as a counterexample *in a toy model* and nothing more.
+  2. **Faithfulness: the model of the shipping protocol reproduces `SH-14.1`.** Configured so the
+     wrap is reachable and a producer can stall across it, it must yield the known counterexample --
+     a claim succeeding against a numerically identical but generations-later position. A model that
+     cannot produce a defect the crate already documents is not modelling this protocol.
+  3. **Anti-vacuity: the same model satisfies its invariant where no violation is possible.**
+     Configured so the wrap is unreachable -- total pushes bounded below it, or a single producer,
+     which has no race to lose -- it must come back green. A model that reports a violation there is
+     over-permissive, and its counterexample in (2) proved nothing.
+
+  Not a candidate: `capacity == 1`, which belongs to `slotwise_mpsc`
+  ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)) and is already resolved.
+
+- [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. This is the item the milestone
+  exists for.
+
+  Done when both hold:
+
+  1. **The list names only what the *selected* tool cannot model**, not what tools in general cannot.
+     Expect the syscall boundary -- including the doorbell's `SetEvent`/`ResetEvent` -- real-time
+     behaviour, and the model-to-code
+     gap that no tool closes. Do **not** preclassify scheduler-dependence: loom explores scheduler
+     interleavings deliberately, so recording it as unreachable would be a false gap. Whether the
+     memory orderings are reachable likewise depends on which tool M30.1 selected.
+  2. **Both copies of the disclosure are updated** -- the "How far the memory orderings are verified,
+     and how far they are not" section exists in
+     [that crate's README.md](crates/windows-waitable-queues/README.md) and
+     [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs). Deriving one from the other is not
+     available today: the `include_str!` there is `#[cfg(all(doctest, windows))]` on a private item,
+     so it compiles the README's code as doctests and does not render its prose. Making one derive
+     would mean a shared fragment both include, which is separate work.
+
+- [ ] **M30.4** -- Re-home `M31.6`, which is currently orphaned.
+
+  Done when all three hold:
+
+  1. **It has a live item in a live checklist**, scoped as
+     [D-29](crates/windows-waitable-queues/DESIGN-NOTES.md#d-29) requires -- the loom verification
+     covers both MPSC shapes or neither is verified. (D-29 owns that obligation;
+     [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) owns only the release timing, that
+     verification gates 1.0 rather than 0.1.0.)
+  2. **All five references point at it.** Three in
+     [that crate's DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md), one in
+     [src/doorbell.rs](crates/windows-waitable-queues/src/doorbell.rs), one in
+     [sabotage.json](crates/windows-waitable-queues/sabotage.json).
+  3. **The component tracker row stays accurate** as the work proceeds. The row itself was added
+     when the work was queued, not deferred to this item.
+
+- [ ] **M30.5** -- Decide what, if anything, the workspace adopts, and record the decision with its
+  cost.
+
+  Done when all three hold:
+
+  1. **The cost is stated, not implied.** What running it costs in wall-clock and in whose time,
+     what tooling it adds and who maintains that, and the standing cost the workspace already knows
+     it pays here -- a specification is a second statement of the contract and can drift from the
+     code with nothing to detect it, so a stale model that still passes is worse than no model. An
+     adoption recorded without its cost is the half of this item that is easiest to skip and the
+     half the milestone exists to surface.
+  2. **The decision answers three questions**: what keeps the model and the code in step, who
+     re-runs it, and what happens when they disagree. "Adopt nothing, and say why" is a legitimate
+     outcome.
+  3. **The contract sweep is done, whichever way it went.** Three public places in
+     `windows-waitable-queues` promise machine-checked verification before 1.0:
+     [that crate's README.md](crates/windows-waitable-queues/README.md),
+     [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and
+     [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). A no-adoption outcome obliges this
+     most: left unswept it would recreate, in the same crate, the orphaned commitment M30.4 exists
+     to fix.
+
 ## M-inf -- Parked
 
 Ungated work with no identified predecessor deliverable.

DESIGN-RATIONALE.md

@@ -447,3 +447,130 @@ prose-reduction pass is adopted, each needs its own item at that time.
 - [`SubmitThreadpoolWork`](https://learn.microsoft.com/windows/win32/api/threadpoolapiset/nf-threadpoolapiset-submitthreadpoolwork)
 - [WIL token helpers](https://github.com/microsoft/wil/blob/master/include/wil/token_helpers.h)
 - [`GetFileInformationByHandleEx`](https://learn.microsoft.com/windows/win32/api/fileapi/nf-fileapi-getfileinformationbyhandleex)
+
+## <a id="machine-checking-what-is-argued"></a>Why M30 exists, what it is not, and how the pilot was chosen
+
+Rationale for [CHECKLIST.md](CHECKLIST.md) -> `M30`. It is here, in Tier 2, rather than in
+[DESIGN-NOTES.md](DESIGN-NOTES.md), because **no decision has been taken**: `M30.5` is what produces
+one, and "adopt nothing, and say why" remains a legitimate result. Tier 1 records current decisions,
+and recording pre-decision context there would let a reader mistake it for an adopted contract.
+
+### What checks this workspace's concurrency today
+
+Reasoning recorded beside the code, an extensive unit suite, a sabotage suite that injects defects
+and requires each to be caught, and a cargo-mutants sweep. That combination is not weak, and it has
+found real bugs -- [D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup among
+them.
+
+### The measured blind spot, which is the reason for the milestone
+
+[crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that
+weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite
+green, while every *logic* defect injected beside it was caught. That asymmetry is not a gap in the
+suite's thoroughness; it is what a test is. A test observes what a run happened to do, and cannot
+observe an ordering that a run happened not to need.
+
+The general form is worth keeping in view when reading the survey's results: classes with an oracle
+converge, classes without one do not. Memory ordering has no oracle here.
+
+### The goal is to narrow where hand-inspection has to look, not to replace it
+
+A method that proves a protocol correct for three producers and a capacity of two does not prove the
+shipping code correct. What it does is move a class of question out of "argued carefully" and into
+"checked", so that what remains uncheckable is a short, named list rather than the whole surface.
+**That list is the deliverable**, which is why `M30.3` is the item the milestone exists for rather
+than a tidying step after the pilot. Formal methods here are a scoping instrument.
+
+### The tool classes, and what each can and cannot see
+
+- **TLA+/PlusCal** -- protocol-level, exhaustive over a small configuration. It has **no built-in
+  hardware memory model**, and its ordinary interleaved-action semantics is sequential consistency,
+  so by default it cannot see a weakened ordering. That is a property of the default model rather
+  than an absolute limit: a specification *can* model weak-memory reordering explicitly, with store
+  buffers or a reordering relation written into the spec. What it still checks in that case is the
+  protocol as written, not the orderings the Rust implementation actually emits -- so the
+  model-to-code gap remains, and `M30.1` should record which of the two is meant rather than
+  treating "no memory model" as settled.
+- **loom** -- an instrumented code-level model. It runs the crate's own logic, but the
+  synchronization primitives must be substituted for `loom`'s instrumented types, and loom then
+  explores the executions the C11 model permits. That is much closer to the code than a protocol
+  spec, and it is where the measured weakened-`Acquire` blind spot lives -- but it is still a model:
+  what runs under loom is not the shipping binary, and the Windows calls are not executed as
+  written. An earlier version of this line called it "actual Rust under the C11 memory model", which
+  overstated the guarantee and blurred exactly the model-to-code gap `M30.2` and `M30.3` exist to
+  record.
+- **kani or similar bounded proof** -- Rust, memory-safety and assertion checking.
+- **`const` assertions** -- arithmetic relationships between constants. Already used here, and the
+  cheapest of the four, because they fail the build rather than a run somebody chose to make.
+
+### Why `SH-14.1` is the pilot, and why the reason is not the count
+
+Reaching the claim position's wrap takes 2^32 pushes -- about 37 seconds of sustained maximum-rate
+pushing on the host the queue crate publishes. That is far outside a unit suite budgeted in
+milliseconds, but it is not in itself beyond a long integration test, so "beyond any test" would
+overstate it.
+
+What is beyond any test is the rest of the condition. The crate's README records that reaching the
+wrap is necessary but *not sufficient*: a producer must also be stalled inside a window a few
+instructions wide, and no test can schedule that deliberately. A model whose position wraps at 8
+makes the whole interleaving reachable in seconds and **exhaustive** rather than sampled, and yields
+a counterexample trace rather than a suspicion. Parameter shrinking earns its place by making the
+interleaving exhaustive, not by making a count small.
+
+`capacity == 1` was offered as a second candidate in an early draft and is not one. It belongs to
+`slotwise_mpsc`'s slot *sequence* protocol
+([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)), not to `reserving_mpsc`'s claim
+position, and is already resolved by that shape refusing a capacity below two.
+
+### This must not pre-empt D-31
+
+[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) decided on considered grounds that 0.1.0
+ships without machine-checked orderings. Its reasoning is the starting point rather than something to
+overturn, and its central objection survives any tool choice: **no candidate models the real
+`SetEvent`/`ResetEvent` calls**, so stubbing them verifies a model of `SetEvent` rather than
+`SetEvent` itself. That is the "measures the model, not the thing" trap this workspace has already
+been caught by once, and the doorbell is precisely where its one real ordering bug lived.
+
+An earlier version of this section said the objection was that "a model checker covers atomics and
+cannot cover `SetEvent`" -- which is wrong for TLA+, whose ordinary interleaved-action semantics is
+sequentially consistent and which has no *built-in* memory model to cover atomics with (a spec can
+model reordering explicitly, but then it checks the modelled protocol rather than the emitted code).
+The tool-independent part of D-31's objection is only the syscall boundary; how much of the atomics
+a tool sees is exactly what `M30.1` is for.
+
+### The same trap has a second costume
+
+Shrinking a model's parameters -- a position that wraps at 8 rather than 2^32 -- is itself a claim:
+that the protocol's correctness does not depend on the width of that field. If nobody states why the
+shipping code refines the reduced model, a green run proves something about the model alone. A
+reduced model that has not been tied to the code can pass and mean nothing. `M30.2` carries that as
+an acceptance criterion.
+
+### Two corrections the milestone's own drafting needed
+
+Both were errors in the argument *for* the pilot rather than in the plan, so a reader taking them on
+trust would have aimed the pilot wrongly.
+
+**The untestability was mis-attributed to the count.** The first draft said `SH-14.1` "needs 2^32
+pushes to manifest and is therefore beyond any test". Corrected above: the count is reachable, and
+the stall window is what is not.
+
+**The success criterion went wrong twice, and the second error was the instructive one.** The first
+draft asked for a counterexample from a deliberately broken variant and explicitly *not* a green run
+on the correct one -- an overcorrection against vacuous green runs, since a counterexample from a
+broken variant can equally be produced by a malformed or over-permissive model that would find one
+anywhere. The fix was to require both: property check and anti-vacuity check.
+
+That fix was wrong for this particular pilot, and the reason is worth keeping. **`SH-14.1` is a live
+defect in the shipping protocol**, documented in the crate and disclosed to adopters. So a faithful
+model of the shipping claim protocol, at a position width small enough to wrap, *must* find it --
+and "the unmodified model satisfies its invariant" could only be satisfied by a model that does not
+reproduce a defect the crate ships. The criterion was inverted: it would have been failed by a
+correct model and passed by a broken one.
+
+The general form: **when the system being modelled has a known defect, a green run on the unmodified
+model is a failure signal, not a success.** The two checks still exist, but they attach to different
+configurations rather than to modified and unmodified code -- the model must reproduce the defect
+where the wrap is reachable, and must come back green where it is not (total pushes bounded below
+the wrap, or a single producer, which has no race to lose). `M30.2` carries that as its criteria 2
+and 3.