libxtc 0.4.0
Async concurrency for C: Tokio + Seastar + BEAM, in one library
Loading...
Searching...
No Matches
xtc_dst_inject.h
1/*-
2 * Copyright (c) 2026, The XTC Project
3 * Use of this source code is governed by the ISC License.
4 *
5 * src/inc/xtc_dst_inject.h
6 * DST bug-injection harness (the "bug-detection latency" yardstick).
7 *
8 * FoundationDB / TigerBeetle back the claim "deterministic simulation
9 * finds real bugs" by PLANTING a known bug and proving the simulator
10 * catches it within a small number of seeds, deterministically, with
11 * a replayable trace. That -- not a code-coverage percentage -- is
12 * the metric that inspires confidence: "if you break a safety
13 * invariant, DST catches it fast and hands you the exact seed."
14 *
15 * This header defines the injection points. In a normal build
16 * XTC_DST_INJECT_BUG is undefined and every check compiles to 0, so
17 * the harness is completely absent from production and from the
18 * default test build. A dedicated build defines
19 * -DXTC_DST_INJECT_BUG=<n> to activate exactly ONE planted bug, and
20 * the DST suite is then expected to FAIL (an invariant fires) within
21 * a bounded seed count -- driven by scripts/dst-bug-inject.sh, which
22 * asserts each planted bug is caught. A planted bug the sweep does
23 * NOT catch is a hole in the DST coverage of that safety property.
24 *
25 * Each bug id targets a DST-reachable safety-critical site whose
26 * violation a specific invariant checker or capstone test detects:
27 *
28 * 1 LOSTWAKE -- proc.c drops a mailbox waker fire. A parked
29 * receiver never wakes; the sim's quiescence /
30 * lost-wakeup invariant (a proc still alive but no
31 * runnable work and no timer) fires -> XTC_E_DEADLK.
32 * 2 LOCKEXCL -- lock_mgr.c grants a conflicting lock. Mutual
33 * exclusion breaks; test_sim_compose's lock-held
34 * witness (count must stay <= 1) fires.
35 * 3 NODURABLE -- wal.c skips the fdatasync but still acks the
36 * commit. An acked commit is not durable; the
37 * test_sim_compose_crash durability invariant (every
38 * acked commit present after recovery) fires.
39 * 4 CREDITWIN -- credit.c posts the free-credit semaphore twice on
40 * release. The sliding window can then be exceeded;
41 * test_sim_credit's window invariant (in-flight
42 * never > window) fires.
43 * 5 RESLEAK -- res.c drops the decrement in xtc_res_release. The
44 * accountant never returns to zero; test_sim_res'
45 * conservation invariant (final used == 0) fires.
46 * 6 RESOVER -- res.c skips the cap check in xtc_res_acquire. The
47 * cap can be blown through; test_sim_res' SAFETY
48 * invariant (used never > cap) fires.
49 * 7 CHANDROP -- chan.c drops a message in xtc_chan_mpmc_try_recv
50 * (advances tail without returning it). An item is
51 * lost; test_sim_chan's mpmc exactly-once invariant
52 * (no drop/dup) fires.
53 * 8 REGDUP -- reg.c lets a second pid register a name already
54 * held. At-most-one-holder breaks; test_sim_reg's
55 * duplicate-registration invariant fires.
56 * 9 SAGAORDER -- saga.c compensates the completed prefix FORWARD
57 * instead of in reverse. The undo order is wrong;
58 * test_sim_saga's exact-reverse-order invariant
59 * fires.
60 *
61 * 10 BATCHWAKE -- batch.c drops the submit notification; parked driver
62 * fails the logical progress bound.
63 * 11 BATCHCAP -- batch.c admits beyond max_active; active cap fails.
64 * 12 BATCHRES -- batch.c retains terminal reservations; conservation fails.
65 * 13 BATCHSTALE -- batch.c ignores handle identity; wrong request cancelled.
66 * 14 BATCHDONE -- batch.c retains DONE members in the next vector.
67 * 15 SCHEDFAIR -- sched.c ignores the mandatory fairness override;
68 * the bounded-service invariant fails.
69 * 16 BATCHDROP -- batch.c drops an mt hand-in drained into a full
70 * group; an accepted request never completes.
71 * 17 WALKILL -- examples/06_sqlxtc/wal.c runs a commit without the
72 * cancellation mask, so a killed committer leaves a
73 * dead waiter (or the leadership) behind; the log
74 * wedges (test_sim_wal_kill: LIVENESS).
75 * 18 IDXSKIP -- examples/06_sqlxtc/xstore.c's index rebuild at an
76 * open skips the last index, so after a crash
77 * recovery that index misses rows
78 * (test_sim_sqlxtc_reopen: INDEX).
79 * 19 EVICTNOWB -- examples/06_sqlxtc/bufmgr.c's evictor drops every
80 * 4th dirty victim without writing it back; the
81 * page reloads stale (test_sim_sqlxtc_evict: a lost
82 * or wrong row).
83 * 20 OCKDROP -- examples/06_sqlxtc/wal.c's online checkpoint drops
84 * the last frame of each catch-up / finish copy, so
85 * a commit acked during the checkpoint is missing
86 * from the new log (test_sim_sqlxtc_ckpt: a lost
87 * or wrong row after crash recovery).
88 * 21 PRUNEHZN -- examples/06_sqlxtc/xstore.c's prune-on-write
89 * deletes the version AT the snapshot horizon (the
90 * one the oldest snapshot reads) when a newer one
91 * exists (test_sim_sqlxtc_gc: SNAPSHOT).
92 * 22 SHIFTLO -- examples/06_sqlxtc/btree.c's cursor_seek skips the
93 * lower-fence re-check when a parked cursor resumes,
94 * so after a redistribution moved its position into
95 * the LEFT sibling it resumes at the page's first key
96 * and skips the keys that moved
97 * (test_sim_btree_scan: skipped anchor).
98 *
99 * NOT plantable under DST (an honest gap, recorded so it is not
100 * mistaken for missing coverage): the xtc_amutex mutual-exclusion and
101 * lost-wakeup invariants. test_sim_latch's critical section is
102 * deliberately yield-free, so the single-threaded cooperative
103 * scheduler runs each section atomically and a double-grant never
104 * interleaves a lost update; and a dropped hand-off wake is invisible
105 * because the sim reschedules a parked fiber from its state (as
106 * test_sim_wake_park documents), not from a wake fd, and unlock sets
107 * w->granted under the lock before waking. Both amutex bugs were
108 * built and confirmed to pass the test both ways, so they are dropped
109 * rather than shipped as coverage theater. Mutual exclusion IS proven
110 * by bug 2 (LOCKEXCL) against the heavyweight lock manager.
111 *
112 * When you add a new safety invariant, add a planted-bug id here and a
113 * case to scripts/dst-bug-inject.sh so DST must prove it catches it.
114 */
115
116#ifndef XTC_DST_INJECT_H
117#define XTC_DST_INJECT_H
118
119/*
120 * XTC_DST_BUG(n) is 1 iff the build activated planted bug n. Zero in
121 * every normal build (XTC_DST_INJECT_BUG undefined), so all injection
122 * sites vanish. Exactly one bug is active per injected build.
123 */
124#if defined(XTC_DST_INJECT_BUG)
125# define XTC_DST_BUG(n) ((XTC_DST_INJECT_BUG) == (n))
126#else
127# define XTC_DST_BUG(n) (0)
128#endif
129
130/* Symbolic ids (keep in sync with scripts/dst-bug-inject.sh). */
131#define XTC_DST_BUG_LOSTWAKE 1 /* proc.c: drop a mailbox waker fire */
132#define XTC_DST_BUG_LOCKEXCL 2 /* lock_mgr.c: grant a conflicting lock */
133#define XTC_DST_BUG_NODURABLE 3 /* wal.c: skip fdatasync, still ack */
134#define XTC_DST_BUG_CREDITWIN 4 /* credit.c: double-post the free-credit sem */
135#define XTC_DST_BUG_RESLEAK 5 /* res.c: drop the release decrement */
136#define XTC_DST_BUG_RESOVER 6 /* res.c: skip the acquire cap check */
137#define XTC_DST_BUG_CHANDROP 7 /* chan.c: drop an mpmc message on recv */
138#define XTC_DST_BUG_REGDUP 8 /* reg.c: allow a duplicate registration */
139#define XTC_DST_BUG_SAGAORDER 9 /* saga.c: compensate forward, not reverse */
140
141#define XTC_DST_BUG_BATCHWAKE 10 /* batch.c: omit submit notification */
142#define XTC_DST_BUG_BATCHCAP 11 /* batch.c: ignore max_active admission cap */
143#define XTC_DST_BUG_BATCHRES 12 /* batch.c: retain terminal reservation */
144#define XTC_DST_BUG_BATCHSTALE 13 /* batch.c: ignore handle identity */
145#define XTC_DST_BUG_BATCHDONE 14 /* batch.c: retain completed vector member */
146#define XTC_DST_BUG_SCHEDFAIR 15 /* sched.c: bypass mandatory fairness override */
147#define XTC_DST_BUG_BATCHDROP 16 /* batch.c: drop a held mt hand-in */
148#define XTC_DST_BUG_WALKILL 17 /* wal.c: commit not masked against kills */
149#define XTC_DST_BUG_IDXSKIP 18 /* xstore.c: an index rebuild skips one index */
150#define XTC_DST_BUG_EVICTNOWB 19 /* bufmgr.c: evict a dirty page unwritten */
151#define XTC_DST_BUG_OCKDROP 20 /* wal.c: an online-checkpoint copy round drops its last frame */
152#define XTC_DST_BUG_PRUNEHZN 21 /* xstore.c: prune-on-write deletes the version at the horizon */
153#define XTC_DST_BUG_SHIFTLO 22 /* btree.c: a resumed cursor skips the lo-fence re-check */
154#define XTC_DST_BUG_GCBATCH 23 /* xstore.c: version GC forgets its row at a batch boundary */
155
156#endif /* XTC_DST_INJECT_H */