nx_fabric_flow_gate.nx source
↩ module page · 137 lines · 7194 B
1// nx_fabric_flow_gate.nx -- LIVE GATE for R1 of the SkyHammer fabric exceed ladder.
2// Proves the ยง7 acceptance spec mechanically: a credit-controlled link (R1, composing
3// nx_h2_flow) is LOSSLESS + latency-BOUNDED under a burst that makes an uncontrolled
4// baseline drop heavily -- with three NEGATIVE CONTROLS so the result cannot be rigged.
5//
6// criteria (all must hold):
7// 1 R1 overflow-drops == 0 (lossless by construction)
8// 2 baseline drops >= 5% of N (the burst genuinely overloads -- non-vacuous)
9// 3a R1 p99 latency <= 3*(B/D) (bounded / deterministic)
10// 3b NC2 (lossless-uncontrolled) p99 >= 3 * R1 p99 (R1 escapes the loss/bloat tradeoff)
11// 4 R1 goodput >= baseline goodput (no throughput sacrifice)
12// negative controls:
13// NC1 credit bookkeeping w/o the backpressure gate -> drops RETURN (the GATE is the cause)
14// NC2 buffer >= N (no real bottleneck) -> baseline drops VANISH (bottleneck is real)
15// NC3 every run still delivers all N (drops counted at the buffer, independent of delivery)
16//
17// expect_exit: 0 license_tier: ORIGINAL
18import "nx_fabric_flow.nx"
19
20func gp(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
21func gn(v: i64) -> i64 {
22 let b: *u8 = sys_mmap(28); var m: i64 = v
23 if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) }
24 let t: *u8 = sys_mmap(28); var k: i64 = 0
25 if m == 0 { t[0] = 48 as u8; k = 1 }
26 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
27 var i: i64 = 0
28 while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
29 sys_write(1, b, k); return 0
30}
31func fdn(fd: i64, v: i64) -> i64 {
32 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m }
33 let t: *u8 = sys_mmap(28); var k: i64 = 0
34 if m == 0 { t[0] = 48 as u8; k = 1 }
35 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
36 var i: i64 = 0
37 while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
38 sys_write(fd, b, k); return 0
39}
40func chk(name: *u8, ok: i64) -> i64 {
41 if ok == 1 { gp(" PASS " as *u8); gp(name); gp("\n" as *u8); return 1 }
42 gp(" FAIL " as *u8); gp(name); gp("\n" as *u8); return 0
43}
44func show(tag: *u8, m: *FfMetrics) -> i64 {
45 gp(tag); gp(": drops=" as *u8); gn(m.drops); gp(" delivered=" as *u8); gn(m.delivered)
46 gp(" ticks=" as *u8); gn(m.ticks); gp(" p50=" as *u8); gn(m.p50); gp(" p99=" as *u8); gn(m.p99)
47 gp(" goodput(x1000)=" as *u8); gn(m.goodput_x1000); gp("\n" as *u8); return 0
48}
49
50func main() -> i64 {
51 let N: i64 = 600
52 let B: i64 = 16
53 let D: i64 = 4
54 let R: i64 = 16 // 4x overload (R/D) -> a real burst
55
56 gp("nx_fabric_flow R1 gate -- deterministic LOSSLESS credit flow vs uncontrolled\n" as *u8)
57 gp("link: N=" as *u8); gn(N); gp(" buffer=" as *u8); gn(B); gp(" drain=" as *u8); gn(D)
58 gp("/tick offer=" as *u8); gn(R); gp("/tick (overload=" as *u8); gn(R / D); gp("x)\n" as *u8)
59
60 let base: *FfMetrics = sys_mmap(64) as *FfMetrics
61 let r1: *FfMetrics = sys_mmap(64) as *FfMetrics
62 let nc1: *FfMetrics = sys_mmap(64) as *FfMetrics
63 let nc2: *FfMetrics = sys_mmap(64) as *FfMetrics
64
65 ff_run_sim(FF_UNCTL, N, B, D, R, base) // baseline: uncontrolled
66 ff_run_sim(FF_CREDIT, N, B, D, R, r1) // R1: credit-controlled
67 ff_run_sim(FF_NC1, N, B, D, R, nc1) // NC1: backpressure gate removed
68 ff_run_sim(FF_UNCTL, N, 2000, D, R, nc2) // NC2: buffer >= N, no bottleneck
69
70 show("BASELINE (uncontrolled)" as *u8, base)
71 show("R1 (credit/h2_flow)" as *u8, r1)
72 show("NC1 (credit, no backpressure)" as *u8, nc1)
73 show("NC2 (uncontrolled, huge buffer)" as *u8, nc2)
74
75 var pass: i64 = 0
76 var tot: i64 = 0
77
78 // 1. R1 lossless
79 var c1: i64 = 0; if r1.drops == 0 { c1 = 1 }
80 pass = pass + chk("1 R1 overflow-drops == 0 (LOSSLESS)" as *u8, c1); tot = tot + 1
81
82 // 2. baseline overload is real (>=5% of N)
83 var c2: i64 = 0; if base.drops >= (N * 5) / 100 { c2 = 1 }
84 pass = pass + chk("2 baseline drops >= 5% of N (burst non-vacuous)" as *u8, c2); tot = tot + 1
85
86 // 3a. R1 bounded latency
87 var c3a: i64 = 0; if r1.p99 <= (3 * B) / D { c3a = 1 }
88 pass = pass + chk("3a R1 p99 <= 3*(B/D) (BOUNDED/deterministic)" as *u8, c3a); tot = tot + 1
89
90 // 3b. The loss/bloat TRADEOFF exceed (the real, measured determinism story):
91 // a small uncontrolled buffer is low-latency only by DROPPING (criterion 2);
92 // the only uncontrolled way to be LOSSLESS is to oversize the buffer (NC2),
93 // which BLOATS the latency tail. R1 is lossless at a small buffer, so it gets
94 // BOTH -- the lossless-uncontrolled config pays >= 3x R1's p99 (here ~22x).
95 var c3b: i64 = 0; if r1.p99 >= 1 { if nc2.p99 >= 3 * r1.p99 { c3b = 1 } }
96 pass = pass + chk("3b lossless-uncontrolled (NC2) p99 >= 3 * R1 p99 (R1 escapes loss/bloat tradeoff)" as *u8, c3b); tot = tot + 1
97
98 // 4. no throughput sacrifice
99 var c4: i64 = 0; if r1.goodput_x1000 >= base.goodput_x1000 { c4 = 1 }
100 pass = pass + chk("4 R1 goodput >= baseline goodput" as *u8, c4); tot = tot + 1
101
102 // NC1: removing ONLY the backpressure gate brings the drops back -> the GATE is the cause.
103 var cn1: i64 = 0; if nc1.drops > 0 { cn1 = 1 }
104 pass = pass + chk("NC1 backpressure removed -> drops RETURN (engine proven)" as *u8, cn1); tot = tot + 1
105
106 // NC2: with no real bottleneck even the uncontrolled sender drops nothing.
107 var cn2: i64 = 0; if nc2.drops == 0 { cn2 = 1 }
108 pass = pass + chk("NC2 buffer>=N -> baseline drops VANISH (bottleneck is real)" as *u8, cn2); tot = tot + 1
109
110 // NC3: reliability -- every run still delivers all N (drops counted independently of delivery).
111 var cn3: i64 = 0
112 if base.delivered == N { if r1.delivered == N { if nc1.delivered == N { if nc2.delivered == N { cn3 = 1 } } } }
113 pass = pass + chk("NC3 all runs deliver N (drop counter independent of delivery)" as *u8, cn3); tot = tot + 1
114
115 gp("---- nx_fabric_flow R1 gate: passed " as *u8); gn(pass); gp(" / " as *u8); gn(tot); gp("\n" as *u8)
116
117 if pass == tot {
118 let lfd: i64 = sys_openat_append("knowledge/status/fabric_nx_fabric_flow.log" as *u8, 0x1a4)
119 if lfd >= 0 {
120 sys_write(lfd, "R1-FABRIC-FLOW organ=nx_fabric_flow checks=" as *u8, 43)
121 fdn(lfd, pass); sys_write(lfd, "/" as *u8, 1); fdn(lfd, tot)
122 sys_write(lfd, " lossless+bounded+NC1/2/3 verdict=GREEN\n" as *u8, 40)
123 sys_close(lfd)
124 }
125 gp("R1 LIVE GREEN -- deterministic lossless flow control MEASURED-EXCEEDS uncontrolled\n" as *u8)
126 sys_exit(0)
127 }
128 let rfd: i64 = sys_openat_append("knowledge/status/fabric_nx_fabric_flow.log" as *u8, 0x1a4)
129 if rfd >= 0 {
130 sys_write(rfd, "R1-FABRIC-FLOW organ=nx_fabric_flow checks=" as *u8, 43)
131 fdn(rfd, pass); sys_write(rfd, "/" as *u8, 1); fdn(rfd, tot)
132 sys_write(rfd, " verdict=RED\n" as *u8, 13)
133 sys_close(rfd)
134 }
135 sys_exit(1)
136 return 0
137}