Skip to content

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Aug 15, 2025

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 sim642 added usability performance Analysis time, memory usage parallel Parallel Goblint labels Aug 15, 2025
@sim642
Copy link
Member Author

sim642 commented Sep 3, 2025

Here are some benchmarks extending the ones in #1752 (comment) on sv-benchmarks with witness generation disabled and HTML generation enabled.
They include the runs from there, but also "-jobs" variants of both where 4 jobs are allowed for HTML generation (instead of the default 1).

cputime

image

walltime

image

memory

image

@sim642 sim642 mentioned this pull request Sep 3, 2025
3 tasks
@sim642 sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Sep 3, 2025
@sim642
Copy link
Member Author

sim642 commented Sep 3, 2025

Hmm, the cputime plot is odd: just using more jobs (with either HTML generation) uses less CPU time. And this is not only CPU time measured by Goblint's own timing, but also CPU time as measured by BenchExec.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parallel Parallel Goblint performance Analysis time, memory usage usability
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant