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 * NOT plantable under DST (an honest gap, recorded so it is not
62 * mistaken for missing coverage): the xtc_amutex mutual-exclusion and
63 * lost-wakeup invariants. test_sim_latch's critical section is
64 * deliberately yield-free, so the single-threaded cooperative
65 * scheduler runs each section atomically and a double-grant never
66 * interleaves a lost update; and a dropped hand-off wake is invisible
67 * because the sim reschedules a parked fiber from its state (as
68 * test_sim_wake_park documents), not from a wake fd, and unlock sets
69 * w->granted under the lock before waking. Both amutex bugs were
70 * built and confirmed to pass the test both ways, so they are dropped
71 * rather than shipped as coverage theater. Mutual exclusion IS proven
72 * by bug 2 (LOCKEXCL) against the heavyweight lock manager.
73 *
74 * When you add a new safety invariant, add a planted-bug id here and a
75 * case to scripts/dst-bug-inject.sh so DST must prove it catches it.
76 */
77
78#ifndef XTC_DST_INJECT_H
79#define XTC_DST_INJECT_H
80
81/*
82 * XTC_DST_BUG(n) is 1 iff the build activated planted bug n. Zero in
83 * every normal build (XTC_DST_INJECT_BUG undefined), so all injection
84 * sites vanish. Exactly one bug is active per injected build.
85 */
86#if defined(XTC_DST_INJECT_BUG)
87# define XTC_DST_BUG(n) ((XTC_DST_INJECT_BUG) == (n))
88#else
89# define XTC_DST_BUG(n) (0)
90#endif
91
92/* Symbolic ids (keep in sync with scripts/dst-bug-inject.sh). */
93#define XTC_DST_BUG_LOSTWAKE 1 /* proc.c: drop a mailbox waker fire */
94#define XTC_DST_BUG_LOCKEXCL 2 /* lock_mgr.c: grant a conflicting lock */
95#define XTC_DST_BUG_NODURABLE 3 /* wal.c: skip fdatasync, still ack */
96#define XTC_DST_BUG_CREDITWIN 4 /* credit.c: double-post the free-credit sem */
97#define XTC_DST_BUG_RESLEAK 5 /* res.c: drop the release decrement */
98#define XTC_DST_BUG_RESOVER 6 /* res.c: skip the acquire cap check */
99#define XTC_DST_BUG_CHANDROP 7 /* chan.c: drop an mpmc message on recv */
100#define XTC_DST_BUG_REGDUP 8 /* reg.c: allow a duplicate registration */
101#define XTC_DST_BUG_SAGAORDER 9 /* saga.c: compensate forward, not reverse */
102
103#endif /* XTC_DST_INJECT_H */