On Tue, 2024-10-08 at 19:12 -0700, Eduard Zingerman wrote: [...] > This patch forcibly enables checkpoints for each loop back-edge. > This helps with the programs in question, as verification of both > syzbot program and reduced snippet finishes in ~2.5 sec. [...] > File Program Insns (DIFF) States (DIFF) > -------------------------- ------------------------------------ ---------------- ------------------- > ... > pyperf600.bpf.o on_event -53870 (-9.81%) -3000 (-10.16%) > ... fwiw, this patch speeds up verification of pyperf600 by a small margin, sufficient for it to pass in combination with jump history bump when LLVM20 is used. # ./veristat pyperf600.bpf.o no_alu32/pyperf600.bpf.o cpuv4/pyperf600.bpf.o ... File Program Verdict Duration (us) Insns States Peak states --------------- -------- ------- ------------- ------ ------ ----------- pyperf600.bpf.o on_event success 2400571 872914 26490 25480 pyperf600.bpf.o on_event success 2460908 947038 26090 25330 pyperf600.bpf.o on_event success 2158117 788481 26329 25368 --------------- -------- ------- ------------- ------ ------ ----------- W/o this patch jump history bump is not sufficient to get no_alu32 version verified, instruction limit is reached. The draft is here: https://github.com/eddyz87/bpf/tree/jmp-history-pyperf600 [...]
