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
//! Loom enumeration test for the cross-shard park/wake fence.
//!
//! `kevy-ring`'s SPSC ring already has its own loom suite (see
//! `crates/kevy-ring/tests/loom.rs`) covering the producer/consumer
//! handshake at the atomic level. This test sits one layer up — it
//! models the **park-bit** that `Shard::run` wraps around the ring to
//! avoid a lost-wake-up race:
//!
//! ```text
//! Receiver side (Shard::run):
//! ... idle loop ...
//! parked[me].store(true, SeqCst); // 1. advertise "I'm parking"
//! fence(SeqCst); // 2. fence ↕ sender's load
//! if drain_inbound()? { // 3. one more drain attempt
//! parked[me].store(false, SeqCst); // 4. found work → un-park
//! continue; // and process
//! }
//! poller.wait(PARK_TIMEOUT_MS) // 5. block (woken by sender)
//!
//! Sender side (send_to + flush_wakes):
//! ring.push(msg) // A. push (or set a flag)
//! fence(SeqCst); // B. fence ↕ receiver's store
//! if parked[dst].load(SeqCst) { // C. only wake if parked
//! wakers[dst].wake() // D. syscall (eventfd write)
//! }
//! ```
//!
//! The invariant: in every legal interleaving the receiver either
//! (i) sees the message in step `3` or (ii) gets a wake signal (because
//! the sender's load in `C` observed `parked=true`). The bug the test
//! guards against is "both empty": receiver drained nothing AND sender
//! skipped the wake — which would leave the receiver blocked forever
//! in production (until `PARK_TIMEOUT_MS` saved it, but that's a
//! 50 ms-latency band-aid, not a correctness fix).
//!
//! Production NOTE: the current `Shard::run` relies on the SeqCst
//! total order of `parked.store` ↔ `parked.load` alone, *without* the
//! explicit SeqCst fences modelled here. The fences are needed to
//! make the disjunction hold *without* the `PARK_TIMEOUT_MS=50 ms`
//! backstop. As written, production has a (rare) lost-wake window
//! bounded by 50 ms — acceptable for v1 but worth revisiting when
//! tail-latency tuning comes around. The loom test below documents
//! the fenced version that *would* be lock-free-correct, so a future
//! refactor can drop the timeout without regressing.
//!
//! ## Charter
//!
//! `loom` is a dev-only crates.io crate gated behind `--cfg loom` in
//! `Cargo.toml` — it never enters a normal `cargo build` / `cargo test`.
//! Same status as `cargo-fuzz` / `cargo-llvm-cov` (charter-exempted
//! dev-tool dep).
//!
//! ## How to run
//!
//! ```bash
//! RUSTFLAGS="--cfg loom" cargo test -p kevy-rt --test loom --release
//! ```
//!
//! `--release` is recommended: loom's exhaustive search explores
//! thousands of interleavings, and debug builds make each one slow.
use ;
use Arc;
use thread;
/// Reduced model — replace the SPSC ring with one `AtomicBool` flag so
/// the test space is small enough for `LOOM_MAX_PREEMPTIONS=2`. The
/// pattern of "push payload then load parked" / "store parked then peek
/// payload" is identical; loom is exercising the SeqCst fence between
/// them, which is the actual primitive under test.
/// Same property, but flipped: assert the *contrapositive* — if the
/// sender did NOT signal a wake (sender saw parked=false), then the
/// receiver MUST have drained the published message. This is the
/// strict correctness invariant the fence buys us in addition to the
/// disjunction above.