1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
// Copyright (c) 2026 Mike Grier
//! [`RingContract`](crate::contract::RingContract) -- this crate's conservation
//! rules, made executable.
//!
//! # Why an oracle rather than more assertions
//!
//! Some of what this crate promises is a property of a *sequence*, not of any
//! single value or call, and a per-value type cannot carry it. "Every SQE that
//! successfully queues produces exactly one completion" is only observable by
//! counting pushes against completions across a whole run, and so is "no
//! registered buffer is still in use once everything has finished".
//!
//! Those rules are stated in `DESIGN-NOTES.md` and, before this module, were
//! checked nowhere. That was not a hypothetical gap: two real defects in this
//! repository were conservation failures. `Appender::claim` returned early on
//! a failed write and permanently leaked the arena slot its token held, and a
//! strategy harness shared one deferred-commit slot between two lanes so half
//! its commits were never awaited. Both were found by review and by
//! measurement respectively, and both would have fallen out of a quiescence
//! check automatically. (The first was a token leak, and the rule that caught
//! that kind of leak retired with the token API -- see below.)
//!
//! # Why it lives here
//!
//! The layer that owns an invariant owns the oracle for it. A copy written in
//! a test harness is a second implementation of the rule rather than a check
//! of it -- if the two disagree, the harness is what gets "fixed", and the
//! disagreement is precisely the bug worth finding. Being public means a
//! consumer can hold its own harness, its own test doubles, or a captured run
//! to the same definition this crate's tests use.
//!
//! # What it checks
//!
//! | Rule | Where it comes from |
//! |---|---|
//! | Every queued SQE produces exactly one completion | [`DESIGN-NOTES.md`'s category-2 audit](../DESIGN-NOTES.md#one-sqe-one-completion) |
//! | A push that failed synchronously produces none | the same section: it is un-counted, not merely uncompleted |
//! | No completion arrives for an operation never pushed | corollary of the above |
//! | Nothing is outstanding at quiescence | what `IoRing::run_down`'s termination depends on |
//!
//! Every rule here is about the **kernel**, not about a caller's bookkeeping.
//! A fifth row used to sit above -- "every token is claimed, or deliberately
//! leaked" -- and it retired with the token API: a push now hands back only an
//! `OperationId`, which owns nothing, so there is nothing a caller could fail
//! to claim. [D-74](../DESIGN-NOTES.md#d-74) records why that is a retirement
//! rather than a narrowing.
//!
//! What replaced it is **not** `held() == outstanding()`. Those two are not
//! equal in general and the ring does not compare them: a `_raw` flush or
//! cancel is outstanding while deliberately stowing no inventory
//! entry, so a perfectly valid push makes them differ. Reading equality as an
//! invariant would report that valid push as a conservation failure, which is
//! the over-constraining this oracle's next section exists to avoid.
//!
//! The owned-push invariant is narrower: **every push that stows an entry
//! retires exactly that entry at the pop which observes its completion**, so
//! what remains in the inventory is precisely the set of owned pushes whose
//! completions have not yet been seen. [`IoRing::held`] counts that set, which
//! is a subset of what [`IoRing::outstanding`] counts: `held() <= outstanding()`,
//! and the gap is the raw operations in flight.
//! Teardown checks the matching property rather than the equality: that rundown
//! succeeded **and** no identity the ring minted is still in flight, which
//! covers the inventory as well ([D-78](../DESIGN-NOTES.md#d-78)).
//!
//! # What it deliberately does **not** check
//!
//! Being explicit about this matters as much as the list above: over-
//! constraining is the same defect as under-specifying, and an oracle that
//! reports a violation which is not one trains its reader to ignore it.
//!
//! - **Completion order.** The ring makes no ordering promise between
//! independent operations, so this counts them and never sequences them.
//! There is one promised ordering -- a covering flush against the operations
//! *preceding* it, and nothing about those following it
//! ([D-24](../DESIGN-NOTES.md#d-24), as corrected by
//! [D-47](../DESIGN-NOTES.md#d-47-detail)) -- and this oracle does not check
//! it. Not because it is unobservable: tag the operations and it is entirely
//! observable from the completion stream, which is exactly how
//! [tests/flush_barrier.rs](../tests/flush_barrier.rs) tests it and how D-47
//! measured the flag's one-sidedness over some 4,500 trials. It is that
//! *this* oracle is a conservation checker -- it matches each completion
//! against an outstanding claim and never relates that claim to the order
//! anything was submitted in, so it holds nothing it could compare against.
//!
//! An observer that does want to check it needs tagged identities, so that a
//! popped completion can be attributed to the operation it belongs to. Pop
//! order itself is a faithful witness of the order the kernel *posted* those
//! completions -- that is precisely the observable D-47 measured, and what
//! this crate's contract is stated in terms of. What it does not witness is
//! the order the operations *began executing*, which is invisible from user
//! mode -- see [D-47](../DESIGN-NOTES.md#d-47-detail) for why the contract is
//! stated in terms of completion order and stops there.
//! - **Whether an operation succeeded.** A failed operation still completes
//! exactly once; conservation and success are different questions.
//! - **Anything about the device.** Whether a flush truly reached durable
//! media is invisible here and everywhere else short of a power cut.
//! - **That a caller pushed anything sensible.** This checks conservation of
//! what was pushed, not that pushing it was a good idea.
use ;
use fmt;
/// A conservation rule this crate promises, broken.
/// What one operation *still being tracked* is known to have done so far.
///
/// Terminal outcomes are deliberately absent. An operation that finishes --
/// which since [D-74](../DESIGN-NOTES.md#d-74) means simply that its
/// completion was popped -- leaves this map entirely and its identity moves
/// to the bounded history described
/// on [`RingContract`], because retaining a terminal entry per operation is
/// what made the oracle grow without limit (M28.2).
/// How many finished identities the oracle remembers for duplicate diagnosis.
///
/// A **diagnostic window, not a correctness parameter.** Nothing is missed
/// when a duplicate falls outside it: the completion is still reported, as
/// [`Violation::UnexpectedCompletion`] rather than
/// [`Violation::DuplicateCompletion`]. What the window buys is the *stronger*
/// of the two claims, which the variants' own docs explain is worth keeping --
/// a duplicate cannot be explained away by a caller forgetting to report a
/// push, and an unrecognised identity can.
///
/// Changing it is not a breaking change. It trades a fixed amount of memory
/// for how far back a duplicate is still named precisely.
const FINISHED_HISTORY: usize = 1024;
/// An executable form of this crate's conservation rules.
///
/// Fed by the caller rather than wired into [`crate::Batch`], for two reasons.
/// A ring can be driven through `push_raw` and the `_raw` entry points without
/// any of this crate's bookkeeping being involved at all, so an internal hook
/// would silently cover less than it appears to. And a consumer validating its
/// own harness needs to drive the same rules from outside.
///
/// # What this costs to run, which is bounded (M28.2)
///
/// Memory here is a function of **operations in flight**, not of operations
/// ever performed. An operation that finishes leaves the tracking map, so a
/// consumer that pushes and claims forever holds a map whose size follows its
/// own concurrency rather than its uptime.
///
/// That was not true before M28.2: a claimed operation was marked `Completed`
/// and kept, so the oracle retained one entry per operation for the life of
/// the process. The sample never showed it because it appends 24 records, and
/// nothing documented it -- so a long-running consumer following this crate's
/// own recommendation grew without limit. It is also why an always-on checked
/// inventory was ruled out in `M23.3`, since a check that cannot be left
/// running is not a check.
///
/// Retiring an entry would lose the ability to call a later completion for it
/// a *duplicate* rather than merely unrecognised, so the last
/// `FINISHED_HISTORY` finished identities are remembered for that purpose
/// alone. Beyond that window a duplicate is still reported, under the weaker
/// name.
///
/// # Example
///
/// ```
/// use windows_ioring_sys::contract::RingContract;
///
/// let mut contract = RingContract::new();
/// contract.observe_push(0x1234);
/// contract.observe_completion(0x1234);
/// assert!(contract.check_quiescent().is_empty());
/// ```