`--cores` flag is detrimental to performance

[facundominguez]

The --cores flag specifies how many cores should be used to check verification conditions. It is set by default to Nothing, meaning that the implementation will try to assign verification conditions to different processors as it sees fit.

I have found an example recently where verification with --cores=1, that is no parallelism, is faster than verification with parallelism (the default setting). The improvement is significant as verification with parallelism requires twice as long as no parallelism.

I decided to benchmark the flag against the testsuite. If I make --cores=1 the default, a couple of benchmarks improve considerably.

It would be interesting to know if someone has a larger example where parallelism makes a substantial improvement (say in the order of minutes).

The benchmark framework is measuring CPU time at the moment. To have conclusive results we should be measuring wall-clock time instead. I manually checked the Base and the Fusion/T benchmarks below and they are faster with no parallelism even when measured with wall-clock time.

Benchmark results follow. "before" is with parallelism, "after" is without.

[ranjitjhala]

Wow!🤩 good catch @facundominguez !!!

[facundominguez]

I measured with wall clock time. The improvements are less pronounced there.

Still there are some reasons that incline me to remove --cores.

1. None of the speedups due to parallelism are large.
2. The cpu time are sometimes much higher with parallelism.
3. There are cases where using mutiple cores makes wall clock time considerably longer.
4. There is no rule to predict when using multiple cores will be better or worse. Which makes maintenance harder as modules which use --cores need to be constantly reevaluated.

When some of these issues are addressed, we could propose our users to experiment with parallelism again. But in the current form, it would cause troubles more often than not.

[ranjitjhala]

Maybe instead of removing it entirely, we can make cores=1 the default?

[facundominguez]

Yes, we could do that, but note that it doesn't address any of the issues I'm bringing.

If there were some use case that badly needs support for multiple cores, it would be worth considering. But otherwise I don't see what benefit it has at the moment.

[ranjitjhala]

Good point! My worry is if we remove it entirely, it will be gone and if at some point in the future we want to "revive" it, we'll have to do everything from scratch? So just wanted to keep it around, in the off chance that (a) it might be useful for some specific case, (b) it may come in handy if/when we figure out how to make multiple cores actually useful?

…

On Mon, Jul 28, 2025 at 1:13 PM Facundo Domínguez ***@***.***> wrote: *facundominguez* left a comment (ucsd-progsys/liquidhaskell#2562) <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2562*issuecomment-3129368643__;Iw!!Mih3wA!Az2QLE5NkwuYbpZak8Ny5QwCihsBo9nI5RAaklNm8kCpicRp1xFZNLh8K04cwRG9SnAza-tWg5hElyZITo1-kB2r$> Yes, we could do that, but note that it doesn't address any of the issues I'm bringing. If there were some use case that badly needs support for multiple cores, it would be worth considering. But otherwise I don't see what benefit it has at the moment. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2562*issuecomment-3129368643__;Iw!!Mih3wA!Az2QLE5NkwuYbpZak8Ny5QwCihsBo9nI5RAaklNm8kCpicRp1xFZNLh8K04cwRG9SnAza-tWg5hElyZITo1-kB2r$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGUXEKRVCYVO46AJPT3KZ747AVCNFSM6AAAAACCOIUP5GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTCMRZGM3DQNRUGM__;!!Mih3wA!Az2QLE5NkwuYbpZak8Ny5QwCihsBo9nI5RAaklNm8kCpicRp1xFZNLh8K04cwRG9SnAza-tWg5hElyZITiLqsTRH$> . You are receiving this because you commented.Message ID: ***@***.***>

-- - Ranjit.

[facundominguez]

The implementation in LH is small and easy to reinstate with git revert 3f27e04d. I think the pitfalls in the implementation make your point (a) a very narrow possibility at the moment.

But we can leave the flag too. In that case, I'd like to document it with a notice like

Warning: unpredictable performance
See https://github.com/ucsd-progsys/liquidhaskell/issues/2562

[facundominguez]

I changed the default to only 1 core in #2564.

[AlecsFerra]

But the issue is that in the end you use a single instance of z3 so you don't get any parallelism?

[facundominguez]

I think multiple processes are created. Here's where the implementation splits for multicore. My impression is that much effort is spent in serializing expressions to SMTLIB for every core. But someone would have to look closer into the matter.