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
// Copyright (C) 2024-2025 Greg Burd. Licensed under either of the
// Apache License, Version 2.0 or the MIT license, at your option.
// See LICENSE-APACHE and LICENSE-MIT at the root of this repository.
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Shuttle concurrency-permutation gate for the BIN/IN split-path
//! check-then-act race (DST tree coverage).
//!
//! The whole file compiles to nothing unless built with `--cfg noxu_shuttle`,
//! so the default `cargo test` and every production build are unaffected.
//! Under the cfg, the tree-node `RwLock` resolves (through
//! `noxu_util::dst_sync_pl`, routed in `noxu-tree/src/tree.rs`) to a
//! shuttle-instrumented lock, so shuttle's scheduler explores the
//! `split_child` / merge-clear interleavings of the *real* split path. The
//! hand-over-hand `read_arc()` read descent is backed under shuttle by
//! `noxu_latch::dst_arc_guard` (an Arc-owning read guard the
//! `#![forbid(unsafe_code)]` tree/util crates cannot host themselves), so the
//! *entire* tree — read and write paths — is schedulable.
//!
//! # The bug this gate closes
//!
//! (`.agent/archived-audits/bench/bug-bin-split-concurrency.md`.)
//! `insert_recursive_inner` checked `child.get_n_entries() >= max_entries`
//! under a PARENT READ lock, dropped that read lock (required — the split
//! needs `parent.write()`), then called `split_child`. In the drop→reacquire
//! window a racing thread — a second splitter, or the INCompressor merging and
//! CLEARING a sibling (`compress_node`'s `entries.clear()`) — could leave the
//! child no longer full, or empty. Pre-fix, `split_child` then built a
//! `SplitEntries` from that stale child and `SplitEntries::get_key(split_index)`
//! panicked with "index out of bounds: len is 0" on the empty entries vec.
//!
//! **The fix (v7.2.2):** `split_child`, after taking the child write lock,
//! re-validates `child.get_n_entries() >= max_entries` and returns `Ok(())`
//! (a benign no-op) if a racing thread already emptied/split it — the check
//! and the split are now atomic w.r.t. the child latch, matching JE's
//! `IN.split` re-testing `needsSplitting()` after latching.
//!
//! # Why this reproduces the bug that a benchmark had to find
//!
//! The 96-thread saturation benchmark found this because DST could not: the
//! tree used `parking_lot::RwLock` directly, so shuttle could not schedule the
//! node-latch interleavings. Routing the node latch through the seam (with the
//! hand-over-hand `read_arc()` descent backed under shuttle by
//! `noxu_latch::dst_arc_guard`) makes the whole tree schedulable; shuttle now
//! drives the exact drop→reacquire race deterministically over thousands of
//! interleavings.
//!
//! # Not vacuous (the regression proof)
//!
//! [`split_racing_merge_clear_never_panics`] and
//! [`two_concurrent_splitters_never_panic`] both PASS with the fix and FAIL
//! (shuttle finds the panicking interleaving) with the re-check reverted. To
//! prove it locally, delete the two lines in `Tree::split_child`
//!
//! ```ignore
//! if child_guard.get_n_entries() < max_entries {
//! return Ok(());
//! }
//! ```
//!
//! and re-run under `--cfg noxu_shuttle`: shuttle reports a panicking schedule
//! ("index out of bounds: the len is 0 but the index is 0" in
//! `SplitEntries::get_key`) with a reproducible seed. Restore the fix and every
//! schedule passes. (This is documented, not run automatically, so the gate
//! stays green in CI while the reversal proof remains a one-edit check.)
//!
//! # Invariants (mapped to `noxu-spec` `btree_latching`)
//!
//! * **no-panic** — no schedule panics (the observed symptom of the bug).
//! * **split-atomicity** (`btree_latching::AtMostOneSplit` /
//! `LockInvariant`) — `split_child` never operates on a stale (emptied or
//! no-longer-full) child: it either splits a still-full child or returns
//! the benign `Ok(())` no-op. Never a partial/garbage split; a full child
//! is split at most once.
//! * **structural-consistency** — after the race quiesces the parent's slot
//! count is coherent (never fewer entries than it started with; a
//! successful split adds exactly one sibling slot).
//! * **key-order** (`btree_latching::NoLostWrites`) — every entry that
//! remains in the child is in sorted key order (no lost/duplicated/
//! reordered entry from a torn split).
//!
//! # Running
//!
//! ```sh
//! RUSTFLAGS="--cfg noxu_shuttle" cargo test -p noxu-tree --test shuttle_bin_split
//! ```
use ;
use Lsn;
use Arc;
/// Number of interleavings shuttle explores per test.
const ITERATIONS: usize = 5_000;
/// Build a level-2 tree (root Internal with BIN children) whose rightmost BIN
/// child is topped up to exactly `max_entries` (full, i.e. the state where the
/// next insert would split it). Construction is single-threaded and
/// uncontended, so it runs fine on shuttle's cooperative executor (no green
/// thread ever blocks on a lock here).
///
/// A plain bulk insert never fills a child to `max` (each split leaves halves
/// ~half-full), so we extend the rightmost key range until one child reaches
/// `max` — the precise "full child about to be split" state the bug needs.
/// Locate a resident, still-full BIN child of the root together with its slot
/// index. Returns `None` if the tree did not build a level-2 shape (defensive;
/// 64 keys / max 8 always splits).
/// Assert the child, whatever the schedule left it, is a coherent BIN: entries
/// in sorted key order, no duplicates. A torn split (the pre-fix failure mode)
/// would leave garbage or panic before reaching here.
/// THE REGRESSION: a `split_child` racing an INCompressor-style merge-clear on
/// the SAME child. This is the drop→reacquire window from the bug report: the
/// caller passed the fullness check under the (now-dropped) parent read lock,
/// then a racing merge emptied the child before the split re-acquired its
/// write lock.
///
/// With the v7.2.2 re-check, every interleaving is safe: if the clear wins the
/// child write lock first, `split_child` re-validates fullness and returns the
/// benign `Ok(())` no-op; if the split wins first, it splits the still-full
/// child and the clear then empties the (now left-half) child. No schedule
/// panics. With the fix reverted, shuttle finds the clear-then-split schedule
/// and `SplitEntries::get_key(0)` panics on the empty vec.
/// Read descent (`search`, which uses the hand-over-hand `read_arc()` coupling
/// backed under shuttle by `noxu_latch::dst_arc_guard`) racing a concurrent
/// `insert`. This exercises the Arc-owning-guard shim at runtime and asserts
/// the descent is safe under interleaving: no panic, and a key that was present
/// before the race is always found (latch coupling means `search` never falls
/// into the wrong half of a concurrent split). Fewer iterations — the descent
/// is deeper, so schedules are larger.
/// Two concurrent splitters on the SAME full child — the primary bug scenario:
/// two inserters both pass the read-lock fullness check, both drop the parent
/// read lock, both call `split_child`. They serialise on `parent.write()`; the
/// first splits, and by the time the second takes the child write lock the
/// child is no longer full. With the re-check the second returns the benign
/// `Ok(())` no-op; without it the second builds a `SplitEntries` from the
/// now-half (or the first's torn intermediate) child and can panic.