Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Feb 16, 2022

Implements the second half of #589 on top of #597.

Uses the parmap library to parse files in parallel using forked processes. Merging still happens once in the parent process, because it's not clear whether anything more clever with parmapfold would help (#532).

OpenSSL

On 250 files from OpenSSL compilation database, there's a notable improvement in preprocessing+parsing time.
With -j 1:

real	0m59,919s
user	0m55,434s
sys	0m4,429s

With -j 8:

real	0m16,363s
user	1m24,972s
sys	0m5,803s

With -j 16 (which doesn't help much):

16
real	0m13,405s
user	2m10,305s
sys	0m8,085s

When also including merging time, the improvement is much smaller though:
With -j 1:

real	1m9,892s
user	1m6,274s
sys	0m3,579s

With -j 8:

real	0m43,579s
user	1m54,741s
sys	0m6,216s

Something quite fishy is happening with the merging of files that were parsed in parallel. Somehow they are considerably slower to merge and I'm not sure how that can be.

@sim642 sim642 added performance Analysis time, memory usage pr-dependency Depends or builds on another PR, which should be merged before labels Feb 16, 2022
@michael-schwarz michael-schwarz self-requested a review February 19, 2022 10:32
@sim642 sim642 mentioned this pull request Feb 21, 2022
Base automatically changed from parallel-preprocess to master February 21, 2022 15:12
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Feb 21, 2022
@sim642
Copy link
Member Author

sim642 commented Feb 28, 2022

Something quite fishy is happening with the merging of files that were parsed in parallel. Somehow they are considerably slower to merge and I'm not sure how that can be.

I wonder if this is for a similar reason as #603 (comment). Will have to recheck the performance at some point.

@sim642 sim642 linked an issue Mar 7, 2022 that may be closed by this pull request
2 tasks
@sim642 sim642 added the parallel Parallel Goblint label Mar 16, 2022
@michael-schwarz
Copy link
Member

I'm a bit skeptical about introducing some other concurrency library on the eve of Ocaml getting proper multi-threading. So unless there are specific reasons we cannot wait for 5.0 here, I'd want to at least try with the new OCaml concurrency (domains+effects).

@sim642
Copy link
Member Author

sim642 commented Mar 19, 2022

Since this is kind of hacky anyway, there's no rush to push this through right now. The big issue is CIL having lots of global state, which this somewhat tries to work around (by renumbering statements which each child process otherwise numbers from 1) and which Multicore OCaml won't magically solve (because on a shared heap you have to deal with data races instead). So this isn't safely feasible without rewriting CIL to not use any global state.

Regarding the wait for OCaml 5.0, the moment we want to use some Multicore OCaml features in Goblint, we'll have to give up any OCaml 4.x compatibility from there on out. That means just living on the bleeding edge, while currently we support a number of older versions still. And of course we'll be held back until all our dependencies get OCaml 5.0 compatibility, and making the jump we'll have to give up earlybird debugging support for a long while since it's really lagging behind already on the minor versions. Therefore I think we won't be jumping to Multicore OCaml features in a rush anyway.

EDIT: Also js_of_ocaml support for Multicore is under a big question mark right now. So by bumping the minimum to OCaml 5.0 we'd be dropping Gobview support altogether.

@michael-schwarz michael-schwarz marked this pull request as draft May 25, 2022 13:39
@sim642
Copy link
Member Author

sim642 commented Jul 26, 2022

Closing as not planned to complete. This requires CIL to be refactored free of global state in order to work reliably.

@sim642 sim642 closed this Jul 26, 2022
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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Parallel preprocessing and parsing

3 participants