code wiki / _hdl_build / nx_dispatch_lease_gate.nx

nx_dispatch_lease_gate.nx source

↩ module page · 243 lines · 12862 B

1// nx_dispatch_lease_gate.nx -- the REFEREE for WMS rung M4 (leasing dispatcher). 2// 3// module: nishi-core.autonomy.dispatch_lease_gate 4// capability: GATE (prints a VERDICT computed from REAL checks; incl negative control) 5// 6// PROVES (the gate requirement, exactly): 7// T1 picks-READY -- dl_pick_ready returns the highest-w READY rung, never blocked 8// T2 dispatch-leases -- dl_dispatch leases that rung (fd>=0, id matches, lease file exists) 9// T3 second-dispatch-DENIED -- a 2nd dl_try_lease on the SAME stream returns -1 (the 10// collision proof: two workers cannot hold one stream) 11// T3b keep-moving -- a fresh dl_dispatch while the top is leased returns the NEXT 12// ready stream (not the blocked one, not a stall) 13// T4 NEG CONTROL -- a deliberately BLOCKED stream (unmet dep) is NEVER dispatched: 14// dl_ready==0 AND no dispatch ever returns its id 15// T5 release-then-redispatch -- after dl_release the same stream leases again (fd>=0): 16// proves it is a LEASE (releasable), not a permanent mark 17// T6 TAMPER -- (a) fa_append oversize -> -2 (durability rejects, never torn) 18// (b) a stale lease (epoch older than DL_STALE_SEC) is STOLEN 19// (fd>=0) -- a dead worker's lease cannot wedge the machine 20// 21// VALIDITY (why the neg-control genuinely bites): if dl_pick_ready ignored an_deps_done it 22// would return G-BLOCKED -> T1/T4 RED. If dl_try_lease used plain open not O_EXCL, T3 would 23// return fd>=0 (collision) -> RED. If dl_release didn't unlink, T5 would stay -1 -> RED. 24// 25// HERMETIC: the gate WRITES its own scratch queue to /tmp/dlg_<ms>.tsv (9-field rows, same 26// grammar) and uses a fresh scratch lease dir /tmp/dlg_<ms>/ -- it NEVER touches production. 27// <ms> = sys_now_realtime_ms() so two concurrent gate runs never share lease state. 28// 29// WRITE DISCIPLINE: every evidence record (one buffer -> one locked fa_appendz) to 30// knowledge/status/dispatch_lease_gate.log -- eating our own dogfood (the torn-line floor). 31// license_tier: ORIGINAL 32import "nx_dispatch_lease.nx" 33import "nx_framed_append.nx" 34 35const GLOG: *u8 = "knowledge/status/dispatch_lease_gate.log\x00" as *u8 36 37func g_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 38func g_n(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m; sys_write(1,"-" as *u8,1)}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;k=1}; while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1}; var i: i64=0; while i<k{bb[i]=t[k-1-i];i=i+1}; sys_write(1,bb,k); return 0 } 39 40// append decimal of v (NUL-terminated) into dst at off; returns new offset. 41func g_catd(dst: *u8, off: i64, v: i64) -> i64 { 42 let o: i64 = fa_catn(dst, off, v) 43 dst[o] = 0 as u8 44 return o 45} 46 47// one-buffer -> one locked fa_appendz evidence record: "MGATE test=<name> result=PASS|FAIL detail=<n>" 48func g_log(name: *u8, pass: i64, detail: i64) -> i64 { 49 let buf: *u8 = sys_mmap(256 + 16) 50 var o: i64 = 0 51 o = fa_cat(buf, o, "MGATE test=\x00" as *u8) 52 o = fa_cat(buf, o, name) 53 o = fa_cat(buf, o, " result=\x00" as *u8) 54 if pass == 1 { o = fa_cat(buf, o, "PASS\x00" as *u8) } else { o = fa_cat(buf, o, "FAIL\x00" as *u8) } 55 o = fa_cat(buf, o, " detail=\x00" as *u8) 56 o = fa_catn(buf, o, detail) 57 buf[o] = 0 as u8 58 return fa_appendz(GLOG, buf, 256) 59} 60 61// print + log one assertion; returns pass (1/0) so the caller can tally. 62func g_assert(name: *u8, pass: i64, detail: i64) -> i64 { 63 g_p(" " as *u8); g_p(name); g_p(": \x00" as *u8) 64 if pass == 1 { g_p("PASS\x00" as *u8) } else { g_p("FAIL\x00" as *u8) } 65 g_p(" (detail=\x00" as *u8); g_n(detail); g_p(")\n\x00" as *u8) 66 g_log(name, pass, detail) 67 return pass 68} 69 70// getpid (__syscall 39) is BROKEN on this backend (-25 for EVERY process -> not unique -> the real cause of the 71// intermittent-RED control-plane flake). Claim a process-unique i64 token ATOMICALLY via O_EXCL: first creator of 72// /tmp/nxuq_<n> owns <n>; a collision (EEXIST, fd<0) retries n+1. Seeded by monotonic us. Provably collision-free. 73func g_uniq() -> i64 { 74 var n: i64 = sys_now_us() 75 if n < 0 { n = 0 - n } 76 var tries: i64 = 0 77 while tries < 1000000 { 78 let p: *u8 = sys_mmap(64) 79 var o: i64 = fa_cat(p, 0, "/tmp/nxuq_\x00" as *u8) 80 o = fa_catn(p, o, n) 81 p[o] = 0 as u8 82 let fd: i64 = __syscall(SYS_OPENAT, AT_FDCWD, p, 0xc1, 0x1a4, 0, 0) // O_CREAT|O_EXCL|O_WRONLY 83 if fd >= 0 { sys_close(fd); return n } 84 n = n + 1 85 tries = tries + 1 86 } 87 return n 88} 89// build the scratch queue path /tmp/dlg_<ms>_<uniq>.tsv and the lease dir /tmp/dlg_<ms>_<uniq> into outs. 90func g_scratch_paths(ms: i64, qpath: *u8, ldir: *u8) -> i64 { 91 var o: i64 = 0 92 o = fa_cat(ldir, o, "/tmp/dlg_\x00" as *u8) 93 o = fa_catn(ldir, o, ms) 94 ldir[o] = 95 as u8; o = o + 1 // '_' -- ms-only collided at the same millisecond under concurrency (the flake); g_uniq makes scratch collision-proof 95 o = fa_catn(ldir, o, g_uniq()) 96 ldir[o] = 0 as u8 // ldir = "/tmp/dlg_<ms>_<uniq>" 97 var q: i64 = 0 98 while ldir[q] != (0 as u8) { qpath[q] = ldir[q]; q = q + 1 } 99 qpath[q] = 46 as u8; q = q + 1 // '.' 100 qpath[q] = 116 as u8; q = q + 1 // 't' 101 qpath[q] = 115 as u8; q = q + 1 // 's' 102 qpath[q] = 118 as u8; q = q + 1 // 'v' 103 qpath[q] = 0 as u8 // qpath = "/tmp/dlg_<ms>.tsv" 104 return 0 105} 106 107// write the controlled scratch fixture (9 tab fields per row; '\n' terminated). 108// Dep graph: G-READY-HI (w9, no dep), G-READY-LO (w5, no dep), G-BLOCKED (w9, dep 109// G-DEP which is still TODO not DONE -> blocked), G-DEP (w1, no dep, status TODO). 110// G-DEP is authored ONLY to be G-BLOCKED's unmet dependency. It MUST be TODO (so 111// G-BLOCKED stays blocked = the neg-control), but its weight is deliberately w1 -- 112// below G-READY-LO (w5) -- so that in the T3b keep-moving scan (G-READY-HI held) the 113// next-best READY UNLEASED row is unambiguously G-READY-LO, not G-DEP. (G-DEP is 114// itself independently ready since it has no deps; w1 keeps it from outranking the 115// intended keep-moving target without changing its TODO/blocked-dep role.) 116func g_write_fixture(path: *u8) -> i64 { 117 let fd: i64 = sys_openat_wr(path, 0x1a4) // O_CREAT|O_WRONLY|O_TRUNC, 0644 118 if fd < 0 { return 0 - 1 } 119 let s: *u8 = "G-READY-HI\tX\t9\tS\tBuilder\tTODO\t-\tgate\tready-hi\nG-READY-LO\tX\t5\tS\tBuilder\tTODO\t-\tgate\tready-lo\nG-BLOCKED\tX\t9\tS\tBuilder\tTODO\tG-DEP\tgate\tblocked-on-dep\nG-DEP\tX\t1\tS\tBuilder\tTODO\t-\tgate\tthe-unmet-dep\n\x00" as *u8 120 var n: i64 = 0 121 while s[n] != (0 as u8) { n = n + 1 } 122 sys_write(fd, s, n) 123 sys_close(fd) 124 return 0 125} 126 127// hand-write a STALE lease file (epoch=1, far older than DL_STALE_SEC) at <dir>/<id>.lease 128// so T6b can prove dl_try_lease STEALS it. 129func g_write_stale_lease(dir: *u8, id: *u8) -> i64 { 130 let lp: *u8 = sys_mmap(512) 131 dl_lease_path(dir, id, lp) 132 let fd: i64 = sys_openat_wr(lp, 0x1a4) 133 if fd < 0 { return 0 - 1 } 134 sys_write(fd, "1\x00" as *u8, 1) // epoch=1 (1970) -> always stale 135 sys_close(fd) 136 return 0 137} 138 139func main() -> i64 { 140 g_p("=== M4 DISPATCH-LEASE GATE: pick READY -> lease -> deny dup -> keep moving -> neg-ctrl blocked -> release-redispatch -> tamper ===\n\x00" as *u8) 141 let ms: i64 = sys_now_realtime_ms() 142 let qpath: *u8 = sys_mmap(128) 143 let ldir: *u8 = sys_mmap(128) 144 g_scratch_paths(ms, qpath, ldir) 145 sys_mkdir(ldir, 0x1ed) // fresh hermetic lease dir 146 if g_write_fixture(qpath) < 0 { g_p(" FIXTURE-WRITE-FAILED\n\x00" as *u8); sys_exit(1); return 1 } 147 148 let cx: *i64 = an_newcx() 149 let rows: i64 = an_load(qpath, cx) 150 if rows <= 0 { g_p(" FIXTURE-LOAD-FAILED\n\x00" as *u8); sys_exit(1); return 1 } 151 152 let rhi: i64 = an_find(cx, "G-READY-HI\x00" as *u8) 153 let rlo: i64 = an_find(cx, "G-READY-LO\x00" as *u8) 154 let rbl: i64 = an_find(cx, "G-BLOCKED\x00" as *u8) 155 var pass: i64 = 0 156 157 // ---- T1: picks the highest-w READY rung (G-READY-HI), skipping the blocked one ---- 158 let p1: i64 = dl_pick_ready(cx) 159 var t1: i64 = 0 160 if p1 == rhi { t1 = 1 } 161 pass = pass + g_assert("T1-picks-READY\x00" as *u8, t1, p1) 162 163 // ---- T2: dispatch leases that rung (fd>=0, id==G-READY-HI, lease file exists) ---- 164 let id_out: *u8 = sys_mmap(64) 165 let fd_out: *i64 = sys_mmap(16) as *i64 166 let fd2: i64 = dl_dispatch(cx, ldir, id_out, fd_out) 167 var t2: i64 = 0 168 if fd2 >= 0 { if dl_streq(id_out, "G-READY-HI\x00" as *u8) == 1 { if dl_lease_held(ldir, "G-READY-HI\x00" as *u8) == 1 { t2 = 1 } } } 169 pass = pass + g_assert("T2-dispatch-leases\x00" as *u8, t2, fd2) 170 171 // ---- T3: a SECOND lease attempt on the SAME held stream is DENIED (-1) ---- 172 let fd3: i64 = dl_try_lease(ldir, "G-READY-HI\x00" as *u8) 173 var t3: i64 = 0 174 if fd3 < 0 { t3 = 1 } // -1 = correctly denied (no collision) 175 if fd3 >= 0 { dl_release(ldir, "G-READY-HI\x00" as *u8, fd3) } // safety: don't leak a wrongly-won lease 176 pass = pass + g_assert("T3-second-dispatch-DENIED\x00" as *u8, t3, fd3) 177 178 // ---- T3b: keep-moving -- fresh dispatch while G-READY-HI is leased -> G-READY-LO ---- 179 let id_b: *u8 = sys_mmap(64) 180 let fd_b: *i64 = sys_mmap(16) as *i64 181 let fdb: i64 = dl_dispatch(cx, ldir, id_b, fd_b) 182 var t3b: i64 = 0 183 if fdb >= 0 { if dl_streq(id_b, "G-READY-LO\x00" as *u8) == 1 { t3b = 1 } } 184 pass = pass + g_assert("T3b-keep-moving\x00" as *u8, t3b, fdb) 185 186 // ---- T4: NEGATIVE CONTROL -- the BLOCKED stream is never ready, never dispatched ---- 187 // (a) dl_ready(G-BLOCKED)==0 because its dep G-DEP is TODO not DONE. 188 // (b) neither dispatched id (T2 id_out, T3b id_b) is ever G-BLOCKED. 189 var t4: i64 = 1 190 if dl_ready(cx, rbl) != 0 { t4 = 0 } // blocked must be NOT ready 191 if dl_streq(id_out, "G-BLOCKED\x00" as *u8) == 1 { t4 = 0 } 192 if dl_streq(id_b, "G-BLOCKED\x00" as *u8) == 1 { t4 = 0 } 193 pass = pass + g_assert("T4-NEGCTRL-blocked-never-dispatched\x00" as *u8, t4, dl_ready(cx, rbl)) 194 195 // ---- T5: release G-READY-HI, then it is re-dispatchable (lease again succeeds) ---- 196 dl_release(ldir, "G-READY-HI\x00" as *u8, fd_out[0]) 197 let fd5: i64 = dl_try_lease(ldir, "G-READY-HI\x00" as *u8) 198 var t5: i64 = 0 199 if fd5 >= 0 { t5 = 1 } // re-leasable after release (was -1 in T3) 200 if fd5 >= 0 { dl_release(ldir, "G-READY-HI\x00" as *u8, fd5) } // tidy up 201 pass = pass + g_assert("T5-release-then-redispatch\x00" as *u8, t5, fd5) 202 203 // ---- T6a: TAMPER -- fa_append oversize rejected (-2), durability never torn ---- 204 let ot: i64 = fa_append("/tmp/dlg_tamper.txt\x00" as *u8, "0123456789012345678901234567890123456789\x00" as *u8, 40, 8) 205 var t6a: i64 = 0 206 if ot == (0 - 2) { t6a = 1 } // -2 = oversized REJECTED 207 pass = pass + g_assert("T6a-TAMPER-oversize-rejected\x00" as *u8, t6a, ot) 208 209 // ---- T6b: TAMPER -- a STALE lease (epoch 1970) is STOLEN, not honored ---- 210 // release G-READY-LO first (T3b holds it), then plant a stale lease and steal it. 211 if fdb >= 0 { dl_release(ldir, "G-READY-LO\x00" as *u8, fd_b[0]) } 212 g_write_stale_lease(ldir, "G-STALE\x00" as *u8) 213 let fd6: i64 = dl_try_lease(ldir, "G-STALE\x00" as *u8) // must STEAL (epoch 1 < now-30) 214 var t6b: i64 = 0 215 if fd6 >= 0 { t6b = 1 } 216 if fd6 >= 0 { dl_release(ldir, "G-STALE\x00" as *u8, fd6) } 217 pass = pass + g_assert("T6b-TAMPER-stale-lease-stolen\x00" as *u8, t6b, fd6) 218 219 // ---- VERDICT ---- 220 let total: i64 = 8 // T1 T2 T3 T3b T4 T5 T6a T6b 221 var ok: i64 = 0 222 if pass == total { ok = 1 } 223 g_p("M4 DISPATCH-LEASE-GATE pass=\x00" as *u8); g_n(pass); g_p("/\x00" as *u8); g_n(total); g_p(" verdict=\x00" as *u8) 224 if ok == 1 { g_p("GREEN\n\x00" as *u8) } else { g_p("RED\n\x00" as *u8) } 225 226 // final verdict record -- one buffer -> one locked fa_appendz 227 let vb: *u8 = sys_mmap(256 + 16) 228 var vo: i64 = 0 229 vo = fa_cat(vb, vo, "DISPATCH-LEASE-GATE pass=\x00" as *u8) 230 vo = fa_catn(vb, vo, pass) 231 vo = fa_cat(vb, vo, "/\x00" as *u8) 232 vo = fa_catn(vb, vo, total) 233 vo = fa_cat(vb, vo, " epoch=\x00" as *u8) 234 vo = fa_catn(vb, vo, sys_now_realtime_sec()) 235 vo = fa_cat(vb, vo, " verdict=\x00" as *u8) 236 if ok == 1 { vo = fa_cat(vb, vo, "GREEN\x00" as *u8) } else { vo = fa_cat(vb, vo, "RED\x00" as *u8) } 237 vb[vo] = 0 as u8 238 fa_appendz(GLOG, vb, 256) 239 240 if ok == 1 { sys_exit(0); return 0 } 241 sys_exit(1) 242 return 1 243}