Change jobs
option default to 0
#1810
Open
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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. Thejobs
option is just used to run multiple subprocesses at once, not doing any parallelism in OCaml.