code wiki / (root) / nx_lockbound_gate.nx

nx_lockbound_gate.nx

buildroot/runtime/nx_lockbound_gate.nx

7953 B142 linesdepth 3pulls 4 transitivereach 0 importersview sourcekind gate/proof
docsdependenciesstructsconstsfunctions

about

nx_lockbound_gate.nx -- does ss_plane_lock REFUSE a wedged plane instead of hanging on it? WHY. The 2026-08-06 commit lock closed a real defect (nx_segrace_gate: 24/24 kept vs 4/24 under a verbatim unlocked control) but it did so with a BLOCKING flock, and that changed the failure mode rather than only removing the defect. MEASURED the same day: nx_segrace_gate went RED with an UNCHANGED binary because one worker sat in kernel state D wchan=wait_for_commit -- a filesystem journal commit -- HOLDING the lock, while its siblings sat in wchan=locks_lock_inode_wait. The lock behaved correctly; the WAIT was unbounded. Trading silent data loss for an unbounded hang is not obviously a win, and it must not be discovered by whoever is on call. Debt 1786070596. ★A GUARD THAT CANNOT BE SHOWN TO FIRE HAS NOT BEEN TESTED, and a TIMEOUT is the easiest guard in the world to write and never exercise: on a healthy host the bound is simply never reached, so the code path ships untested and only runs for the first time during the incident it exists for. This gate manufactures the incident: a child DELIBERATELY HOLDS the plane lock for longer than the ceiling while the parent tries to commit through it. BOTH WAYS, because a lock that always refuses would also pass a refusal-only test: T1 CONTROL -- with NO holder, a commit must SUCCEED (the lock still works normally) T2 BOUNDED -- with a holder, the commit must be REFUSED, and refused STRICTLY BEFORE the holder lets go. Elapsed < hold time is the whole point: it proves the parent gave up on its own bound rather than simply outlasting the holder, which is the failure a naive "did it eventually return?" test cannot tell apart. license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0

dependencies 3 imports · 0 importers

nx_seg_store.nx nx_syscalls.nx nx_gate_verdict.nx nx_lockbound_gate.nx

imports: nx_seg_store.nxnx_syscalls.nxnx_gate_verdict.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main gv_ctr sys_mmap nxa_die sys_write sys_exit nxa_lock_take nxa_lock_addr sys_write ↻ nxa_lock_give nxa_lock_addr ↻ nxa_report_overrun sys_write ↻ nxa_dump_printable sys_write ↻ nxa_dump_sizes sys_write ↻ lb_p sys_write ↻ lb_reset sys_mmap ↻ ss_cat ss_writefile sys_openat_wr sys_write ↻ sys_close sys_fsync lb_commit_one ss_begin_cap sys_mmap ↻ ss_add ss_add2 ss_w32 ss_len ss_commit ss_segid_ok ss_commit_body ss_segid_ok ↻ sys_mmap ↻ ss_cat ↻

structs

none

consts

43const LB_HEADROOM_MS: i64 = 30000
44const LB_SETTLE_MS: i64 = 700 // let the child actually acquire before the parent attempts
45const LB_CAP: i64 = 4096
46const LB_KIND_LIVE: i64 = 1

functions

48func lb_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
called by 2: lb_nmain calls 1: sys_write
49func lb_n(v: i64) -> i64
called by 1: main calls 3: lb_psys_mmapsys_write
60func lb_commit_one(prefix: *u8, key: *u8) -> i64
67func lb_reset(prefix: *u8) -> i64
called by 1: main calls 3: sys_mmapss_catss_writefile
77func main(argc: i64, argv: *i64) -> i64