nx_index_wr_decouple_gate.nx source
↩ module page · 53 lines · 3469 B
1// nx_index_wr_decouple_gate.nx -- proves write-read decoupling: a reader pinned to a generation is UNAFFECTED by
2// concurrent writers (snapshot isolation), while new readers see new segments (monotonic visibility). license_tier: ORIGINAL
3import "nx_index_wr_decouple.nx"
4import "nx_gate.nx"
5
6func gwf(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} if fd>=0 { sys_write(fd,s,n) } return 0 }
7
8func main() -> i64 {
9 gw("=== nx_index_wr_decouple_gate: ingest builds segments while queries serve a pinned snapshot ===\n" as *u8)
10 var pass: i64=0; var tot: i64=0
11
12 let counts: *i64 = sys_mmap(8*8) as *i64
13 counts[0]=100; counts[1]=50; counts[2]=25 // per-segment doc counts (immutable once committed)
14 let nseg: *i64 = sys_mmap(8) as *i64; nseg[0]=0
15
16 // writer commits seg0 -> gen1; reader A pins its snapshot at gen1 and queries.
17 let gA: i64 = wr_commit(nseg)
18 let rA: i64 = wr_query(counts, gA)
19
20 // writer commits seg1, seg2 (later, "concurrent") -> gen2, gen3.
21 wr_commit(nseg); wr_commit(nseg)
22
23 // reader A re-reads AT ITS PINNED SNAPSHOT -> must be UNCHANGED (writes were invisible to it).
24 let rA2: i64 = wr_query(counts, gA)
25 var t1: i64=0; if rA==100 { if rA2==100 { t1=1 } }
26 tot=tot+1; if t1==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
27 gw("T1 snapshot isolation: reader@gen1 = " as *u8); gn(rA); gw(" then " as *u8); gn(rA2); gw(" AFTER 2 concurrent writes (unchanged)\n" as *u8)
28
29 // new readers see the new segments (monotonic visibility).
30 let rB: i64 = wr_query(counts, 2)
31 let rC: i64 = wr_query(counts, 3)
32 var t2: i64=0; if rB==150 { if rC==175 { t2=1 } }
33 tot=tot+1; if t2==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
34 gw("T2 monotonic visibility: reader@gen2 = " as *u8); gn(rB); gw(", reader@gen3 = " as *u8); gn(rC); gw("\n" as *u8)
35
36 // visible segment sets are correct per snapshot.
37 let va: *i64 = sys_mmap(8*8) as *i64; let na: i64 = wr_visible(1, va)
38 let vc: *i64 = sys_mmap(8*8) as *i64; let nc: i64 = wr_visible(3, vc)
39 var t3: i64=0; if na==1 { if va[0]==0 { if nc==3 { if vc[0]==0 { if vc[1]==1 { if vc[2]==2 { t3=1 } } } } } }
40 tot=tot+1; if t3==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
41 gw("T3 visible sets: reader@gen1={0}, reader@gen3={0,1,2}\n" as *u8)
42
43 // decoupling: the writer advanced to gen3 while reader A stayed pinned at gen1 -> ingest never blocked the read.
44 var t4: i64=0; if nseg[0]==3 { if rA2==100 { t4=1 } }
45 tot=tot+1; if t4==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
46 gw("T4 decoupled: writer at gen=" as *u8); gn(nseg[0]); gw(" while reader stayed at gen1 (ingest continuous, query never blocked)\n" as *u8)
47
48 gw("\n=== nx_index_wr_decouple_gate " as *u8); gn(pass); gw("/" as *u8); gn(tot); gw(" ===\n" as *u8)
49 let lfd: i64=sys_openat_append("knowledge/status/wr_decouple_gate.log" as *u8, 420)
50 if pass==tot { gwf(lfd, "WR-DECOUPLE-GATE verdict=GREEN snapshot-isolation monotonic-visibility\n" as *u8); if lfd>=0 { sys_close(lfd) } gw("WR-DECOUPLE GREEN -- ingest builds segments while queries serve a pinned snapshot; the NAS ingests Common Crawl while the site keeps serving\n" as *u8); sys_exit(0); return 0 }
51 gwf(lfd, "WR-DECOUPLE-GATE verdict=RED\n" as *u8); if lfd>=0 { sys_close(lfd) }
52 gw("WR-DECOUPLE RED\n" as *u8); sys_exit(1); return 1
53}