code wiki / _hdl_build / nx_apex_gcc_bench.nx
nx_apex_gcc_bench.nx source
↩ module page · 249 lines · 12583 B
1// nx_apex_gcc_bench.nx -- APEX RUNG 1: FAIR head-to-head vs gcc -O3.
2//
3// EXTENDS runtime/nx_eqsat_vs_gcc_battery_test.nx (global rule #15: reuse, don't
4// reinvent). Same 8-kernel fixed battery, same FAIR deduped op-count metric, but
5// ALSO emits the EQUIVALENCE-CERTIFICATE axis the rung-1 brief requires: prov ON,
6// every merge cited through the single nx_eqsat_union_cited chokepoint; after
7// saturation we verify every logged rule_id is in the proven-sound allow-list
8// {1..10} and prov_overflow==0. A RULE_NONE (0) or overflow POISONS the cert.
9//
10// TWO AXES, reported separately:
11// AXIS A (op-count): deduped arithmetic-node count of the extracted min-cost
12// form, vs the arithmetic ops in gcc -O3 -S of the SAME
13// computation (counted by the FROZEN LEA rule, see bench .c).
14// AXIS B (verified-equivalence): membership-proof certificate -- gcc has none.
15//
16// METRIC NOTE: op-count is ONE-PER-ARITHMETIC-INSTRUCTION on both sides; MUL is
17// NOT double-charged. The internal class_cost (mul=3, div=30) is the EXTRACTION
18// objective only and is reported for context, never as the head-to-head number.
19//
20// Output per kernel: "<id> <emit_total> <arith_ops> <cost> <root_op> <sat> <cert>"
21// cert = 1 PROVEN-EQUIVALENT (all merges cited 1..10, no overflow), 0 POISONED.
22
23import "nx_eqsat.nx"
24import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc)
25const K_MAGIC_4096: i64 = 4096
26
27// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer
28// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the
29// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls).
30// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign.
31func _emit_num(v: i64) -> i64 { nxi_out(v); return 0 }
32func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
33
34// Structural equality of two emitted subtrees (recursive; small DAGs).
35func _emit_eq(out: *NxEmitNode, i: i64, j: i64) -> i64 {
36 if i == j { return 1 }
37 if out[i].op != out[j].op { return 0 }
38 if out[i].payload != out[j].payload { return 0 }
39 let ci0: i64 = out[i].c0; let cj0: i64 = out[j].c0
40 let ci1: i64 = out[i].c1; let cj1: i64 = out[j].c1
41 let ci2: i64 = out[i].c2; let cj2: i64 = out[j].c2
42 if ci0 < 0 { if cj0 >= 0 { return 0 } } else { if cj0 < 0 { return 0 } else { if _emit_eq(out, ci0, cj0) == 0 { return 0 } } }
43 if ci1 < 0 { if cj1 >= 0 { return 0 } } else { if cj1 < 0 { return 0 } else { if _emit_eq(out, ci1, cj1) == 0 { return 0 } } }
44 if ci2 < 0 { if cj2 >= 0 { return 0 } } else { if cj2 < 0 { return 0 } else { if _emit_eq(out, ci2, cj2) == 0 { return 0 } } }
45 return 1
46}
47
48// FAIR deduped arithmetic-op count: count an arith node only if no structurally
49// equal earlier node exists. nx_eqsat_emit re-emits shared children (post-order
50// TREE of a DAG), so dedup is mandatory to compare apples-to-apples with gcc's
51// CSE'd asm (a shared (a+b) counts ONCE, like gcc's single leaq).
52func _arith_ops(out: *NxEmitNode, cnt: i64) -> i64 {
53 var k: i64 = 0; var a: i64 = 0
54 while k < cnt {
55 let op: i64 = out[k].op
56 if op != NX_EQ_OP_CONST {
57 if op != NX_EQ_OP_VAR {
58 var seen: i64 = 0; var j: i64 = 0
59 while j < k {
60 if out[j].op != NX_EQ_OP_CONST {
61 if out[j].op != NX_EQ_OP_VAR {
62 if _emit_eq(out, j, k) == 1 { seen = 1; j = k }
63 }
64 }
65 j = j + 1
66 }
67 if seen == 0 { a = a + 1 }
68 }
69 }
70 k = k + 1
71 }
72 return a
73}
74
75// AXIS B: verify the membership-proof certificate. After saturation, EVERY logged
76// rule_id must be in the proven-sound allow-list {1..10}; a RULE_NONE (0) sentinel
77// or a prov overflow POISONS the certificate (fail-closed). Returns 1 PROVEN, 0
78// POISONED. This is the CompCert-class no-miscompiles axis gcc structurally lacks.
79func _cert_ok(g: *NxEGraph) -> i64 {
80 if g.prov_overflow != 0 { return 0 }
81 var i: i64 = 0
82 while i < g.n_prov {
83 let rid: i64 = g.prov[i]
84 // allow-list: 1 <= rid <= NX_EQSAT_RULE_N-1 (ADD_ZERO..SHIFT_MERGE). 0 =
85 // RULE_NONE = poison. SHIFT_MERGE (11) is admitted ONLY because its W=8 two-
86 // witness soundness battery + i+j>=W boundary-unsound proof certify it in
87 // nx_rule_soundness/membership-proof BEFORE the live engine cites it (the same
88 // discipline that admitted xor_self/mul_pow2). Widened from CONSTFOLD(10) to
89 // NX_EQSAT_RULE_N-1 so the allow-list tracks the engine's single source of truth.
90 if rid < NX_EQSAT_RULE_ADD_ZERO { return 0 }
91 if rid > (NX_EQSAT_RULE_N - 1) { return 0 }
92 i = i + 1
93 }
94 return 1
95}
96
97func _report(id: i64, g: *NxEGraph, root: i64) -> i64 {
98 let s: i64 = nx_eqsat_saturate(g, 64)
99 var sat: i64 = s
100 if s < 0 {
101 if s != (0 - NX_EQSAT_STEP_BUDGET) { sys_exit(40 + id); return 40 + id }
102 sat = NX_EQSAT_STEP_BUDGET
103 }
104 if nx_eqsat_recompute_best(g) != NX_EQSAT_OK { sys_exit(60 + id); return 60 + id }
105 let cost: i64 = nx_eqsat_best_cost(g, root)
106 let out: *NxEmitNode = sys_mmap(256 * 40) as *NxEmitNode
107 let cnt: *i64 = sys_mmap(8) as *i64
108 cnt[0] = 0
109 let r: i64 = nx_eqsat_emit(g, root, out, 256, cnt)
110 if r < 0 { sys_exit(80 + id); return 80 + id }
111 let total: i64 = cnt[0]
112 let arith: i64 = _arith_ops(out, total)
113 let rop: i64 = out[r].op
114 let cert: i64 = _cert_ok(g)
115 _emit_num(id); _emit_num(total); _emit_num(arith); _emit_num(cost); _emit_num(rop); _emit_num(sat); _emit_num(cert); _nl()
116 return arith
117}
118
119// Build the DSL rule table: the 7 byte-equivalent builtins (add_zero..mul_pow2)
120// PLUS the CERTIFIED shift-merge row (shape (d), id 11). The shift-merge row is the
121// payoff: it closes the K3/K6 chained-shift LAPP. It is DATA -- one NxDslRule row,
122// authored exactly like xor_self in nx_eqsat_dsl_parity_test.nx (RHS computes i+j),
123// admitted only after the soundness battery passes. lhs_op=SHL, a_kind=DSL_VAR (?x),
124// b_kind=DSL_VAR (the OUTER shift slot; the matcher reads ?j from it), rhs_kind=
125// RHS_SHL_A_BY_IADDED_J, side_cond=SC_SHIFT_MERGE_IJW (the i+j<W guard + shape-(d)
126// selector), count_mode=CNT_REAL_MERGE (idempotent -> converges to SATURATED),
127// dual_order=0 (SHL is non-commutative: only SHL(SHL(x,i),j) matches).
128func _mk_apex_table() -> *NxDslRule {
129 let table: *NxDslRule = sys_mmap(16 * 96) as *NxDslRule
130 let n: i64 = nx_eqsat_builtin_dsl_table(table)
131 nx_eqsat_dsl_set_row(table, n, NX_EQSAT_RULE_SHIFT_MERGE, NX_EQ_OP_SHL,
132 DSL_VAR, 0, DSL_VAR, 0,
133 RHS_SHL_A_BY_IADDED_J, 0,
134 SC_SHIFT_MERGE_IJW, CNT_REAL_MERGE, 0)
135 return table
136}
137
138// Fresh e-graph with const-fold AND provenance (prov) armed so the certificate
139// axis is live, AND the DSL rule table (7 builtins + certified shift-merge) loaded
140// so shape (d) can fire. prov buffer is caller-owned (rule: defensive at
141// boundaries). Enabling the DSL table is behaviorally identical to the inline path
142// for the 6 MEET kernels (proven by nx_eqsat_dsl_parity_test.nx); it ONLY ADDS the
143// shift-merge rewrite, which fires solely on the K3/K6 nested-SHL subterms.
144func _fresh() -> *NxEGraph {
145 let nodes: *NxENode = sys_mmap(512 * 128) as *NxENode
146 let classes: *NxEClass = sys_mmap(512 * 64) as *NxEClass
147 let g: *NxEGraph = sys_mmap(256) as *NxEGraph
148 if nx_eqsat_init(g, nodes, 512, classes, 512) != NX_EQSAT_OK { sys_exit(20); }
149 if nx_eqsat_enable_constfold(g) < 0 { sys_exit(21); }
150 let prov: *i64 = sys_mmap(K_MAGIC_4096 * 8) as *i64
151 if nx_eqsat_enable_prov(g, prov, K_MAGIC_4096) != NX_EQSAT_OK { sys_exit(22); }
152 let table: *NxDslRule = _mk_apex_table()
153 if nx_eqsat_enable_dsl(g, table, 8, 16) != NX_EQSAT_OK { sys_exit(23); }
154 return g
155}
156
157func main() -> i64 {
158 // K1: y = x*8 -> shl x 3
159 let g1: *NxEGraph = _fresh()
160 let x1: i64 = nx_eqsat_add_var(g1, 0)
161 let c8: i64 = nx_eqsat_add_const(g1, 8)
162 let k1: i64 = nx_eqsat_add_binary(g1, NX_EQ_OP_MUL, x1, c8)
163 let a1: i64 = _report(1, g1, k1)
164
165 // K2: y = (a+b)*(a+b) -> t=a+b; t*t (CSE: one add, one mul)
166 let g2: *NxEGraph = _fresh()
167 let a_2: i64 = nx_eqsat_add_var(g2, 0)
168 let b_2: i64 = nx_eqsat_add_var(g2, 1)
169 let s2: i64 = nx_eqsat_add_binary(g2, NX_EQ_OP_ADD, a_2, b_2)
170 let k2: i64 = nx_eqsat_add_binary(g2, NX_EQ_OP_MUL, s2, s2)
171 let a2: i64 = _report(2, g2, k2)
172
173 // K3: y = x*2 + x*2 -> shl x 2
174 let g3: *NxEGraph = _fresh()
175 let x3: i64 = nx_eqsat_add_var(g3, 0)
176 let c2: i64 = nx_eqsat_add_const(g3, 2)
177 let m3a: i64 = nx_eqsat_add_binary(g3, NX_EQ_OP_MUL, x3, c2)
178 let m3b: i64 = nx_eqsat_add_binary(g3, NX_EQ_OP_MUL, x3, c2)
179 let k3: i64 = nx_eqsat_add_binary(g3, NX_EQ_OP_ADD, m3a, m3b)
180 let a3: i64 = _report(3, g3, k3)
181
182 // K4: y = (x + 0) * 1 -> x (0 arith ops)
183 let g4: *NxEGraph = _fresh()
184 let x4: i64 = nx_eqsat_add_var(g4, 0)
185 let z4: i64 = nx_eqsat_add_const(g4, 0)
186 let o4: i64 = nx_eqsat_add_const(g4, 1)
187 let p4: i64 = nx_eqsat_add_binary(g4, NX_EQ_OP_ADD, x4, z4)
188 let k4: i64 = nx_eqsat_add_binary(g4, NX_EQ_OP_MUL, p4, o4)
189 let a4: i64 = _report(4, g4, k4)
190
191 // K5: y = (x - x) + (a & a) -> a (0 arith ops)
192 let g5: *NxEGraph = _fresh()
193 let x5: i64 = nx_eqsat_add_var(g5, 0)
194 let a_5: i64 = nx_eqsat_add_var(g5, 1)
195 let ss5: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_SUB, x5, x5)
196 let aa5: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_AND, a_5, a_5)
197 let k5: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_ADD, ss5, aa5)
198 let a5: i64 = _report(5, g5, k5)
199
200 // K6: y = (x*4) * 8 -> shl x 5
201 let g6: *NxEGraph = _fresh()
202 let x6: i64 = nx_eqsat_add_var(g6, 0)
203 let c4: i64 = nx_eqsat_add_const(g6, 4)
204 let c8b: i64 = nx_eqsat_add_const(g6, 8)
205 let m6: i64 = nx_eqsat_add_binary(g6, NX_EQ_OP_MUL, x6, c4)
206 let k6: i64 = nx_eqsat_add_binary(g6, NX_EQ_OP_MUL, m6, c8b)
207 let a6: i64 = _report(6, g6, k6)
208
209 // K7: y = a + (a + a) -> a*3 form (add_self: a+a -> shl a 1)
210 let g7: *NxEGraph = _fresh()
211 let a_7: i64 = nx_eqsat_add_var(g7, 0)
212 let inner7: i64 = nx_eqsat_add_binary(g7, NX_EQ_OP_ADD, a_7, a_7)
213 let k7: i64 = nx_eqsat_add_binary(g7, NX_EQ_OP_ADD, a_7, inner7)
214 let a7: i64 = _report(7, g7, k7)
215
216 // K8: y = 6 + 7 -> 13 (0 arith ops)
217 let g8: *NxEGraph = _fresh()
218 let c6: i64 = nx_eqsat_add_const(g8, 6)
219 let c7: i64 = nx_eqsat_add_const(g8, 7)
220 let k8: i64 = nx_eqsat_add_binary(g8, NX_EQ_OP_ADD, c6, c7)
221 let a8: i64 = _report(8, g8, k8)
222
223 // K9 (PHASE-ORDERING probe): y = ((x << 2) << 3) << 1. A triply-nested constant
224 // shift the e-graph must collapse by applying shift-merge across the chain in
225 // ANY association order (equality saturation explores them ALL simultaneously):
226 // inner ((x<<2)<<3) -shift_merge-> (x<<5)
227 // then ((x<<5)<<1) -shift_merge-> (x<<6) == 1 arith op
228 // The structural claim TESTED: does the e-graph's no-phase-ordering search beat
229 // gcc -O3's fixed pipeline here? HONEST RESULT (reported, NOT cherry-picked):
230 // gcc 13 -O3 ALSO folds ((x<<2)<<3)<<1 to a single `salq $6` -- its shift-merge /
231 // reassociation runs to fixpoint inside the basic block and there is only ONE
232 // productive order, so the e-graph's order-independence gives NO edge. This is
233 // COMPETITIVE (ours 1 == gcc 1), NOT a genuine op-count WIN. It proves the engine
234 // collapses the nested chain to the same minimum gcc reaches (no LAPP), and
235 // documents -- honestly -- that a true phase-ordering EXCEED needs a case where
236 // gcc's pipeline commits early to a form that blocks a later cheaper rewrite. We
237 // did NOT manufacture such a case; we report the measured COMPETITIVE truth.
238 let g9: *NxEGraph = _fresh()
239 let x9: i64 = nx_eqsat_add_var(g9, 0)
240 let c2b: i64 = nx_eqsat_add_const(g9, 2)
241 let sh9a: i64 = nx_eqsat_add_binary(g9, NX_EQ_OP_SHL, x9, c2b) // x<<2
242 let c3b: i64 = nx_eqsat_add_const(g9, 3)
243 let sh9b: i64 = nx_eqsat_add_binary(g9, NX_EQ_OP_SHL, sh9a, c3b) // (x<<2)<<3
244 let c1b: i64 = nx_eqsat_add_const(g9, 1)
245 let k9: i64 = nx_eqsat_add_binary(g9, NX_EQ_OP_SHL, sh9b, c1b) // ((x<<2)<<3)<<1
246 let a9: i64 = _report(9, g9, k9)
247
248 return 0
249}