From 169b0c33463c4c8f9c7945f38b00dd6682a2037a Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 3 Nov 2026 17:16:44 -0500 Subject: [PATCH 1/2] chore(tools): let a sabotage entry declare its result hardware-dependent The post-merge sweep of #176 failed on windows-ioring-sys' entry that drops a flush's covering flag: declared to survive from the machine it was written on, it is caught on runners whose device stack does not order the flush by itself, and GitHub runners have given both answers. The engineer's ruling, 2026-11-03: a new expectation. hardware-dependent scores caught and survived alike, puts '-- on this machine; either is declared' on the verdict line so which one a machine gave is kept, and still fails a patch that does not build or a run that never reached the tests. Recorded in DESIGN-NOTES (sabotage-hardware-dependent), with the rule that it is for the machine and not for flaky tests; documented in the README; one case for each side and its edge, the hang in the overrun case, and four harness sabotage entries, all caught. Completed item: M34.26: Add expect: hardware-dependent to the sabotage harness, and declare the RS-C-4 covering-flag entry with it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 2 ++ DESIGN-NOTES.md | 18 ++++++++++++++++++ tools/README-sabotage.md | 15 +++++++++++++-- tools/run-sabotage.ps1 | 26 +++++++++++++++++++++----- tools/sabotage2.json | 32 ++++++++++++++++++++++++++++++++ tools/test-run-sabotage.ps1 | 27 +++++++++++++++++++++++++++ 6 files changed, 113 insertions(+), 7 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 8d05658b..135244ff 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -282,6 +282,8 @@ last learned. The decision and its alternatives are in > **-> UNBLOCKS PARKED WORK:** completing this unblocks `M34.25` in [PARKED.md](PARKED.md#m3425-plus). +- [x] **M34.26** -- Add `expect: hardware-dependent` to the sabotage harness, and declare the RS-C-4 covering-flag entry with it. + ## M37 -- Discharge the failable-call standard across the workspace Numbered M37, not M22. This section arrived from PR #84, which numbered it M22 without knowing diff --git a/DESIGN-NOTES.md b/DESIGN-NOTES.md index 57f9807d..4f635d4e 100644 --- a/DESIGN-NOTES.md +++ b/DESIGN-NOTES.md @@ -3027,6 +3027,24 @@ last learned and not from nothing, which is what a clone's first scoped sweep ot The alternatives and what building it found are in [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#how-the-record-came-to-a-branch). + +**An entry whose result depends on the machine declares `hardware-dependent`.** +The engineer, 2026-11-03, choosing among taking such an entry out of its manifest into documentation, a new +expectation, and leaving it to fail at random. The case was `windows-ioring-sys`' entry that drops a flush's +covering flag: it was declared to survive from the machine it was written on, and GitHub runners have since +both caught it and not, so every full sweep failed or passed on which runner it drew. `expect: +hardware-dependent` scores caught and survived alike and puts `-- on this machine; either is declared` on +the verdict line, so which one a machine gave is kept; a patch that does not build, or a run that never +reached the tests, still fails, since it measured nothing. + +- **It is for the machine, not for flakiness.** An entry whose result varies because the tests are + timing-sensitive, or because the runner was slow, is a defect in the entry or the tests, and + `hardware-dependent` would hide it. The `why` of an entry declaring it says what about the machine + decides the result. +- **Why not documentation alone.** The entry still runs everywhere and still fails a sweep on a patch that + stops compiling; moved into prose, nothing would notice the day the patch stopped applying. + +The work is [CHECKLIST.md](CHECKLIST.md) `M34.26`. ## A `compile_fail` doctest names the error it exists to produce **Every `compile_fail` doctest pins its expected error code -- ```` ```compile_fail,E0502 ```` -- and CI diff --git a/tools/README-sabotage.md b/tools/README-sabotage.md index 3be5916e..fc811a29 100644 --- a/tools/README-sabotage.md +++ b/tools/README-sabotage.md @@ -104,7 +104,7 @@ the field, never a raw PowerShell error: the tool is a diagnostic instrument, so its own failures must not need diagnosing, and must not take a calling script down with them. Missing file, invalid JSON, absent `package` or `sabotages`, an empty `sabotages`, an unresolvable `root`, a missing per-sabotage field, an `expect` that is not -one of `caught`, `survives` and `refused-by-build`, and a `buildError` that is +one of `caught`, `survives`, `refused-by-build` and `hardware-dependent`, and a `buildError` that is missing where it is required or present where it is ignored are each reported this way, as are running from outside a git repository, an `-OutputDirectory` git does not ignore, and a `testArgs` carrying `--target-dir`. @@ -352,6 +352,17 @@ If such an entry's build fails with some *other* error, it is reported as `MANIFEST DOES NOT COMPILE (the build failed, but not with '...')`; if it builds cleanly, the guard did not fire, and the result says `BUILT CLEANLY` first. +**`... -- on this machine; either is declared`** -- the entry declared +`hardware-dependent`, and this is the verdict the tests gave on the machine that +ran them. Both `caught` and `survived` count as declared: the sabotage measures +the device as much as the tests, so one machine catches it and another does not, +and a single `expect` would fail every sweep on whichever machine disagreed. The +line keeps which it was, so two runs can still be compared. Anything that is not a +verdict on the tests -- `MANIFEST DOES NOT COMPILE`, `INFRASTRUCTURE` -- still +fails, since it measured nothing. Use it only where the `why` can say what about +the machine decides the result; an entry whose result is merely unreliable is a +defect in the entry or the tests, not a property of the hardware. + **`MANIFEST DOES NOT COMPILE`** -- the patch is not valid Rust, so the tests never got a chance to notice it. Reported for a build-phase failure and, separately, for `a doctest would not build`: `--no-run` cannot pre-build @@ -535,7 +546,7 @@ Inside each entry of `sabotages`: |---|---|---| | `name` | yes | Unique; also the `-Name` filter key and the transcript filename. Two names that differ only in punctuation are rejected, as is `baseline`. | | `file` | yes | Source to patch, relative to `root`. | -| `expect` | yes | `caught` for a defect the tests must notice, `survives` for a control, `refused-by-build` for a defect a compile-time guard must reject. | +| `expect` | yes | `caught` for a defect the tests must notice, `survives` for a control, `refused-by-build` for a defect a compile-time guard must reject, `hardware-dependent` for one whose result depends on the machine it runs on (either verdict counts, and the line says which). | | `buildError` | with `refused-by-build` only | Literal text the build's error output must contain -- the guard's own message, e.g. `a policy is missing from Policy::ALL`. Required for `refused-by-build` and rejected for anything else. | | `why` | yes | What breaks, and why the suite should or should not notice. This is the part a future reader needs; the patch only says what changed. | | `find` | yes | Lines to replace. Must match **exactly once**. | diff --git a/tools/run-sabotage.ps1 b/tools/run-sabotage.ps1 index 561c9e4e..50dcd82f 100644 --- a/tools/run-sabotage.ps1 +++ b/tools/run-sabotage.ps1 @@ -42,6 +42,14 @@ it -- so a harness with no timeout hangs too, and a lost-wakeup defect that hangs the suite has been detected exactly as intended. + AN ENTRY CAN DECLARE ITS RESULT HARDWARE-DEPENDENT. `expect` is normally + one verdict, but some sabotages measure the machine as much as the tests: a + device that orders a flush behind outstanding writes hides a missing barrier, + and one that does not exposes it. Such an entry declares + `hardware-dependent`, which counts caught and survived alike and reports + which one this machine gave; a patch that does not build, or a run that + never reached the tests, still fails, since neither is a measurement. + THE BASELINE MUST BE GREEN FIRST. Against an already-red suite every sabotage "fails" and the whole sweep means nothing while looking like a clean bill of health. This script refuses to start until the unmodified @@ -1148,14 +1156,14 @@ foreach ($entry in @($spec.sabotages)) { ) -join "`n") 2 } } - if (@('caught', 'survives', 'refused-by-build') -notcontains $entry.expect) { + if (@('caught', 'survives', 'refused-by-build', 'hardware-dependent') -notcontains $entry.expect) { # Checked because an unrecognised value is not inert: `expect` is # compared for equality when scoring, so anything else can never match # and the entry would be reported as misbehaving on every run, whatever # the suite actually did. Exit-WithMessage (@( "The sabotage '$($entry.name)' declares expect = '$($entry.expect)'." - "It must be 'caught', 'survives' or 'refused-by-build'." + "It must be 'caught', 'survives', 'refused-by-build' or 'hardware-dependent'." ) -join "`n") 2 } # `buildError` is what makes a build failure count, so it is required @@ -1866,10 +1874,18 @@ foreach ($sabotage in $selected) { if ($sabotage.expect -eq 'refused-by-build' -and @('passed', 'failed', 'hung') -contains $run.Outcome) { $actual = "BUILT CLEANLY: the guard did not fire; then $actual" } + # A hardware-dependent entry's result is a measurement of the machine it ran + # on, so either verdict on the tests is what it declared; the line says which + # this machine gave. Anything that is not a verdict on the tests -- a patch + # that does not build, a run that never started -- is still a failure. + $hardware = $sabotage.expect -eq 'hardware-dependent' -and @('passed', 'failed', 'hung') -contains $run.Outcome + if ($hardware) { + $actual = "$actual -- on this machine; either is declared" + } $ok = switch ($run.Outcome) { - 'passed' { $sabotage.expect -eq 'survives' } - 'failed' { $sabotage.expect -eq 'caught' } - 'hung' { $sabotage.expect -eq 'caught' } + 'passed' { $sabotage.expect -eq 'survives' -or $hardware } + 'failed' { $sabotage.expect -eq 'caught' -or $hardware } + 'hung' { $sabotage.expect -eq 'caught' -or $hardware } 'build-failed' { $refusedAsNamed } default { $false } } diff --git a/tools/sabotage2.json b/tools/sabotage2.json index 60604825..fff98394 100644 --- a/tools/sabotage2.json +++ b/tools/sabotage2.json @@ -211,6 +211,38 @@ "why": "The two flags choose the entries by different rules, so a run given both would use one and silently ignore the other.", "find": ["if (-not [string]::IsNullOrWhiteSpace($Since) -and -not [string]::IsNullOrWhiteSpace($Diff)) {"], "replace": ["if ($false) {"] + }, + { + "name": "a hardware-dependent entry that is caught is scored as misbehaving", + "file": "tools/run-sabotage.ps1", + "expect": "caught", + "why": "An entry declared hardware-dependent is a measurement: on one machine the tests catch it and on another they do not. Scoring only the survived side would make every machine that catches it a red sweep, which is the failure that prompted the declaration. Added with hardware-dependent, the engineer's ruling of 2026-11-03, for an entry whose result depends on the device it runs on.", + "find": [" 'failed' { $sabotage.expect -eq 'caught' -or $hardware }"], + "replace": [" 'failed' { $sabotage.expect -eq 'caught' }"] + }, + { + "name": "a hardware-dependent entry whose patch does not build is scored as behaving", + "file": "tools/run-sabotage.ps1", + "expect": "caught", + "why": "A patch that does not compile measured nothing, on any machine. Letting hardware-dependent absorb it would turn a broken manifest entry into a permanent green that no sweep ever reports. Added with hardware-dependent, the engineer's ruling of 2026-11-03, for an entry whose result depends on the device it runs on.", + "find": [" 'build-failed' { $refusedAsNamed }"], + "replace": [" 'build-failed' { $refusedAsNamed -or $sabotage.expect -eq 'hardware-dependent' }"] + }, + { + "name": "a hardware-dependent result does not say it was this machine's", + "file": "tools/run-sabotage.ps1", + "expect": "caught", + "why": "The verdict line is where the measurement is kept: without the note it reads as an ordinary caught or survived, and a reader comparing two runs cannot tell a machine difference from a change in the tests. Added with hardware-dependent, the engineer's ruling of 2026-11-03, for an entry whose result depends on the device it runs on.", + "find": [" $actual = \"$actual -- on this machine; either is declared\""], + "replace": [" $actual = \"$actual\""] + }, + { + "name": "hardware-dependent is refused as an unknown expect", + "file": "tools/run-sabotage.ps1", + "expect": "caught", + "why": "The validator holds the list of values scoring understands; one missing from it refuses every manifest that uses it before a single entry runs. Added with hardware-dependent, the engineer's ruling of 2026-11-03, for an entry whose result depends on the device it runs on.", + "find": [" if (@('caught', 'survives', 'refused-by-build', 'hardware-dependent') -notcontains $entry.expect) {"], + "replace": [" if (@('caught', 'survives', 'refused-by-build') -notcontains $entry.expect) {"] } ] } diff --git a/tools/test-run-sabotage.ps1 b/tools/test-run-sabotage.ps1 index 80c3f86f..a4d24c78 100644 --- a/tools/test-run-sabotage.ps1 +++ b/tools/test-run-sabotage.ps1 @@ -1591,6 +1591,8 @@ Test-Case 'a sweep of planned overruns kills what overruns and spares what is gi New-FauxRun 'sleeps past the bound, but its own bound allows it' 'sleep 5 fail' 'caught' 'caught \(suite failed, exit 101\)' ` -Extra @{ timeoutSeconds = 9 } New-FauxRun 'finishes under the bound' 'sleep 1 pass' 'survives' 'survived \(NOT caught\)' + New-FauxRun 'hardware-dependent, and the tests hang' 'hang' 'hardware-dependent' ` + ("caught \(tests HUNG past ${b}s\)" + [regex]::Escape(' -- on this machine; either is declared')) ) $root = New-FauxFixture -Runs $runs try { @@ -1638,6 +1640,31 @@ Test-Case 'a sweep whose runs do not do what their entries declared fails, and n } } +Test-Case 'a hardware-dependent entry behaves as declared caught or survived, says which, and still fails when the tests never ran' { + # Both sides of the declaration, and its edge: a run that survives and one that + # fails are each what it declared, and the line says which this machine gave; a + # patch that does not build is not a measurement of the machine, so it fails as + # it would under any other declaration. The hang is left to the overrun cases, + # where its cost is paid: here it would cost a whole bound. + $either = ' -- on this machine; either is declared' + $runs = @( + New-FauxRun 'the device orders the flush itself' 'pass' 'hardware-dependent' ('survived \(NOT caught\)' + [regex]::Escape($either)) + New-FauxRun 'the device does not' 'fail' 'hardware-dependent' ('caught \(suite failed, exit 101\)' + [regex]::Escape($either)) + New-FauxRun 'the patch does not build' 'build-fail' 'hardware-dependent' 'MANIFEST DOES NOT COMPILE \(tests never ran\)' -Ok $false + ) + $root = New-FauxFixture -Runs $runs + try { + $result = Invoke-FauxSweep -Root $root + Assert-Equal 1 $result.ExitCode $result.Output + Assert-FauxPlanReported -Runs $runs -Output $result.Output + Assert-Match '1 of 3 sabotages did not behave as declared\.' $result.Output + $listed = $result.Output.Substring($result.Output.IndexOf('UNEXPECTED RESULTS')) + Assert-Match '(?m)^\s+the patch does not build\s*$' $listed 'the build failure is listed' + Assert-False ($listed -match 'orders the flush itself|the device does not') 'neither measurement is listed' + } + finally { Remove-Fixture $root } +} + Test-Case 'the same plan gives the same verdicts on every sweep' { # Nothing in a faux run is random, so two sweeps of one plan must agree # line for line, apart from the seconds each took. Overruns are left out From 22124f1ab8689afeb36f3b7b50dd132b9e9d08a5 Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 3 Nov 2026 17:16:45 -0500 Subject: [PATCH 2/2] test(ioring): declare the RS-C-4 covering-flag sabotage hardware-dependent It was declared to survive, and whether it survives depends on whether the device orders a flush behind the file's outstanding writes by itself: GitHub runners have caught it (post-merge sweeps of c714e83b and 13f06742) and not (the nightly of 2026-11-03). It now declares hardware-dependent, its name says what decides the result, and D-65 records it. It survives on the machine this was made on. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- crates/windows-ioring-sys/DESIGN-NOTES.md | 2 +- crates/windows-ioring-sys/sabotage.json | 24 ++++++----------------- 2 files changed, 7 insertions(+), 19 deletions(-) diff --git a/crates/windows-ioring-sys/DESIGN-NOTES.md b/crates/windows-ioring-sys/DESIGN-NOTES.md index 706c7f10..adf803ff 100644 --- a/crates/windows-ioring-sys/DESIGN-NOTES.md +++ b/crates/windows-ioring-sys/DESIGN-NOTES.md @@ -97,7 +97,7 @@ runs a continuation), this crate exposes the mechanism and documents the trade-o | D-62 | **The properties that must hold under every resolution are checked by *asking* [`RingContract`](src/contract.rs), not by restating it -- and the same rule decides where the expected outstanding count comes from.** `M26.4` states five properties over the resolver `M26.3` built: conservation, no hang, `pop_within` honours its bound, `outstanding` is accurate, and no use-after-free. Only two needed anything new. Conservation is already this crate's own oracle, so the harness reports to it and asks it for the verdict, on the rule that the layer owning an invariant owns the oracle for it -- a copy in a harness is a second implementation, and when the two disagree it is the harness that gets "fixed". **The accurate-`outstanding` property follows the same rule rather than counting for itself**: the expected value is read back out of the contract through its own `Outstanding` violation, because a counter in the harness would be a third party to the disagreement. **"No hang" is a step budget**, since a resolver answers instantly and a hang here is therefore an unterminating loop rather than a block. **Two weaknesses are declared rather than papered over.** `pop_within`'s upper bound is nearly free under an ordinary resolution -- the resolver rarely makes it approach its deadline -- so the non-vacuous case uses a separate degenerate responder in which nothing completes during the window; that is not an `RS-C-1` violation, because no finite observation can distinguish "eventually" from "never", but the prefix of a satisfying resolution in which the eventually has not happened yet. And **no-use-after-free covers this crate's memory handling, not the kernel's**, since under a resolver nothing external ever writes into a buffer; the kernel-side half stays with [generated_sequences.rs](tests/generated_sequences.rs) against a real ring. **Coverage counters are asserted, not printed**: all five properties are satisfied trivially by a run that does nothing, so a vacuity guard is what separates "the properties held" from "nothing reached the states they are about". | | D-63 | **The resolver is calibrated against two defects that really happened, and the two suites' sensitivities were measured rather than assumed -- they differ, and the difference is the reason the calibration is its own file.** [D-41](#d-41)'s corollary is the rule: a green result from an instrument nobody has shown can go red is not evidence, and this repository has already produced one instrument of exactly that shape -- `M17.4` reverted issue #47 as it shipped and the generated suite reported **green**, because it sampled the right state while draining by a poll that recovers completions whether the ring signalled or not. **The two defects are calibrated differently because they live in different places.** `M21.6`'s -- an expired wait treated as a failure -- was in this crate, so it is re-injected by [sabotage.json](sabotage.json) and swept; what [calibration.rs](tests/calibration.rs) adds is the precondition that makes that sabotage mean anything, namely that `RS-P-4` reaches `pop_within` at all. [D-47](#d-47)'s is in a **consumer**, so there is nothing to mutate and the defective consumer is written out: a believer in the hold-back `D-24` claimed and `D-47` withdrew, which the resolver must break. **Measured, and the two suites are not equivalent.** `M21.6`'s defect is caught by both the calibration and `M26.4`'s property suite -- the latter only because that suite distinguishes a declined submit from a genuine error, which makes the detection deliberate rather than lucky. A *narrowed* resolver -- one enforcing the hold-back -- is caught by the calibration alone, and the property suite correctly stays green, because a narrower resolution is still a valid one and conservation still holds under it. **That is why a calibration file exists rather than a calibration assertion inside the property suite**: only a test that demands sensitivity can detect an instrument going blind, and such a test fails when the *instrument* regresses rather than when the crate does. | | D-64 | **The standard seeded-sweep size is 2048, and a coverage threshold must be stated against the space a test can reach rather than against the sweep size.** The sweeps were widened from 64 (and the property suite's 240 plans) for breadth, on the measurement that seed count is not what these suites cost: a seed is tens of microseconds -- a whole ring, a batch, a drain and a rundown -- so the resolver's 22 unit tests sweep 2048 seeds each inside a lib suite that runs in well under a tenth of a second, far inside this repository's sub-second budget for a submodule. Only [properties_under_every_resolution.rs](tests/properties_under_every_resolution.rs) moved materially, to a little over a second, and even there roughly an eighth of the original cost was a deliberate sleep in the bound test rather than the plans. **The trap the widening exposed is the part worth keeping.** `different_seeds_reach_different_resolutions` asserted that distinct completion orders exceeded *half the seed count*, which is satisfiable only while the seeds are fewer than the outcomes: six operations admit `6! = 720` orders, so that threshold becomes arithmetically impossible past 1440 seeds and the test would have failed with nothing regressed. Thresholds of that kind are now phrased against the achievable space. **Saturation was measured rather than assumed**, because the obvious response -- cap the sweep where it stops gaining -- turned out not to apply: over the resolver's own mixer, 1024 seeds reach 539 of the 720 orders and 2048 reach 670, so the sweep is still gaining breadth at its current size and only around 8192 exhausts the space. **The property suite's vacuity guards are fractions of the plan count** for the same reason in reverse: an absolute floor chosen for 240 plans is a twelvefold margin at 2048, which would let the suite lose most of its work without complaint. Each is set near half the minimum observed over repeated runs, since that file's seeds are clock-derived and its counts therefore vary; the fixed-seed suites are deterministic and need no such margin. | -| D-65 | **The kernel tests' job is confirming a real Windows stays *inside* the specified space, and that division of labour is enforced by a census that reads markers rather than mentions.** `M26` split one job in two: the resolver sweeps the permissions (`RS-P-n`), and tests against a real ring confirm the constraints (`RS-C-n`). The split is load-bearing for exactly one clause -- `RS-C-4`, which the resolver is forbidden to violate, so a Windows that broke the drain would be caught by nothing the resolver does. **A hole was found where that mattered most**: [flush_barrier.rs](tests/flush_barrier.rs) asserted the clause but sat behind an early return taken when its control could not discriminate, so on such a machine the constraint was untested on both sides at once. The fix separates two questions that one gate had been answering together -- *is the barrier doing work*, a comparative claim that genuinely needs the control, and *did the kernel stay inside `RS-C-4`*, a conformance question where skipping can only hide a violation. The conformance assertion now runs on every machine and only the comparative claim is withheld. **The census was green and useless on its first build, and trying to make it go red is what found that.** It searched each file for the clause ID anywhere in its text; removing `RS-C-4`'s check from the only test performing it did not turn it red, because a second file mentioned the clause only to *disclaim* it -- and under a substring search a disclaimer is indistinguishable from a claim. This is the same trap already recorded for a probe whose only mention of a tag was a comment. A claim is now a structured `CONFIRMS:` / `EXERCISES:` marker naming a clause and nothing else, verified to go red in three directions. **Two blind spots are declared rather than hidden**: a census over source proves a clause is *claimed*, never that the file's assertion still runs or still means anything; and dropping the covering flag does **not** fire the `RS-C-4` assertion on every machine, because a device stack that orders a flush behind its file's outstanding writes by itself produces no violation to see -- so that sabotage is a portable demonstration of nothing, and the assertion's conformance value (reporting a violation if one occurs) is separate from its sensitivity (proving it would notice). **The toolkit's "five techniques" framing becomes six**, and the sixth is different in kind: the other five check this crate against its own stated contract and cannot tell you that contract is wrong, whereas the resolver checks it against a written specification of what the platform may do, and the kernel tests check the platform against that same specification. | +| D-65 | **The kernel tests' job is confirming a real Windows stays *inside* the specified space, and that division of labour is enforced by a census that reads markers rather than mentions.** `M26` split one job in two: the resolver sweeps the permissions (`RS-P-n`), and tests against a real ring confirm the constraints (`RS-C-n`). The split is load-bearing for exactly one clause -- `RS-C-4`, which the resolver is forbidden to violate, so a Windows that broke the drain would be caught by nothing the resolver does. **A hole was found where that mattered most**: [flush_barrier.rs](tests/flush_barrier.rs) asserted the clause but sat behind an early return taken when its control could not discriminate, so on such a machine the constraint was untested on both sides at once. The fix separates two questions that one gate had been answering together -- *is the barrier doing work*, a comparative claim that genuinely needs the control, and *did the kernel stay inside `RS-C-4`*, a conformance question where skipping can only hide a violation. The conformance assertion now runs on every machine and only the comparative claim is withheld. **The census was green and useless on its first build, and trying to make it go red is what found that.** It searched each file for the clause ID anywhere in its text; removing `RS-C-4`'s check from the only test performing it did not turn it red, because a second file mentioned the clause only to *disclaim* it -- and under a substring search a disclaimer is indistinguishable from a claim. This is the same trap already recorded for a probe whose only mention of a tag was a comment. A claim is now a structured `CONFIRMS:` / `EXERCISES:` marker naming a clause and nothing else, verified to go red in three directions. **Two blind spots are declared rather than hidden**: a census over source proves a clause is *claimed*, never that the file's assertion still runs or still means anything; and dropping the covering flag does **not** fire the `RS-C-4` assertion on every machine, because a device stack that orders a flush behind its file's outstanding writes by itself produces no violation to see -- so that sabotage is a portable demonstration of nothing, and the assertion's conformance value (reporting a violation if one occurs) is separate from its sensitivity (proving it would notice). It was first declared to survive, from the machine it was written on; GitHub runners have since both caught it and not, so its entry declares `hardware-dependent` (the engineer, 2026-11-03), which counts either verdict and records which one each machine gave. **The toolkit's "five techniques" framing becomes six**, and the sixth is different in kind: the other five check this crate against its own stated contract and cannot tell you that contract is wrong, whereas the resolver checks it against a written specification of what the platform may do, and the kernel tests check the platform against that same specification. | | D-66 | **The suite's frozen observations were one class, it was 31 assertions wide, and the restatement is guarded by a source census because no run objects to it.** `M26.7` audited the suite for assertions that pin the platform's incidental behaviour rather than this crate's contract -- the shape [D-52](#d-52) demonstrated, where one assertion gave *opposite answers on two handles of the same API*. **The census came from a command**, as the item required, and the answer was not the file anyone guessed: 31 sites across five kernel tests read `try_pop()` straight after `submit_and_wait` and unwrapped the `Option`, asserting the kernel had **already** queued the completion. `pop_within`'s own documentation denies that in this crate's words -- a submit-side wait's return "promises nothing about poppability" -- and [RESPONSE-SPACE.md](RESPONSE-SPACE.md) states it as `RS-P-5`. They passed for the reason [D-40](#d-40) measured: a buffered read completes inside the submit in 80 of 80 attempts, while an unbuffered one genuinely pends. **The restatement is the one `D-52` prescribed** -- ask for the completion within a bound this crate chooses, which holds on every handle -- and it also removed an unbounded `try_pop` spin found in the same sweep. **Nothing catches a regression by running**, which is the part worth keeping: reverting a site leaves its test green on any machine where the observation is true, so the guard is a census that refuses the shape at the source, plus a resolver-driven test that makes the pending case reachable on demand and shows `try_pop` failing where `pop_within` succeeds. **A second, narrower class was found and deliberately not settled**: five assertions require a complete transfer, which the space lists as *deliberately undecided* and `Completion::result` never promises. That is a specification gap the suite silently answers, queued as `M26.10` rather than decided here, since the space's own instruction is to decide it before a resolver relies on either answer. One of the five is already in the honest form -- [flush_barrier.rs](tests/flush_barrier.rs) checks the transfer as its own precondition and says so -- and is left alone. | | D-67 | **This crate does not implement retry policy. It supplies bounded primitives and reports what the platform documented, and the caller owns backoff, attempt counts and when to give up.** `M26.8` began as "what should `run_down` do when its submit is refused" and was settled by reading `SubmitIoRing`'s reference page rather than by measuring, which is the correction worth keeping: **no amount of measurement constitutes a contract.** The documentation gives a return-value row for `IORING_E_WAIT_TIMEOUT` -- *"All operations were submitted without error and the subsequent wait timed out"* -- and Remarks stating *"If this function returns an error other than IORING_E_WAIT_TIMEOUT, then all entries remain in the submission queue"*, plus that a per-entry failure arrives as a completion rather than as a submit failure. Three things follow. **`Batch::submit_and_wait` had `M21.6`'s defect** at the one site that sweep did not reach: `do_submit` passed a timed-out wait to `check`, reporting a fully successful submission as an error -- and because any *other* error means the entries are still queued, an `Err` was ambiguous between "your buffers are free" and "the kernel still owns them", which is [D-5](#d-5)'s hazard with the sign hidden. **[`IoRing::run_down`](src/ring.rs) was the only waiting API in this crate shaped wrongly**: it waited in 50 ms segments with no period to sit inside, which made "how long to keep trying" this crate's policy rather than its caller's. [`IoRing::run_down_within`](src/ring.rs) is the primitive -- the caller supplies the bound, `Ok(true)` means safe to drop, `Ok(false)` means call again -- and `run_down` is now that with an unbounded period, which is a choice a caller makes by calling it. Note the contrast that makes this precise: [`IoRing::pop_within`](src/ring.rs) also waits in segments and is *correct*, because its segments sit inside a deadline the caller supplied. **An error from rundown is not terminal and says so**: the entries remain queued, the ring is resumable, and the one thing a caller must not do is drop it. **`RS-P-7` and `RS-P-3` moved from inference to citation** -- `M26.1` had written `RS-P-7` as a consequence clause with no authority for submits failing at all, and `M26.3`'s resolver had read it as a permission anyway; the space now carries a `Documented` tag that outranks `Observed`, because a measurement describes one run of one build. | | D-68 | **A thread-pool wait must be armed before the event it watches is signalled, so the ring's completion event is attached unsignalled and the setup signal is raised after arming.** **One clause corrected by [D-77](#d-77) -- the mechanism offered for the rule, not the rule. And this ordering did not cure the stall it was written for -- M26.13 reproduced it against this build -- so the ordering is retained on documentary grounds rather than as a demonstrated cure. The stall was later closed by the draining teardown, [Teardown drains rather than cancels](../../DESIGN-NOTES.md#teardown-drains); see the 2026-10-01 "closed by the draining teardown" entry in [RESOLVED-TEST-FAILURES.md](RESOLVED-TEST-FAILURES.md).** `M26.9`'s intermittent stall was settled the same way [D-67](#d-67) was -- by reading the reference page rather than by measuring. `SetThreadpoolWait`'s Remarks state *"You must re-register the event with the wait object before signaling it each time to trigger the wait callback."* [`IoRing::completion_event`](src/ring.rs) raises its deliberate setup signal as it attaches, and `EventDelivery::new` then built a `ThreadpoolWait` around the returned duplicate and armed it -- signal first, register second, which is the order the sentence forbids. **Three properties compounded to make a dropped signal permanent rather than late.** The event is auto-reset ([D-21](#d-21)), so a signal is consumed rather than left pending for a later arming to observe. It is edge-triggered on the completion queue going empty to non-empty ([D-19](#d-19)), so a ring whose queue is already non-empty is signalled by nothing else. And the setup signal exists precisely to serve the already-non-empty case, so it is the only wakeup such a ring will ever get. The fix separates the two steps: `attach_completion_event_unsignalled` attaches and reports whether the signal is still owed, `raise_setup_signal` raises it, and `EventDelivery::new` arms in between; `completion_event` is the two composed, unchanged, for a caller doing its own waiting. **The ordering was the defect, so [D-21](#d-21) stands.** A manual-reset event would also have survived the wrong order, by not consuming the signal, but that trades the arming rule for a reset the drain has to get right, and nothing measured here argued for reopening a decision whose own rationale is about the drain. **Measured before and after** on the reproducer recorded in [RESOLVED-TEST-FAILURES.md](RESOLVED-TEST-FAILURES.md): 5 failures in 600 and 2 in 600 for the two co-running triggers, against 0 in 3600 after. The rule itself is now stated where a caller meets it -- on `ThreadpoolWait::arm` and `WaitActivation::rearm` in [windows-threadpool-sys](../windows-threadpool-sys/src/wait.rs), on `IoRing::completion_event` with a worked remedy for a caller who holds the handle, and on `EventDelivery::new` -- because every other arming site in this workspace already had the order right, so what was missing was the statement rather than the practice. | diff --git a/crates/windows-ioring-sys/sabotage.json b/crates/windows-ioring-sys/sabotage.json index 832e2338..041579e8 100644 --- a/crates/windows-ioring-sys/sabotage.json +++ b/crates/windows-ioring-sys/sabotage.json @@ -726,25 +726,13 @@ ] }, { - "name": "DECLARED BLIND SPOT: dropping the covering flag does not fire RS-C-4 on this machine", + "name": "HARDWARE-DEPENDENT: dropping the covering flag fires RS-C-4 only where the device does not order the flush", "file": "tests/flush_barrier.rs", - "expect": "survives", - "why": "A hardware-dependent limit on the conformance assertion's SENSITIVITY, measured rather than assumed. Running the treatment case with FlushCoverage::Unordered removes the barrier entirely, and on a machine where the device stack orders a flush behind that file's outstanding writes by itself -- which this file's own header documents, and which is the case here -- no preceding write completes after the flush even unflagged, so the assertion stays green. It is therefore NOT a portable demonstration that the assertion can go red: on the spike's machine it would be caught, on this one it survives. Recorded because a reader would otherwise reasonably expect this to be the calibration for RS-C-4, and it cannot be. What the assertion still does everywhere is report a violation if one occurs, which is the conformance job; what it cannot do everywhere is prove it would notice.", - "testArgs": [ - "test", - "-p", - "windows-ioring-sys", - "--locked", - "--all-features", - "--test", - "flush_barrier" - ], - "find": [ - " let covering = run_case(&mut ring, handle, FlushCoverage::CoversPrecedingOperations);" - ], - "replace": [ - " let covering = run_case(&mut ring, handle, FlushCoverage::Unordered);" - ] + "expect": "hardware-dependent", + "why": "A hardware-dependent limit on the conformance assertion's SENSITIVITY, measured rather than assumed. Running the treatment case with FlushCoverage::Unordered removes the barrier entirely. On a machine whose device stack orders a flush behind that file's outstanding writes by itself -- which this file's own header documents -- no preceding write completes after the flush even unflagged, so the assertion stays green and the entry survives; on one whose stack does not, the assertion fires and it is caught. It was declared survives from the machine it was written on, and GitHub runners have since given both answers: survived in the nightly sweep of 2026-11-03 (run 41595881867), caught in the post-merge sweeps of c714e83b (run 41569818547) and 13f06742 (run 41714398521). So it is declared hardware-dependent (D-65), and each sweep's line records which this machine gave. It is NOT a portable demonstration that the assertion can go red. What the assertion still does everywhere is report a violation if one occurs, which is the conformance job; what it cannot do everywhere is prove it would notice.", + "testArgs": ["test", "-p", "windows-ioring-sys", "--locked", "--all-features", "--test", "flush_barrier"], + "find": [" let covering = run_case(&mut ring, handle, FlushCoverage::CoversPrecedingOperations);"], + "replace": [" let covering = run_case(&mut ring, handle, FlushCoverage::Unordered);"] }, { "name": "M26.7: a kernel test goes back to asserting a completion is already poppable",