nx_sts_lock_gate.nx source
↩ module page · 116 lines · 4555 B
1// nx_sts_lock_gate.nx -- proves sts_append_row's lock actually prevents the seq1559 lost-row race.
2//
3// THE COMPARISON IS CONTROLLED: both arms run the IDENTICAL read-modify-write with the IDENTICAL
4// artificial window (a sleep between load and commit). The ONLY difference is whether <prefix>plock
5// is held across it. If the locked arm keeps every row and the unlocked arm loses some, the lock is
6// doing the work -- nothing else varies, so nothing else can be credited.
7//
8// NON-VACUITY IS THE POINT: a concurrency test that never triggers the race proves nothing at all.
9// The unlocked arm MUST lose rows. If it does not, this gate reports VACUOUS rather than GREEN --
10// a guard that cannot be shown to fire has not been tested.
11// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
12import "nx_store_seed_lib.nx"
13import "nx_seg_store.nx"
14import "nx_syscalls.nx"
15import "nx_gate_verdict.nx"
16
17const G_N: i64 = 6
18const G_CAP: i64 = 262144
19const G_WIDEN_MS: i64 = 150
20const G_NL: i64 = 10
21const G_PATHCAP: i64 = 256
22
23func g_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
24func g_num(v: i64) -> i64 {
25 if v == 0 { g_w("0" as *u8); return 0 }
26 var x: i64 = v
27 if x < 0 { g_w("-" as *u8); x = 0 - x }
28 let b: *u8 = sys_mmap(32)
29 var i: i64 = 0
30 while x > 0 { b[i] = ((x % 10) + 48) as u8; x = x / 10; i = i + 1 }
31 while i > 0 { i = i - 1; sys_write(1, ((b as i64) + i) as *u8, 1) }
32 return 0
33}
34
35// count newline-terminated rows currently in the plane
36func g_rows(prefix: *u8) -> i64 {
37 let buf: *u8 = sys_mmap(G_CAP)
38 let n: i64 = sts_load(prefix, buf, G_CAP)
39 var c: i64 = 0
40 var i: i64 = 0
41 while i < n { if buf[i] == (G_NL as u8) { c = c + 1 } i = i + 1 }
42 sys_munmap(buf, G_CAP)
43 return c
44}
45
46// ONE worker. locked=1 holds the plane lock across the whole read-modify-write; locked=0 does the
47// exact same sequence with no lock. Everything else -- buffer, widening, row -- is identical.
48func g_worker(prefix: *u8, id: i64, locked: i64) -> i64 {
49 var fd: i64 = 0 - 1
50 if locked == 1 { fd = sts_lock(prefix) }
51 let buf: *u8 = sys_mmap(G_CAP)
52 var n: i64 = sts_load(prefix, buf, G_CAP)
53 if n < 0 { n = 0 }
54 sys_sleep_ms(G_WIDEN_MS)
55 buf[n] = 114 as u8
56 n = n + 1
57 buf[n] = (48 + id) as u8
58 n = n + 1
59 buf[n] = G_NL as u8
60 n = n + 1
61 sts_seed(prefix, buf, n)
62 if locked == 1 { sts_unlock(fd) }
63 return 0
64}
65
66// reset the plane to empty, then run G_N concurrent workers, then count what survived
67func g_arm(prefix: *u8, locked: i64) -> i64 {
68 let empty: *u8 = sys_mmap(16)
69 sts_seed(prefix, empty, 0)
70 var k: i64 = 0
71 while k < G_N {
72 let pid: i64 = sys_fork()
73 if pid == 0 {
74 g_worker(prefix, k, locked)
75 sys_exit_group(0)
76 }
77 k = k + 1
78 }
79 let st: *i64 = sys_mmap(16) as *i64
80 var reaped: i64 = 0
81 while reaped < G_N { if sys_wait4(0 - 1, st, 0) > 0 { reaped = reaped + 1 } else { reaped = G_N } }
82 return g_rows(prefix)
83}
84
85func main(argc: i64, argv: *i64) -> i64 {
86 g_w("nx_sts_lock_gate -- does the plane lock actually stop the seq1559 lost-row race?\n\n" as *u8)
87 let pl: *u8 = "knowledge/store/stslockgate-locked-" as *u8
88 let pu: *u8 = "knowledge/store/stslockgate-unlocked-" as *u8
89
90 let got_u: i64 = g_arm(pu, 0)
91 g_w(" T1 UNLOCKED arm (neg control): " as *u8); g_num(G_N); g_w(" concurrent appends -> " as *u8)
92 g_num(got_u); g_w(" rows survived\n" as *u8)
93
94 let got_l: i64 = g_arm(pl, 1)
95 g_w(" T2 LOCKED arm (sts_lock) : " as *u8); g_num(G_N); g_w(" concurrent appends -> " as *u8)
96 g_num(got_l); g_w(" rows survived\n\n" as *u8)
97
98 var pass: i64 = 0
99 if got_l == G_N {
100 if got_u < G_N {
101 pass = 1
102 g_w(" T3 the lock is the ONLY variable and it is decisive: unlocked LOST " as *u8)
103 g_num(G_N - got_u); g_w(" of " as *u8); g_num(G_N)
104 g_w(" rows, locked lost 0\n" as *u8)
105 }
106 }
107 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
108 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
109 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
110 let ctr__dry: *i64 = gv_ctr()
111 ctr__dry[0] = pass
112 ctr__dry[1] = 1
113 let rc__dry: i64 = gv_verdict("STS-LOCK-GATE" as *u8, ctr__dry, "race REPRODUCED unlocked, PREVENTED locked)" as *u8)
114 sys_exit(rc__dry)
115 return rc__dry
116}