nx_arena_smp_gate.nx source
↩ module page · 215 lines · 10520 B
1// nx_arena_smp_gate.nx -- TWO THREADS MUST NEVER RECEIVE THE SAME POINTER.
2//
3// THE DEFECT, MEASURED 2026-08-25 while shipping structured concurrency. The arena bump allocator
4// inside nx_syscalls advanced its cursor with a plain read-modify-write:
5// let p: i64 = nxa_st[0]
6// nxa_st[0] = p + need
7// Two threads that read the cursor before either wrote it BOTH RECEIVE THE SAME POINTER and then
8// write over one another. Eight pool workers calling a helper that allocates a 16-byte timespec hit
9// exactly this and produced ARENA-OVERRUN prev_alloc_size=16 followed by SIGSEGV. It generalises to
10// EVERY small allocation from more than one thread -- which is why the scoped-spawn child body was
11// deliberately written to allocate nothing, load-bearing rather than incidental.
12//
13// WHY A BARRIER AND NOT A LOST-UPDATE COUNT. The obvious non-vacuity proof is to run an UNLOCKED
14// counter beside the allocator and show it loses updates. That proof is PROBABILISTIC: on a run where
15// the threads happen not to interleave it shows no loss, and the gate would go RED for no reason.
16// A DETECTOR WITH FALSE POSITIVES IS WORSE THAN NONE. So overlap is established DETERMINISTICALLY:
17// every task blocks on an atomic barrier until ALL of them have arrived, and only then allocates.
18// If the barrier is reached, the tasks provably held the allocator at the same time; if it is not,
19// this gate reports the pointer-distinctness result as UNPROVEN rather than GREEN, because an
20// AXIS THAT CANNOT SEE MUST ABSTAIN, NOT ACQUIT.
21// The lost-update count is still MEASURED and PRINTED beside it, as evidence about the machine
22// rather than as a tooth.
23
24import "nx_syscalls.nx"
25import "nx_gate_verdict.nx"
26import "nx_thread_pool.nx"
27
28// Allocations per task. Chosen large enough that every task holds the allocator many times over the
29// barrier rather than once, so a single unlucky interleaving cannot be what the verdict rests on.
30const AG_PER: i64 = 256
31// Worker/task count is DERIVED from the hardware at runtime (nx_hw_worker_count), never chosen. This
32// is only the ceiling on the result table, sized from the pool's own documented worker bound.
33const AG_MAXTASKS: i64 = 64
34// A BOUND ON AN UNKNOWABLE WAIT, NAMED, AND ITS EXHAUSTION ANNOUNCES. If a task spins this long at
35// the barrier the other tasks are not coming -- the pool gave us fewer live workers than tasks -- so
36// the task gives up, the barrier reports NOT-REACHED, and the distinctness tooth abstains instead of
37// claiming a proof it does not have. Derived from the pool's own join guard so the two agree.
38const AG_BARRIER_SPINS: i64 = NX_MAGIC_2000000000
39
40static ag_ptrs: *i64 // AG_MAXTASKS * AG_PER pointer slots, one region per task, no sharing
41static ag_bar: *i64 // [0] arrived (atomic), [1] released count, [2] gave-up count
42static ag_racy: *i64 // [0] deliberately UNLOCKED counter, [1] atomic control counter
43static ag_ntasks: i64
44
45func ag_puts(s: *u8) -> i64 {
46 var n: i64 = 0
47 while s[n] != (0 as u8) { n = n + 1 }
48 sys_write(1, s, n)
49 return 0
50}
51
52func ag_putn(v: i64) -> i64 {
53 if v == 0 { ag_puts("0\x00" as *u8); return 0 }
54 var x: i64 = v
55 if x < 0 { ag_puts("-\x00" as *u8); x = 0 - x }
56 let t: *u8 = sys_mmap(32)
57 var n: i64 = 0
58 while x > 0 { t[n] = (48 + (x % 10)) as u8; n = n + 1; x = x / 10 }
59 let o: *u8 = sys_mmap(32)
60 var i: i64 = n
61 var j: i64 = 0
62 while i > 0 { i = i - 1; o[j] = t[i]; j = j + 1 }
63 o[j] = 0 as u8
64 ag_puts(o)
65 return 0
66}
67
68// Every task: announce arrival, WAIT for all peers, then hammer the allocator. The wait is what makes
69// the allocations provably simultaneous rather than merely issued from different threads.
70func ag_task(id: i64) -> i64 {
71 let arrived: i64 = __atomic_faa_i64(ag_bar, 1, NX_MO_SEQ_CST) + 1
72 if arrived < 0 { return 1 }
73 var spins: i64 = 0
74 var released: i64 = 0
75 while released == 0 {
76 if __atomic_load_i64(ag_bar, NX_MO_ACQUIRE) >= ag_ntasks { released = 1 }
77 if released == 0 {
78 spins = spins + 1
79 if spins > AG_BARRIER_SPINS {
80 // The peers are not coming. Record it so the verdict can ABSTAIN rather than claim a
81 // concurrency proof this run did not earn.
82 let g: i64 = __atomic_faa_i64(((ag_bar as i64) + 16) as *i64, 1, NX_MO_SEQ_CST)
83 if g < 0 { return 1 }
84 released = 1
85 }
86 }
87 }
88 let r: i64 = __atomic_faa_i64(((ag_bar as i64) + 8) as *i64, 1, NX_MO_SEQ_CST)
89 if r < 0 { return 1 }
90
91 var k: i64 = 0
92 while k < AG_PER {
93 let p: *u8 = sys_mmap(16)
94 ag_ptrs[id * AG_PER + k] = p as i64
95 // MEASURED, NOT ASSERTED: the same unlocked read-modify-write shape the arena used to have,
96 // run under the identical contention. Its loss is printed as evidence about this machine.
97 let v: i64 = ag_racy[0]
98 ag_racy[0] = v + 1
99 let prior: i64 = __atomic_faa_i64(((ag_racy as i64) + 8) as *i64, 1, NX_MO_SEQ_CST)
100 if prior < 0 { return 1 }
101 k = k + 1
102 }
103 return 0
104}
105
106func main(argc: i64, argv: *i64) -> i64 {
107 ag_puts("=== nx_arena_smp_gate -- two threads must never receive the same pointer ===\n\x00" as *u8)
108 let ctr: *i64 = gv_ctr()
109
110 var nw: i64 = nx_hw_worker_count()
111 if nw < 2 { nw = 2 }
112 if nw > AG_MAXTASKS { nw = AG_MAXTASKS }
113 ag_ntasks = nw
114 let total: i64 = ag_ntasks * AG_PER
115
116 ag_ptrs = sys_mmap(AG_MAXTASKS * AG_PER * 8) as *i64
117 ag_bar = sys_mmap(64) as *i64
118 ag_racy = sys_mmap(64) as *i64
119
120 let pool: *NxThreadPool = nx_pool_new(ag_ntasks, AG_MAXTASKS * 4)
121 let sc: *NxScope = sc_scope_open(pool)
122 var t: i64 = 0
123 var spawn_ok: i64 = 1
124 while t < ag_ntasks {
125 if sc_scope_spawn(sc, ag_task, t) < 0 { spawn_ok = 0 }
126 t = t + 1
127 }
128 sc_scope_join(sc)
129
130 let arrived: i64 = ag_bar[0]
131 let released: i64 = ag_bar[1]
132 let gaveup: i64 = ag_bar[2]
133 let racy: i64 = ag_racy[0]
134 let atomicv: i64 = ag_racy[1]
135
136 ag_puts(" workers=\x00" as *u8); ag_putn(ag_ntasks)
137 ag_puts(" per_task=\x00" as *u8); ag_putn(AG_PER)
138 ag_puts(" total_allocs=\x00" as *u8); ag_putn(total)
139 ag_puts("\n barrier arrived=\x00" as *u8); ag_putn(arrived)
140 ag_puts(" released=\x00" as *u8); ag_putn(released)
141 ag_puts(" gave_up=\x00" as *u8); ag_putn(gaveup)
142 ag_puts("\n unlocked_counter=\x00" as *u8); ag_putn(racy)
143 ag_puts(" atomic_counter=\x00" as *u8); ag_putn(atomicv)
144 ag_puts(" lost_updates=\x00" as *u8); ag_putn(total - racy)
145 ag_puts("\n\x00" as *u8)
146
147 gv_check("spawn-accepted-every-task\x00" as *u8, (spawn_ok == 1) as i64, ctr)
148
149 // FIXTURE REACHED THE CONDITION. Without this the distinctness tooth below is satisfied by a run
150 // in which the tasks executed one after another and never contended at all.
151 let overlapped: i64 = ((arrived == ag_ntasks) & (released == ag_ntasks) & (gaveup == 0)) as i64
152 gv_check("fixture-reached-condition-ALL-tasks-held-the-allocator-simultaneously\x00" as *u8,
153 overlapped, ctr)
154
155 // THE LOAD-BEARING TOOTH. Every pointer handed out under that proven contention must be distinct.
156 // A duplicate IS the defect: two threads owning the same bytes.
157 var dupes: i64 = 0
158 var zeros: i64 = 0
159 var i: i64 = 0
160 while i < total {
161 let a: i64 = ag_ptrs[i]
162 if a == 0 { zeros = zeros + 1 }
163 var j: i64 = i + 1
164 while j < total {
165 if ag_ptrs[j] == a { dupes = dupes + 1 }
166 j = j + 1
167 }
168 i = i + 1
169 }
170 ag_puts(" duplicate_pointers=\x00" as *u8); ag_putn(dupes)
171 ag_puts(" null_pointers=\x00" as *u8); ag_putn(zeros)
172 ag_puts("\n\x00" as *u8)
173
174 gv_check("no-two-concurrent-allocations-returned-the-same-pointer\x00" as *u8,
175 ((dupes == 0) & (overlapped == 1)) as i64, ctr)
176 gv_check("no-allocation-returned-null\x00" as *u8, (zeros == 0) as i64, ctr)
177
178 // POSITIVE CONTROLS. An allocator that refused every request, or a harness that recorded nothing,
179 // would satisfy "no duplicates" trivially. These are what stop that.
180 gv_check("positive-control-the-population-is-NON-EMPTY-and-bound-to-its-denominator\x00" as *u8,
181 (total == (ag_ntasks * AG_PER)) as i64, ctr)
182 gv_check("positive-control-more-than-one-worker-actually-ran\x00" as *u8,
183 (ag_ntasks >= 2) as i64, ctr)
184
185 // THE ATOMIC CONTROL. Proves the harness really did perform `total` increments from those threads,
186 // so the distinctness result above is measured over the work it claims. If this is short, the
187 // tasks did not run and nothing else here means anything.
188 gv_check("atomic-control-the-harness-performed-EVERY-increment-it-claims\x00" as *u8,
189 (atomicv == total) as i64, ctr)
190
191 // The unlocked counter is EVIDENCE, not a tooth: its loss is real but probabilistic, and asserting
192 // on it would make this gate flaky. It is printed above so a reader can see the race is live on
193 // this machine, and its absence never fails the run.
194
195 // TWO-SIDED, AND THIS IS A CORRECTION TO MY OWN FIRST CUT. That version asserted "zero after
196 // join" and FAILED -- correctly, because it never called sc_scope_free: it was asserting a
197 // postcondition of free() without ever establishing it. ASSERT THE FIXTURE REACHED THE CONDITION
198 // BEFORE ASSERTING THE OUTCOME applies to teardown exactly as it does to setup.
199 // Measuring BOTH sides is strictly stronger than the original intent: the scope must STILL HOLD
200 // its arena after join, and must return ALL of it after free -- so an accounting function that
201 // simply always answered zero would fail the first tooth and cannot quietly pass the second.
202 let held_after_join: i64 = sc_live_bytes()
203 sc_scope_free(sc)
204 let held_after_free: i64 = sc_live_bytes()
205 ag_puts(" scope_bytes_after_join=\x00" as *u8); ag_putn(held_after_join)
206 ag_puts(" after_free=\x00" as *u8); ag_putn(held_after_free)
207 ag_puts("\n\x00" as *u8)
208 gv_check("scope-still-HELD-its-arena-after-join-so-the-release-below-is-a-real-release\x00" as *u8,
209 (held_after_join > 0) as i64, ctr)
210 gv_check("scope-memory-returned-to-zero-after-free\x00" as *u8,
211 (held_after_free == 0) as i64, ctr)
212
213 return gv_verdict("NX-ARENA-SMP-GATE\x00" as *u8, ctr,
214 "concurrent allocations are distinct, under a barrier that proves they were concurrent\x00" as *u8)
215}