nx_regbatch_gate.nx source
↩ module page · 133 lines · 5975 B
1// nx_regbatch_gate.nx -- INDEPENDENT GATE: batched durability in reg_put. Correctness FIRST, speed second.
2// INHERITS nx_gate_verdict (D001).
3//
4// A speedup that loses rows is not a speedup, so this gate proves the SAFETY properties before it
5// looks at the clock:
6// u2605VISIBILITY IS NOT DEFERRED. reg_put_deferred writes the segment and renames the manifest exactly
7// as reg_put does -- only the power-loss barrier waits. A row must be readable IMMEDIATELY, before
8// any sync. If that were false the batch would be a lie, so it is asserted first.
9// u2605THE TWO PATHS MUST AGREE BYTE-FOR-BYTE. Same body, two entry points -- proven by writing the same
10// record both ways and comparing what comes back. This is the anti-fork tooth: nx_gate_verdict once
11// forked between trees and an identical migration bought different capability depending on where it
12// ran. One body cannot fork; this check is what keeps it honest.
13// u2605THE INDEX SURVIVES. A batched put must still land in the enumeration index, or a fast write that
14// nothing can find is worse than a slow one.
15// Only then: u2605the batch must actually be faster, or the whole change is unjustified complexity.
16// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
17
18import "nx_registry.nx"
19import "nx_gate_verdict.nx"
20
21func rb_cat(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != (0 as u8) { dst[off+i] = s[i]; i = i + 1 } return off + i }
22func rb_catn(dst: *u8, off: i64, v: i64) -> i64 {
23 var m: i64 = v
24 var o: i64 = off
25 if m == 0 { dst[o] = 48 as u8; return o + 1 }
26 let t: *u8 = sys_mmap(24)
27 var k: i64 = 0
28 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
29 var i: i64 = 0
30 while i < k { dst[o+i] = t[k-1-i]; i = i + 1 }
31 return o + k
32}
33
34func main(argc: i64, argv: *i64) -> i64 {
35 let ctr: *i64 = gv_ctr()
36 gv_head("NX-REGBATCH (batched durability: visibility, agreement, index, then speed)" as *u8)
37
38 let nonce: i64 = sys_now_us()
39 let pd: *u8 = sys_mmap(256)
40 var o: i64 = rb_cat(pd, 0, "knowledge/store/rbD" as *u8)
41 o = rb_catn(pd, o, nonce)
42 pd[o] = 45 as u8
43 o = o + 1
44 pd[o] = 0 as u8
45 let pb: *u8 = sys_mmap(256)
46 o = rb_cat(pb, 0, "knowledge/store/rbB" as *u8)
47 o = rb_catn(pb, o, nonce)
48 pb[o] = 45 as u8
49 o = o + 1
50 pb[o] = 0 as u8
51
52 let rec: *u8 = sys_mmap(64)
53 var rl: i64 = rb_cat(rec, 0, "payload-v1" as *u8)
54 let idb: *u8 = sys_mmap(64)
55 let po: *i64 = sys_mmap(16) as *i64
56 let lo: *i64 = sys_mmap(16) as *i64
57
58 // ---- V: VISIBILITY IS NOT DEFERRED ----
59 rb_cat(idb, 0, "solo" as *u8)
60 idb[4] = 0 as u8
61 reg_put_deferred(pb, "rb:" as *u8, "rb:__idx__" as *u8, idb, rec, rl)
62 gv_check("V1 a deferred row is readable IMMEDIATELY, before any sync" as *u8, reg_get(pb, "rb:" as *u8, idb, po, lo) == 1, ctr)
63 gv_check("V2 and its length is intact" as *u8, lo[0] == rl, ctr)
64 var same: i64 = 1
65 let got: *u8 = po[0] as *u8
66 var q: i64 = 0
67 while q < rl { if got[q] != rec[q] { same = 0; q = rl } else { q = q + 1 } }
68 gv_check("V3 and its bytes are intact" as *u8, same == 1, ctr)
69
70 // ---- A: THE TWO PATHS AGREE ----
71 reg_put(pd, "rb:" as *u8, "rb:__idx__" as *u8, idb, rec, rl)
72 let po2: *i64 = sys_mmap(16) as *i64
73 let lo2: *i64 = sys_mmap(16) as *i64
74 gv_check("A1 the durable path stores the same row" as *u8, reg_get(pd, "rb:" as *u8, idb, po2, lo2) == 1, ctr)
75 gv_check("A2 both paths report the SAME length" as *u8, lo2[0] == lo[0], ctr)
76 var agree: i64 = 1
77 let g2: *u8 = po2[0] as *u8
78 var r: i64 = 0
79 while r < rl { if g2[r] != got[r] { agree = 0; r = rl } else { r = r + 1 } }
80 gv_check("A3 and the SAME bytes -- one body, two entry points, no fork" as *u8, agree == 1, ctr)
81
82 // ---- S: the barrier is idempotent and safe to over-call ----
83 gv_check("S1 reg_batch_sync succeeds" as *u8, reg_batch_sync(pb) == 0, ctr)
84 gv_check("S2 and is idempotent -- over-calling is free" as *u8, reg_batch_sync(pb) == 0, ctr)
85 gv_check("S3 the row still reads after the barrier" as *u8, reg_get(pb, "rb:" as *u8, idb, po, lo) == 1, ctr)
86
87 // ---- T: TIMING. durable batch vs deferred batch, same row count ----
88 let d0: i64 = sys_now_us()
89 var i: i64 = 0
90 while i < 8 {
91 var a: i64 = rb_cat(idb, 0, "d" as *u8)
92 a = rb_catn(idb, a, i)
93 idb[a] = 0 as u8
94 reg_put(pd, "rb:" as *u8, "rb:__idx__" as *u8, idb, rec, rl)
95 i = i + 1
96 }
97 let d1: i64 = sys_now_us()
98 let durable_us: i64 = d1 - d0
99
100 let b0: i64 = sys_now_us()
101 var j: i64 = 0
102 while j < 8 {
103 var b: i64 = rb_cat(idb, 0, "b" as *u8)
104 b = rb_catn(idb, b, j)
105 idb[b] = 0 as u8
106 reg_put_deferred(pb, "rb:" as *u8, "rb:__idx__" as *u8, idb, rec, rl)
107 j = j + 1
108 }
109 reg_batch_sync(pb)
110 let b1: i64 = sys_now_us()
111 let batch_us: i64 = b1 - b0
112
113 gv_puts(" durable_8_rows_us=" as *u8); gv_num(durable_us); gv_puts("\n" as *u8)
114 gv_puts(" batched_8_rows_plus_sync_us=" as *u8); gv_num(batch_us); gv_puts("\n" as *u8)
115 if batch_us > 0 {
116 gv_puts(" speedup_permille=" as *u8); gv_num((durable_us * 1000) / batch_us); gv_puts("\n" as *u8)
117 }
118
119 // ---- C: every batched row must still be findable AFTER the batch ----
120 var found: i64 = 0
121 var k: i64 = 0
122 while k < 8 {
123 var c: i64 = rb_cat(idb, 0, "b" as *u8)
124 c = rb_catn(idb, c, k)
125 idb[c] = 0 as u8
126 if reg_get(pb, "rb:" as *u8, idb, po, lo) == 1 { found = found + 1 }
127 k = k + 1
128 }
129 gv_check("C1 u2605all 8 batched rows are readable -- a fast write nothing can find is worse than a slow one" as *u8, found == 8, ctr)
130 gv_check("C2 u2605the batch is FASTER than the durable path" as *u8, batch_us < durable_us, ctr)
131
132 return gv_verdict("REGBATCH" as *u8, ctr, "visibility immediate; both paths byte-identical; all rows findable; batch faster" as *u8)
133}