lib/pluck/src/profiling/internal/incremental.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const Allocator = std.mem.Allocator;
3
4 const pluck = @import("pluck");
5 const bdd = pluck.bdd;
6 const Manager = bdd.Manager;
7 const Bdd = bdd.Bdd;
8 const WmcParams = bdd.WmcParams;
9 const WmcContext = bdd.WmcContext;
10 const VarLabel = bdd.VarLabel;
11 const bench_util = @import("util.zig");
12
13 const evaluator = pluck.evaluator;
14 const lpsmc_module = pluck.lpsmc;
15 const runtime = pluck.runtime;
16 const pexpr = pluck.pexpr;
17
18 fn buildXorChain(manager: *Manager, n: usize) !Bdd {
19 if (n == 0) return Bdd.FALSE;
20
21 var result = try manager.newVar(true);
22 for (1..n) |_| {
23 const v = try manager.newVar(true);
24 result = try manager.bddXor(result, v);
25 }
26 return result;
27 }
28
29 fn buildAndChain(manager: *Manager, n: usize) !Bdd {
30 if (n == 0) return Bdd.TRUE;
31
32 var result = try manager.newVar(true);
33 for (1..n) |_| {
34 const v = try manager.newVar(true);
35 result = try manager.bddAnd(result, v);
36 }
37 return result;
38 }
39
40 fn buildMixedFormula(manager: *Manager, n: usize) !Bdd {
41 if (n < 2) return try manager.newVar(true);
42
43 var result = Bdd.FALSE;
44 var i: usize = 0;
45 while (i + 1 < n) : (i += 2) {
46 const a = try manager.newVar(true);
47 const b = try manager.newVar(true);
48 const clause = try manager.bddAnd(a, b);
49 result = try manager.bddOr(result, clause);
50 }
51 if (n % 2 == 1) {
52 const last = try manager.newVar(true);
53 result = try manager.bddOr(result, last);
54 }
55 return result;
56 }
57
58 test "BENCHMARK: WmcContext persistent cache scaling" {
59 const benchmark_latency = bench_util.benchmarkScope("WmcContext persistent cache scaling");
60 defer benchmark_latency.end();
61 const allocator = bench_util.allocator();
62 const bench = bench_util.BenchConfig.init();
63
64 bench_util.stdout("\n=== Benchmark 1: WmcContext Persistent Cache ===\n", .{});
65 bench_util.stdout("benchmark,num_vars,bdd_size,num_queries,baseline_ns,incremental_ns,speedup,hit_rate\n", .{});
66
67 const var_counts = [_]usize{ 10, 15, 20, 25 };
68 const query_counts = [_]usize{ 1, 10, 50, 100 };
69 const var_len = bench.limit(var_counts.len, 1);
70 const query_len = bench.limit(query_counts.len, 2);
71 const iterations = bench.iters(5, 1);
72
73 for (var_counts[0..var_len]) |num_vars| {
74 var manager = try Manager.init(allocator);
75 defer manager.deinit();
76
77 const formula = try buildXorChain(&manager, num_vars);
78 const bdd_size = manager.size(formula);
79
80 var params = WmcParams.init(allocator);
81 defer params.deinit();
82 for (0..num_vars) |v| {
83 try params.setWeight(@intCast(v), 0.3, 0.7);
84 }
85
86 for (query_counts[0..query_len]) |num_queries| {
87 var baseline_total: i128 = 0;
88 for (0..iterations) |_| {
89 const start = bench_util.nowNs();
90 for (0..num_queries) |_| {
91 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
92 }
93 baseline_total += bench_util.elapsedNsAccum(start);
94 }
95 const baseline_ns: u64 = @intCast(@divFloor(baseline_total, iterations));
96
97 var context = WmcContext.init(allocator);
98 defer context.deinit();
99
100 var incremental_total: i128 = 0;
101 for (0..iterations) |_| {
102 context.clear();
103 const start = bench_util.nowNs();
104 for (0..num_queries) |_| {
105 _ = context.wmcCached(&manager, formula, ¶ms);
106 }
107 incremental_total += bench_util.elapsedNsAccum(start);
108 }
109 const incremental_ns: u64 = @intCast(@divFloor(incremental_total, iterations));
110
111 const speedup = @as(f64, @floatFromInt(baseline_ns)) / @as(f64, @floatFromInt(@max(incremental_ns, 1)));
112 const stats = context.getStats();
113
114 bench_util.stdout("WmcContext,{d},{d},{d},{d},{d},{d:.2},{d:.2}\n", .{
115 num_vars,
116 bdd_size,
117 num_queries,
118 baseline_ns,
119 incremental_ns,
120 speedup,
121 stats.hitRate() * 100,
122 });
123 }
124 }
125 }
126
127 test "BENCHMARK: conditionHelper cache scaling" {
128 const benchmark_latency = bench_util.benchmarkScope("conditionHelper cache scaling");
129 defer benchmark_latency.end();
130 const allocator = bench_util.allocator();
131 const bench = bench_util.BenchConfig.init();
132
133 bench_util.stdout("\n=== Benchmark 2: Condition Cache (XOR chain) ===\n", .{});
134 bench_util.stdout("benchmark,num_vars,bdd_size,condition_ns,nodes_per_ns\n", .{});
135
136 const var_counts = [_]usize{ 10, 15, 20, 22, 24, 25 };
137 const var_len = bench.limit(var_counts.len, 2);
138 const iterations = bench.iters(10, 2);
139
140 for (var_counts[0..var_len]) |num_vars| {
141 var manager = try Manager.init(allocator);
142 defer manager.deinit();
143
144 const formula = try buildXorChain(&manager, num_vars);
145 const bdd_size = manager.size(formula);
146
147 const var_to_condition: VarLabel = @intCast(num_vars - 1);
148
149 var total_ns: i128 = 0;
150 for (0..iterations) |_| {
151 const start = bench_util.nowNs();
152 _ = try manager.condition(formula, var_to_condition, true);
153 total_ns += bench_util.elapsedNsAccum(start);
154 }
155 const avg_ns: u64 = @intCast(@divFloor(total_ns, iterations));
156 const nodes_per_ns = @as(f64, @floatFromInt(bdd_size)) / @as(f64, @floatFromInt(@max(avg_ns, 1))) * 1000;
157
158 bench_util.stdout("ConditionCache,{d},{d},{d},{d:.2}\n", .{
159 num_vars,
160 bdd_size,
161 avg_ns,
162 nodes_per_ns,
163 });
164 }
165 }
166
167 test "BENCHMARK: multi-step conditioning sequence" {
168 const benchmark_latency = bench_util.benchmarkScope("multi-step conditioning sequence");
169 defer benchmark_latency.end();
170 const allocator = bench_util.allocator();
171 const bench = bench_util.BenchConfig.init();
172
173 bench_util.stdout("\n=== Benchmark 3: Multi-Step Conditioning Sequence ===\n", .{});
174 bench_util.stdout("benchmark,num_vars,num_steps,baseline_ns,incremental_ns,speedup\n", .{});
175
176 const var_counts = [_]usize{ 15, 20, 25 };
177 const step_counts = [_]usize{ 1, 3, 5, 8, 10 };
178 const var_len = bench.limit(var_counts.len, 1);
179 const step_len = bench.limit(step_counts.len, 2);
180 const iterations = bench.iters(3, 1);
181
182 for (var_counts[0..var_len]) |num_vars| {
183 var manager = try Manager.init(allocator);
184 defer manager.deinit();
185
186 const formula = try buildMixedFormula(&manager, num_vars);
187
188 var params = WmcParams.init(allocator);
189 defer params.deinit();
190 for (0..num_vars) |v| {
191 try params.setWeight(@intCast(v), 0.5, 0.5);
192 }
193
194 for (step_counts[0..step_len]) |num_steps| {
195 if (num_steps > num_vars) continue;
196
197 var baseline_total: i128 = 0;
198 for (0..iterations) |_| {
199 var current = formula;
200 const start = bench_util.nowNs();
201 for (0..num_steps) |step| {
202 current = try manager.condition(current, @intCast(step), true);
203 _ = bdd.wmcWithAllocator(&manager, current, ¶ms, allocator);
204 }
205 baseline_total += bench_util.elapsedNsAccum(start);
206 }
207 const baseline_ns: u64 = @intCast(@divFloor(baseline_total, iterations));
208
209 var incremental_total: i128 = 0;
210 for (0..iterations) |_| {
211 var context = WmcContext.init(allocator);
212 defer context.deinit();
213
214 var current = formula;
215 const start = bench_util.nowNs();
216 for (0..num_steps) |step| {
217 current = try manager.condition(current, @intCast(step), true);
218 _ = context.wmcCached(&manager, current, ¶ms);
219 }
220 incremental_total += bench_util.elapsedNsAccum(start);
221 }
222 const incremental_ns: u64 = @intCast(@divFloor(incremental_total, iterations));
223
224 const speedup = @as(f64, @floatFromInt(baseline_ns)) / @as(f64, @floatFromInt(@max(incremental_ns, 1)));
225
226 bench_util.stdout("MultiStep,{d},{d},{d},{d},{d:.2}\n", .{
227 num_vars,
228 num_steps,
229 baseline_ns,
230 incremental_ns,
231 speedup,
232 });
233 }
234 }
235 }
236
237 test "BENCHMARK: BDD complexity scaling" {
238 const benchmark_latency = bench_util.benchmarkScope("BDD complexity scaling");
239 defer benchmark_latency.end();
240 const allocator = bench_util.allocator();
241 const bench = bench_util.BenchConfig.init();
242
243 bench_util.stdout("\n=== Benchmark 4: BDD Complexity Scaling ===\n", .{});
244 bench_util.stdout("formula_type,num_vars,bdd_size,wmc_ns,nodes_per_us\n", .{});
245
246 const var_counts = [_]usize{ 10, 15, 20, 25 };
247 const var_len = bench.limit(var_counts.len, 1);
248 const iterations = bench.iters(5, 1);
249
250 for (var_counts[0..var_len]) |num_vars| {
251 const formula_types = [_][]const u8{ "AND", "OR", "XOR", "MIXED" };
252
253 for (formula_types) |formula_type| {
254 var manager = try Manager.init(allocator);
255 defer manager.deinit();
256
257 const formula = if (std.mem.eql(u8, formula_type, "AND"))
258 try buildAndChain(&manager, num_vars)
259 else if (std.mem.eql(u8, formula_type, "OR"))
260 try buildOrChain(&manager, num_vars)
261 else if (std.mem.eql(u8, formula_type, "XOR"))
262 try buildXorChain(&manager, num_vars)
263 else
264 try buildMixedFormula(&manager, num_vars);
265
266 const bdd_size = manager.size(formula);
267
268 var params = WmcParams.init(allocator);
269 defer params.deinit();
270 for (0..num_vars) |v| {
271 try params.setWeight(@intCast(v), 0.5, 0.5);
272 }
273
274 var total_ns: i128 = 0;
275 for (0..iterations) |_| {
276 const start = bench_util.nowNs();
277 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
278 total_ns += bench_util.elapsedNsAccum(start);
279 }
280 const avg_ns: u64 = @intCast(@divFloor(total_ns, iterations));
281 const nodes_per_us = @as(f64, @floatFromInt(bdd_size)) / @as(f64, @floatFromInt(@max(avg_ns, 1))) * 1000;
282
283 bench_util.stdout("{s},{d},{d},{d},{d:.2}\n", .{
284 formula_type,
285 num_vars,
286 bdd_size,
287 avg_ns,
288 nodes_per_us,
289 });
290 }
291 }
292 }
293
294 fn buildOrChain(manager: *Manager, n: usize) !Bdd {
295 if (n == 0) return Bdd.FALSE;
296
297 var result = try manager.newVar(true);
298 for (1..n) |_| {
299 const v = try manager.newVar(true);
300 result = try manager.bddOr(result, v);
301 }
302 return result;
303 }
304
305 test "BENCHMARK: WmcContext cache invalidation" {
306 const benchmark_latency = bench_util.benchmarkScope("WmcContext cache invalidation");
307 defer benchmark_latency.end();
308 const allocator = bench_util.allocator();
309 const bench = bench_util.BenchConfig.init();
310
311 bench_util.stdout("\n=== Benchmark 5: WmcContext Cache Invalidation ===\n", .{});
312 bench_util.stdout("benchmark,num_vars,invalidation_type,queries_before,queries_after,total_ns,hit_rate_after\n", .{});
313
314 const var_counts = [_]usize{ 15, 20, 25 };
315 const var_len = bench.limit(var_counts.len, 1);
316 const iterations = bench.iters(5, 1);
317 const query_reps = bench.value(50, 10);
318
319 for (var_counts[0..var_len]) |num_vars| {
320 var manager = try Manager.init(allocator);
321 defer manager.deinit();
322
323 const formula = try buildMixedFormula(&manager, num_vars);
324
325 var params = WmcParams.init(allocator);
326 defer params.deinit();
327 for (0..num_vars) |v| {
328 try params.setWeight(@intCast(v), 0.5, 0.5);
329 }
330
331 {
332 var total_ns: i128 = 0;
333 var final_hit_rate: f64 = 0;
334 for (0..iterations) |_| {
335 var context = WmcContext.init(allocator);
336 defer context.deinit();
337
338 const start = bench_util.nowNs();
339
340 for (0..query_reps) |_| {
341 _ = context.wmcCached(&manager, formula, ¶ms);
342 }
343
344 context.invalidateWeights();
345
346 for (0..query_reps) |_| {
347 _ = context.wmcCached(&manager, formula, ¶ms);
348 }
349 total_ns += bench_util.elapsedNsAccum(start);
350 final_hit_rate = context.getStats().hitRate();
351 }
352 const avg_ns: u64 = @intCast(@divFloor(total_ns, iterations));
353
354 bench_util.stdout("WmcContext,{d},invalidateWeights,{d},{d},{d},{d:.2}\n", .{
355 num_vars,
356 query_reps,
357 query_reps,
358 avg_ns,
359 final_hit_rate * 100,
360 });
361 }
362
363 {
364 var total_ns: i128 = 0;
365 var final_hit_rate: f64 = 0;
366 for (0..iterations) |_| {
367 var context = WmcContext.init(allocator);
368 defer context.deinit();
369
370 const start = bench_util.nowNs();
371
372 for (0..query_reps) |_| {
373 _ = context.wmcCached(&manager, formula, ¶ms);
374 }
375
376 context.invalidateAll();
377
378 for (0..query_reps) |_| {
379 _ = context.wmcCached(&manager, formula, ¶ms);
380 }
381 total_ns += bench_util.elapsedNsAccum(start);
382 final_hit_rate = context.getStats().hitRate();
383 }
384 const avg_ns: u64 = @intCast(@divFloor(total_ns, iterations));
385
386 bench_util.stdout("WmcContext,{d},invalidateAll,{d},{d},{d},{d:.2}\n", .{
387 num_vars,
388 query_reps,
389 query_reps,
390 avg_ns,
391 final_hit_rate * 100,
392 });
393 }
394
395 {
396 var total_ns: i128 = 0;
397 var final_hit_rate: f64 = 0;
398 for (0..iterations) |_| {
399 var context = WmcContext.init(allocator);
400 defer context.deinit();
401
402 const start = bench_util.nowNs();
403
404 for (0..query_reps) |_| {
405 _ = context.wmcCached(&manager, formula, ¶ms);
406 }
407
408 context.invalidateForVars(&manager, &[_]VarLabel{0});
409
410 for (0..query_reps) |_| {
411 _ = context.wmcCached(&manager, formula, ¶ms);
412 }
413 total_ns += bench_util.elapsedNsAccum(start);
414 final_hit_rate = context.getStats().hitRate();
415 }
416 const avg_ns: u64 = @intCast(@divFloor(total_ns, iterations));
417
418 bench_util.stdout("WmcContext,{d},invalidateForVars,{d},{d},{d},{d:.2}\n", .{
419 num_vars,
420 query_reps,
421 query_reps,
422 avg_ns,
423 final_hit_rate * 100,
424 });
425 }
426 }
427 }
428
429 test "BENCHMARK: larger BDD scaling" {
430 const benchmark_latency = bench_util.benchmarkScope("larger BDD scaling");
431 defer benchmark_latency.end();
432 const allocator = bench_util.allocator();
433 const bench = bench_util.BenchConfig.init();
434
435 bench_util.stdout("\n=== Benchmark 6: Larger BDD Scaling ===\n", .{});
436 bench_util.stdout("formula_type,num_vars,bdd_size,wmc_ns,condition_ns,total_nodes\n", .{});
437
438 const large_var_counts = [_]usize{ 30, 40, 50, 75, 100 };
439 const var_len = bench.limit(large_var_counts.len, 2);
440 const iterations = bench.iters(3, 1);
441
442 for (large_var_counts[0..var_len]) |num_vars| {
443 {
444 var manager = try Manager.init(allocator);
445 defer manager.deinit();
446
447 const formula = try buildAndChain(&manager, num_vars);
448 const bdd_size = manager.size(formula);
449 const total_nodes = manager.totalNodeCount();
450
451 var params = WmcParams.init(allocator);
452 defer params.deinit();
453 for (0..num_vars) |v| {
454 try params.setWeight(@intCast(v), 0.5, 0.5);
455 }
456
457 var wmc_total: i128 = 0;
458 var cond_total: i128 = 0;
459
460 for (0..iterations) |_| {
461 var start = bench_util.nowNs();
462 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
463 wmc_total += bench_util.elapsedNsAccum(start);
464
465 start = bench_util.nowNs();
466 _ = try manager.condition(formula, @intCast(num_vars / 2), true);
467 cond_total += bench_util.elapsedNsAccum(start);
468 }
469
470 const wmc_ns: u64 = @intCast(@divFloor(wmc_total, iterations));
471 const cond_ns: u64 = @intCast(@divFloor(cond_total, iterations));
472
473 bench_util.stdout("AND,{d},{d},{d},{d},{d}\n", .{
474 num_vars,
475 bdd_size,
476 wmc_ns,
477 cond_ns,
478 total_nodes,
479 });
480 }
481
482 {
483 var manager = try Manager.init(allocator);
484 defer manager.deinit();
485
486 const formula = try buildMixedFormula(&manager, num_vars);
487 const bdd_size = manager.size(formula);
488 const total_nodes = manager.totalNodeCount();
489
490 var params = WmcParams.init(allocator);
491 defer params.deinit();
492 for (0..num_vars) |v| {
493 try params.setWeight(@intCast(v), 0.5, 0.5);
494 }
495
496 var wmc_total: i128 = 0;
497 var cond_total: i128 = 0;
498
499 for (0..iterations) |_| {
500 var start = bench_util.nowNs();
501 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
502 wmc_total += bench_util.elapsedNsAccum(start);
503
504 start = bench_util.nowNs();
505 _ = try manager.condition(formula, @intCast(num_vars / 2), true);
506 cond_total += bench_util.elapsedNsAccum(start);
507 }
508
509 const wmc_ns: u64 = @intCast(@divFloor(wmc_total, iterations));
510 const cond_ns: u64 = @intCast(@divFloor(cond_total, iterations));
511
512 bench_util.stdout("MIXED,{d},{d},{d},{d},{d}\n", .{
513 num_vars,
514 bdd_size,
515 wmc_ns,
516 cond_ns,
517 total_nodes,
518 });
519 }
520 }
521 }
522
523 test "BENCHMARK: WmcContext at larger scales" {
524 const benchmark_latency = bench_util.benchmarkScope("WmcContext at larger scales");
525 defer benchmark_latency.end();
526 const allocator = bench_util.allocator();
527 const bench = bench_util.BenchConfig.init();
528
529 bench_util.stdout("\n=== Benchmark 7: WmcContext at Larger Scales ===\n", .{});
530 bench_util.stdout("api,num_vars,queries,baseline_ns,incremental_ns,speedup\n", .{});
531
532 const large_var_counts = [_]usize{ 30, 50, 75, 100 };
533 const var_len = bench.limit(large_var_counts.len, 1);
534 const iterations = bench.iters(3, 1);
535 const query_reps = bench.value(100, 20);
536
537 for (large_var_counts[0..var_len]) |num_vars| {
538 var manager = try Manager.init(allocator);
539 defer manager.deinit();
540
541 const formula = try buildMixedFormula(&manager, num_vars);
542
543 var params = WmcParams.init(allocator);
544 defer params.deinit();
545 for (0..num_vars) |v| {
546 try params.setWeight(@intCast(v), 0.4, 0.6);
547 }
548
549 {
550 var baseline_total: i128 = 0;
551 var incremental_total: i128 = 0;
552
553 for (0..iterations) |_| {
554 var start = bench_util.nowNs();
555 for (0..query_reps) |_| {
556 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
557 }
558 baseline_total += bench_util.elapsedNsAccum(start);
559
560 var context = WmcContext.init(allocator);
561 defer context.deinit();
562 start = bench_util.nowNs();
563 for (0..query_reps) |_| {
564 _ = context.wmcCached(&manager, formula, ¶ms);
565 }
566 incremental_total += bench_util.elapsedNsAccum(start);
567 }
568
569 const baseline_ns: u64 = @intCast(@divFloor(baseline_total, iterations));
570 const incremental_ns: u64 = @intCast(@divFloor(incremental_total, iterations));
571 const speedup = @as(f64, @floatFromInt(baseline_ns)) / @as(f64, @floatFromInt(@max(incremental_ns, 1)));
572
573 bench_util.stdout("WmcContext,{d},{d},{d},{d},{d:.2}\n", .{
574 num_vars,
575 query_reps,
576 baseline_ns,
577 incremental_ns,
578 speedup,
579 });
580 }
581 }
582 }
583
584 test "BENCHMARK: XOR chain hard instances" {
585 const benchmark_latency = bench_util.benchmarkScope("XOR chain hard instances");
586 defer benchmark_latency.end();
587 const allocator = bench_util.allocator();
588 const bench = bench_util.BenchConfig.init();
589
590 bench_util.stdout("\n=== Benchmark 8: XOR Chain Hard Instances ===\n", .{});
591 bench_util.stdout("num_vars,bdd_size,total_nodes,wmc_ns,condition_ns,wmc_context_speedup\n", .{});
592
593 const xor_var_counts = [_]usize{ 10, 15, 18, 20, 22, 24 };
594 const var_len = bench.limit(xor_var_counts.len, 2);
595 const iterations = bench.iters(3, 1);
596 const query_reps = bench.value(10, 5);
597
598 for (xor_var_counts[0..var_len]) |num_vars| {
599 var manager = try Manager.init(allocator);
600 defer manager.deinit();
601
602 const formula = try buildXorChain(&manager, num_vars);
603 const bdd_size = manager.size(formula);
604 const total_nodes = manager.totalNodeCount();
605
606 var params = WmcParams.init(allocator);
607 defer params.deinit();
608 for (0..num_vars) |v| {
609 try params.setWeight(@intCast(v), 0.5, 0.5);
610 }
611
612 var wmc_total: i128 = 0;
613 var cond_total: i128 = 0;
614 var context_total: i128 = 0;
615 var baseline_wmc_total: i128 = 0;
616
617 for (0..iterations) |_| {
618 var start = bench_util.nowNs();
619 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
620 wmc_total += bench_util.elapsedNsAccum(start);
621
622 start = bench_util.nowNs();
623 _ = try manager.condition(formula, @intCast(num_vars - 1), true);
624 cond_total += bench_util.elapsedNsAccum(start);
625
626 start = bench_util.nowNs();
627 for (0..query_reps) |_| {
628 _ = bdd.wmcWithAllocator(&manager, formula, ¶ms, allocator);
629 }
630 baseline_wmc_total += bench_util.elapsedNsAccum(start);
631
632 var context = WmcContext.init(allocator);
633 defer context.deinit();
634 start = bench_util.nowNs();
635 for (0..query_reps) |_| {
636 _ = context.wmcCached(&manager, formula, ¶ms);
637 }
638 context_total += bench_util.elapsedNsAccum(start);
639 }
640
641 const wmc_ns: u64 = @intCast(@divFloor(wmc_total, iterations));
642 const cond_ns: u64 = @intCast(@divFloor(cond_total, iterations));
643 const baseline_ns: u64 = @intCast(@divFloor(baseline_wmc_total, iterations));
644 const context_ns: u64 = @intCast(@divFloor(context_total, iterations));
645 const speedup = @as(f64, @floatFromInt(baseline_ns)) / @as(f64, @floatFromInt(@max(context_ns, 1)));
646
647 bench_util.stdout("{d},{d},{d},{d},{d},{d:.2}\n", .{
648 num_vars,
649 bdd_size,
650 total_nodes,
651 wmc_ns,
652 cond_ns,
653 speedup,
654 });
655 }
656 }
657
658 test "BENCHMARK: ThunkDependencies tracking" {
659 const benchmark_latency = bench_util.benchmarkScope("ThunkDependencies tracking");
660 defer benchmark_latency.end();
661 const allocator = bench_util.allocator();
662 const ThunkDependencies = evaluator.ThunkDependencies;
663 const ThunkId = evaluator.ThunkId;
664 const bench = bench_util.BenchConfig.init();
665
666 bench_util.stdout("\n=== Benchmark 9: ThunkDependencies Tracking ===\n", .{});
667 bench_util.stdout("operation,num_thunks,num_vars_per_thunk,total_deps,time_ns,ops_per_us\n", .{});
668
669 const thunk_counts = [_]usize{ 10, 50, 100, 500 };
670 const vars_per_thunk = [_]usize{ 5, 10, 20 };
671 const thunk_len = bench.limit(thunk_counts.len, 1);
672 const vars_len = bench.limit(vars_per_thunk.len, 1);
673 const iterations = bench.iters(5, 1);
674
675 const makeThunkId = struct {
676 fn call(idx: usize) ThunkId {
677 return ThunkId{ .session = .{
678 .expr_ptr = idx,
679 .callstack_hash = @as(u64, idx) * 12345,
680 } };
681 }
682 }.call;
683
684 for (thunk_counts[0..thunk_len]) |num_thunks| {
685 for (vars_per_thunk[0..vars_len]) |num_vars| {
686 const total_deps = num_thunks * num_vars;
687
688 var add_total: i128 = 0;
689 for (0..iterations) |_| {
690 var deps = ThunkDependencies.init(allocator);
691 defer deps.deinit();
692
693 const start = bench_util.nowNs();
694 for (0..num_thunks) |t| {
695 const thunk_id = makeThunkId(t);
696 for (0..num_vars) |v| {
697 try deps.addDependency(thunk_id, @intCast(v));
698 }
699 }
700 add_total += bench_util.elapsedNsAccum(start);
701 }
702 const add_ns: u64 = @intCast(@divFloor(add_total, iterations));
703 const add_ops_per_us = @as(f64, @floatFromInt(total_deps)) / @as(f64, @floatFromInt(@max(add_ns, 1))) * 1000;
704
705 bench_util.stdout("addDependency,{d},{d},{d},{d},{d:.2}\n", .{
706 num_thunks,
707 num_vars,
708 total_deps,
709 add_ns,
710 add_ops_per_us,
711 });
712
713 var mark_total: i128 = 0;
714 for (0..iterations) |_| {
715 var deps = ThunkDependencies.init(allocator);
716 defer deps.deinit();
717
718 for (0..num_thunks) |t| {
719 const thunk_id = makeThunkId(t);
720 for (0..num_vars) |v| {
721 try deps.addDependency(thunk_id, @intCast(v));
722 }
723 }
724
725 const start = bench_util.nowNs();
726
727 for (0..num_vars) |v| {
728 try deps.markDirty(@intCast(v));
729 }
730 mark_total += bench_util.elapsedNsAccum(start);
731 }
732 const mark_ns: u64 = @intCast(@divFloor(mark_total, iterations));
733 const mark_ops_per_us = @as(f64, @floatFromInt(num_vars)) / @as(f64, @floatFromInt(@max(mark_ns, 1))) * 1000;
734
735 bench_util.stdout("markVariableDirty,{d},{d},{d},{d},{d:.2}\n", .{
736 num_thunks,
737 num_vars,
738 total_deps,
739 mark_ns,
740 mark_ops_per_us,
741 });
742 }
743 }
744 }
745
746 test "BENCHMARK: IncrementalLPSMC caching" {
747 const benchmark_latency = bench_util.benchmarkScope("IncrementalLPSMC caching");
748 defer benchmark_latency.end();
749 const allocator = bench_util.allocator();
750 const PathChoice = evaluator.PathChoice;
751 const VarLabelSet = evaluator.VarLabelSet;
752 const bench = bench_util.BenchConfig.init();
753
754 bench_util.stdout("\n=== Benchmark 10: IncrementalLPSMC Caching ===\n", .{});
755 bench_util.stdout("operation,num_subproblems,vars_per_subproblem,time_ns,ops_per_us\n", .{});
756
757 const subproblem_counts = [_]usize{ 10, 50, 100 };
758 const vars_per_subproblem = [_]usize{ 5, 10 };
759 const sub_len = bench.limit(subproblem_counts.len, 1);
760 const vars_len = bench.limit(vars_per_subproblem.len, 1);
761 const iterations = bench.iters(5, 1);
762 const num_lookups: usize = bench.value(100, 20);
763
764 for (subproblem_counts[0..sub_len]) |num_subproblems| {
765 for (vars_per_subproblem[0..vars_len]) |num_vars| {
766 var lpsmc_template = lpsmc_module.init(allocator);
767 defer lpsmc_module.deinit(&lpsmc_template);
768
769 for (0..num_subproblems) |subproblem_id| {
770 var deps = VarLabelSet{};
771
772 for (0..num_vars) |v| {
773 const var_label: VarLabel = @intCast((subproblem_id * num_vars + v) % 50);
774 try deps.put(allocator, var_label, {});
775
776 const entry = try lpsmc_template.var_to_subproblems.getOrPut(allocator, var_label);
777 if (!entry.found_existing) {
778 entry.value_ptr.* = .{};
779 }
780 try entry.value_ptr.put(allocator, @intCast(subproblem_id), {});
781 }
782 try lpsmc_template.path_choices.put(allocator, @intCast(subproblem_id), PathChoice{
783 .top_k_bdd = Bdd.TRUE,
784 .sampled_bdd = null,
785 .sampled_probability = 0.0,
786 .k_used = 1,
787 .ess_ratio = 1.0,
788 .depends_on_vars = deps,
789 });
790 }
791
792 const total_entries = lpsmc_template.path_choices.count();
793
794 var lookup_total: i128 = 0;
795 for (0..iterations) |_| {
796 const start = bench_util.nowNs();
797 for (0..num_lookups) |v| {
798 _ = lpsmc_module.affectsPathChoices(&lpsmc_template, @intCast(v % 50));
799 }
800 lookup_total += bench_util.elapsedNsAccum(start);
801 }
802 const lookup_ns: u64 = @intCast(@divFloor(lookup_total, iterations));
803 const lookup_ops_per_us = @as(f64, @floatFromInt(num_lookups)) / @as(f64, @floatFromInt(@max(lookup_ns, 1))) * 1000;
804
805 bench_util.stdout("affectsPathChoices,{d},{d},{d},{d:.2}\n", .{
806 total_entries,
807 num_vars,
808 lookup_ns,
809 lookup_ops_per_us,
810 });
811
812 var affected_total: i128 = 0;
813 for (0..iterations) |_| {
814 var affected_list: std.ArrayList(u32) = .empty;
815 defer affected_list.deinit(allocator);
816
817 const start = bench_util.nowNs();
818 for (0..num_lookups) |v| {
819 affected_list.clearRetainingCapacity();
820 try lpsmc_module.getAffectedSubproblems(&lpsmc_template, @intCast(v % 50), &affected_list);
821 }
822 affected_total += bench_util.elapsedNsAccum(start);
823 }
824 const affected_ns: u64 = @intCast(@divFloor(affected_total, iterations));
825 const affected_ops_per_us = @as(f64, @floatFromInt(num_lookups)) / @as(f64, @floatFromInt(@max(affected_ns, 1))) * 1000;
826
827 bench_util.stdout("getAffectedSubproblems,{d},{d},{d},{d:.2}\n", .{
828 total_entries,
829 num_vars,
830 affected_ns,
831 affected_ops_per_us,
832 });
833
834 var clear_total: i128 = 0;
835 for (0..iterations) |_| {
836 var lpsmc = lpsmc_module.init(allocator);
837
838 for (0..num_subproblems) |subproblem_id| {
839 var deps = VarLabelSet{};
840 for (0..num_vars) |v| {
841 const var_label: VarLabel = @intCast((subproblem_id * num_vars + v) % 50);
842 try deps.put(allocator, var_label, {});
843 }
844 try lpsmc.path_choices.put(allocator, @intCast(subproblem_id), PathChoice{
845 .top_k_bdd = Bdd.TRUE,
846 .sampled_bdd = null,
847 .sampled_probability = 0.0,
848 .k_used = 1,
849 .ess_ratio = 1.0,
850 .depends_on_vars = deps,
851 });
852 }
853
854 const start = bench_util.nowNs();
855 lpsmc_module.clearCaches(&lpsmc);
856 clear_total += bench_util.elapsedNsAccum(start);
857
858 lpsmc_module.deinit(&lpsmc);
859 }
860 const clear_ns: u64 = @intCast(@divFloor(clear_total, iterations));
861
862 bench_util.stdout("clearCaches,{d},{d},{d},{d:.2}\n", .{
863 total_entries,
864 num_vars,
865 clear_ns,
866 @as(f64, @floatFromInt(total_entries)) / @as(f64, @floatFromInt(@max(clear_ns, 1))) * 1000,
867 });
868 }
869 }
870 }
871
872 test "BENCHMARK: ThunkRegistry refineVariable" {
873 const benchmark_latency = bench_util.benchmarkScope("ThunkRegistry refineVariable");
874 defer benchmark_latency.end();
875 const allocator = bench_util.allocator();
876 const ThunkRegistry = evaluator.ThunkRegistry;
877 const LazyKCThunk = runtime.LazyKCThunk;
878 const PExpr = pexpr.PExpr;
879 const Env = runtime.Env;
880 const RuntimeValue = runtime.RuntimeValue;
881 const World = evaluator.World;
882 const GuardedWorlds = runtime.GuardedWorlds;
883 const bench = bench_util.BenchConfig.init();
884
885 bench_util.stdout("\n=== Benchmark 11: ThunkRegistry.refineVariable ===\n", .{});
886 bench_util.stdout("num_thunks,num_vars,cache_entries_per_thunk,refine_ns,ops_per_us\n", .{});
887
888 const thunk_counts = [_]usize{ 5, 10, 20 };
889 const cache_entries_per_thunk = [_]usize{ 1, 5, 10 };
890 const thunk_len = bench.limit(thunk_counts.len, 1);
891 const cache_len = bench.limit(cache_entries_per_thunk.len, 1);
892 const iterations = bench.iters(5, 1);
893
894 for (thunk_counts[0..thunk_len]) |num_thunks| {
895 for (cache_entries_per_thunk[0..cache_len]) |cache_entries| {
896 var manager = try Manager.init(allocator);
897 defer manager.deinit();
898
899 const num_vars: usize = 10;
900 var bdd_vars: [10]Bdd = undefined;
901 for (0..num_vars) |v| {
902 bdd_vars[v] = try manager.newVar(true);
903 }
904
905 const dummy_val = try RuntimeValue.initNative(allocator, .{ .int = 42 });
906 defer dummy_val.deinit(allocator);
907
908 var exprs: std.ArrayList(*PExpr) = .empty;
909 defer {
910 for (exprs.items) |e| e.deinit(allocator);
911 exprs.deinit(allocator);
912 }
913
914 var thunks: std.ArrayList(*LazyKCThunk) = .empty;
915 defer {
916 for (thunks.items) |t| t.deinit(allocator);
917 thunks.deinit(allocator);
918 }
919
920 var registry = ThunkRegistry.init(allocator);
921 defer registry.deinit();
922
923 for (0..num_thunks) |thunk_idx| {
924 const expr = try PExpr.init(allocator, .{ .const_native = .{ .float = @floatFromInt(thunk_idx) } });
925 try exprs.append(allocator, expr);
926
927 var callstack_buf: [3]i32 = .{ @intCast(thunk_idx), 0, 0 };
928 const thunk = try LazyKCThunk.init(allocator, expr, Env.empty, 0, &callstack_buf);
929 try thunks.append(allocator, thunk);
930
931 try registry.register(thunk, expr, &callstack_buf);
932
933 for (0..cache_entries) |entry_idx| {
934 var guard = bdd_vars[entry_idx % num_vars];
935 if (entry_idx + 1 < num_vars) {
936 guard = try manager.bddAnd(guard, bdd_vars[(entry_idx + 1) % num_vars]);
937 }
938
939 const worlds_slice = try allocator.alloc(World, 1);
940 worlds_slice[0] = .{ .value = dummy_val, .guard = guard };
941
942 try thunk.cache.append(allocator, GuardedWorlds{
943 .worlds = worlds_slice,
944 .validity_guard = Bdd.TRUE,
945 });
946 }
947 }
948
949 const total_cache_entries = num_thunks * cache_entries;
950
951 var refine_total: i128 = 0;
952 for (0..iterations) |iter| {
953 const var_to_refine: VarLabel = @intCast(iter % num_vars);
954 const start = bench_util.nowNs();
955 try registry.refineVariable(&manager, var_to_refine, true);
956 refine_total += bench_util.elapsedNsAccum(start);
957 }
958 const refine_ns: u64 = @intCast(@divFloor(refine_total, iterations));
959 const ops_per_us = @as(f64, @floatFromInt(total_cache_entries)) / @as(f64, @floatFromInt(@max(refine_ns, 1))) * 1000;
960
961 bench_util.stdout("{d},{d},{d},{d},{d:.2}\n", .{
962 num_thunks,
963 num_vars,
964 cache_entries,
965 refine_ns,
966 ops_per_us,
967 });
968 }
969 }
970 }