nx_sched_qbv_test.nx source

1// nx_sched_qbv_test.nx -- 1:1 KAT for the TSN-Qbv bounded scheduler 2// (nx_sched_qbv.nx). Proves: gate timing, the guard band (best-effort 3// refused if it would cross the critical slice), and the two load-bearing 4// guarantees -- (1) the swept worst-case critical wait EQUALS the analytic 5// bound (cycle - slice), and (2) any best-effort frame allowed to start 6// NEVER overlaps the critical slice (the slice is protected). 7// 8// expect_exit: 0 9// license_tier: ORIGINAL 10 11import "nx_sched_qbv.nx" 12 13func main() -> i64 { 14 let s: *QbvSchedule = sys_mmap(QBV_SCHED_BYTES) as *QbvSchedule 15 qbv_init(s, 1000, 200, 300, 100) // cycle 1000us, crit [200,500), max frame 100us 16 let cs: i64 = 200 17 let ce: i64 = 500 18 let cyc: i64 = 1000 19 20 // ---- T1: critical gate timing ---- 21 if qbv_crit_open(s, 199) != 0 { return 1 } 22 if qbv_crit_open(s, 200) != 1 { return 2 } 23 if qbv_crit_open(s, 499) != 1 { return 3 } 24 if qbv_crit_open(s, 500) != 0 { return 4 } 25 26 // ---- T2: best-effort guard band ---- 27 if qbv_be_can_start(s, 100, 100) != 1 { return 5 } // [100,200) fits before -> ok 28 if qbv_be_can_start(s, 150, 100) != 0 { return 6 } // [150,250) would overrun -> refused 29 if qbv_be_can_start(s, 200, 10) != 0 { return 7 } // inside critical -> refused 30 if qbv_be_can_start(s, 500, 100) != 1 { return 8 } // [500,600) after critical -> ok 31 if qbv_be_can_start(s, 950, 100) != 0 { return 9 } // [950,1050) overruns cycle -> refused 32 33 // ---- T3: worst-case critical wait == analytic bound, and <= one cycle ---- 34 var maxw: i64 = 0 35 var t: i64 = 0 36 while t < cyc { 37 let w: i64 = qbv_crit_wait(s, t) 38 if w > maxw { maxw = w } 39 if w > cyc { return 10 } // never more than a full cycle 40 t = t + 1 41 } 42 if maxw != qbv_crit_worst_bound(s) { return 11 } // swept max == analytic bound 43 if qbv_crit_worst_bound(s) != (cyc - 300) { return 12 } // = 700 (cycle - slice) 44 45 // ---- T4: any allowed best-effort frame never overlaps the critical slice ---- 46 let mf: i64 = 100 47 t = 0 48 while t < cyc { 49 if qbv_be_can_start(s, t, mf) == 1 { 50 // frame occupies [t, t+mf); must NOT overlap [cs, ce) 51 if t < ce { if (t + mf) > cs { return 13 } } // overlap detected -> guard FAILED 52 } 53 t = t + 1 54 } 55 56 sys_write(1, "QBV KAT PASS (gate timing + guard band + worst-case critical wait == bound 700us + slice never overrun)\n", 103) 57 return 0 58}