russell@unturf.com
87503f60ef
Closes the three tractable pending buckets (all non-no_dir work):
+ lean4-0004..0007: 4 correctness/race benches (ir_interp DCL, jobreg
IO.Ref race, g_opts thread-local leakage, process envvar hash).
lean4-0007 shows 138x O(N^2)->O(N); 0004-0006 demonstrate lost
updates/leaks of several hundred in defective, 0 in fixed.
+ 0ad-0001..0004: 3 CWE-407 list.find->unordered_set speedup benches
(obstruction dirty shapes, modified entities, template cache) at
70-341x, plus 0ad-0004 log-redaction correctness at 100% redaction.
+ activemq-0001..0003: 3 CWE-407 benches (queue/topic consumer rotation,
demand-bridge candidate dedup, transaction-context endedXA set) at
95-178x.
+ linux-0001..0008: 8 Python complexity-class models for the kernel
patches. Coexist with the existing build-and-bench.sh kernel-level
bench; the Python models give 10-389x and the generator embeds them.
+ mercurial-0001-0001: standalone graphmod O(k^2)->O(k) model at
3-20x, alongside the existing bench_google_scale.py (which imports
the real mercurial graphmod).
Progress: 13 -> 33 full coverage. Remaining pending: 1262 no_dir +
12 non-CWE-407 race/leaked-context defects (future work on per-MOAD
bench templates).
37 lines
2 KiB
Text
37 lines
2 KiB
Text
=== lean4-0001: guardCycle List vs HashSet ===
|
|
N=100 : defective=0.125ms fixed=0.021ms speedup=6.0x
|
|
N=500 : defective=3.103ms fixed=0.139ms speedup=22.3x
|
|
N=1000 : defective=12.449ms fixed=0.300ms speedup=41.4x
|
|
N=2000 : defective=40.612ms fixed=1.025ms speedup=39.6x
|
|
|
|
=== lean4-0002: inductive type check std::find vs set ===
|
|
K=N=100 : defective=0.206ms fixed=0.004ms speedup=57.6x
|
|
K=N=500 : defective=5.312ms fixed=0.016ms speedup=325.6x
|
|
K=N=1000: defective=18.706ms fixed=0.030ms speedup=629.7x
|
|
|
|
=== lean4-0003: fresh name generation ===
|
|
N=100 : defective=0.167ms fixed=0.004ms speedup=44.0x
|
|
N=500 : defective=4.501ms fixed=0.022ms speedup=206.1x
|
|
N=1000 : defective=17.938ms fixed=0.049ms speedup=369.1x
|
|
|
|
=== lean4-0004: ir_interpreter double-checked lock race (correctness) ===
|
|
threads=2 ops=500 : defective_lost_updates(max)= 490 fixed_lost_updates(max)= 0
|
|
threads=4 ops=500 : defective_lost_updates(max)=1084 fixed_lost_updates(max)= 0
|
|
threads=8 ops=500 : defective_lost_updates(max)= 994 fixed_lost_updates(max)= 0
|
|
|
|
=== lean4-0005: Lake jobreg IO.Ref.modify race (correctness) ===
|
|
workers=4 pushes=200 : expected=800 defective_lost(max)= 599 fixed_lost(max)= 0
|
|
workers=8 pushes=200 : expected=1600 defective_lost(max)=1400 fixed_lost(max)= 0
|
|
workers=16 pushes=200 : expected=3200 defective_lost(max)=2993 fixed_lost(max)= 0
|
|
|
|
=== lean4-0006: kernel/trace g_opts thread-local leakage (correctness) ===
|
|
threads=2 tasks=200 : defective_leakages(max)= 199 fixed_leakages(max)= 0
|
|
threads=4 tasks=400 : defective_leakages(max)= 399 fixed_leakages(max)= 0
|
|
threads=8 tasks=800 : defective_leakages(max)= 798 fixed_leakages(max)= 0
|
|
|
|
=== lean4-0007: process.cpp Windows env vars list-count vs unordered_set ===
|
|
N=100 : defective=0.315ms fixed=0.028ms speedup=11.2x
|
|
N=500 : defective=4.737ms fixed=0.127ms speedup=37.4x
|
|
N=1000 : defective=19.896ms fixed=0.281ms speedup=70.9x
|
|
N=2000 : defective=23.665ms fixed=0.171ms speedup=138.0x
|
|
|