analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Change `jobs` option default to 0

Open sim642 opened this issue 4 months ago • 2 comments

While benchmarking #1752 I noticed that there's no real difference between cputime and walltime, even when I switched Goblint from 1 core to 4 cores. After some profiling I realized that we're not using any parallelism for Graphviz, which is the slowest part of HTML output, even though we have all the implementation to do so.

It's just that our default behavior is shooting us in the foot by forbidding multiple Graphviz processes to run in parallel. The fact that even I wasn't aware of it means it's not a useful default.

As a random example, on smtprc this will reduce HTML speed from 14s to 9s on my laptop. With #1752, the Graphviz time goes from 6.9s to 4.4s, where the largest function's CFG takes 4s to render by Graphviz.

The parallel solvers to be already have a separate option solvers.td3.parallel_domains anyway to benchmark them properly. The jobs option is just used to run multiple subprocesses at once, not doing any parallelism in OCaml.

sim642 avatar Aug 15 '25 09:08 sim642