Introduce backwards compatible infrastructure for parallelism #1708

arkocal · 2025-03-11T09:20:32Z

This contains the rather harmless parts. As discussed, all variations of modules have been implemented using domain_shims and the select stanza in dune. ppx_optcomp is not involved anymore.

The PR is rather large, but can be reviewed commit-by-commit.

In order to maintain backwards compatibility, we need to provide stubs for functionality needed for parallelism when no libraries provide this. Also, to keep possibly diverging parts to a minimum, the utilities for parallelism are kept in a separate module.

This works async in Ocaml4 and truly parallel in OCaml5

fix printing issue by using BatFormat in messages.ml

This is a high level abstraction AND a backward compat. wrapper

Possibly, this could be needed elsewhere, where state is involved

Make stack DLS and initialize for each domain Actually implemented by Felix Krayer

arkocal · 2025-03-11T10:37:00Z

Turns out introducing domain_shims breaks GobView. The application than outputs

Uncaught TypeError: runtime.caml_thread_self is not a function

on the console and hangs indefinitely.

…elopment purposes

michael-schwarz · 2025-03-12T11:50:34Z

Turns out introducing domain_shims breaks GobView. The application than outputs

Do you know where this call happens? Is it something we can safely stub to just return unit or somehow avoid these calls when in Gobview mode?

michael-schwarz · 2025-03-21T16:11:49Z

I guess we either need to turn the gobview job into an unlocked one, or provide a different lockfile for the gobview job somehow?

src/config/options.schema.json

sim642 · 2025-03-26T08:29:19Z

src/common/util/messages.ml

+  let pp_print_option ?(none = fun _ () -> ()) pp_v ppf = function
+    | None -> none ppf ()
+    | Some v -> pp_v ppf v
+  in


What's this about? Isn't it just a copy of what's in Stdlib.Format?

The module now uses BatFormat, which does not define the method.

But why BatFormat? The standard library version from OCaml 5 should be safe: it's been reimplemented to use DLS properly. Batteries as no domains-specific fixes.

src/cdomain/value/cdomains/mutexAttrDomain.ml

src/lifters/wideningTokenLifter.ml

sim642 · 2025-03-26T08:40:23Z

src/util/timing/goblint_timing.ml

+  let enabled_dls = Domain.DLS.new_key (fun () -> false)
+  let options_dls = Domain.DLS.new_key (fun () -> dummy_options)


Is it necessary for these to be domain-local? These are more like global options than state.
#1550 mentions that maybe only current needs to be domain-local.

Felix himself has introduced all of them in 62422e9

As far as can see enabled_dls is rather tracking if it is active in a given moment (set via start and stop), and making it a reference makes the solver crash at the end. Options however are global options and can be made into refs.

9e1614d reflects this now.

As far as can see enabled_dls is rather tracking if it is active in a given moment (set via start and stop), and making it a reference makes the solver crash at the end.

But we only ever call start at the very beginning of Goblint and never even call stop. So I don't understand why there would be any issue. start also modifies options and that's fine.

Interesting, making them into refs did cause issues, so I will need to investigate this further.

src/util/tracing/goblint_tracing.ml

…_backwards_compat_1

Copilot

Copilot reviewed 8 out of 25 changed files in this pull request and generated 1 comment.

Files not reviewed (17)

dune-project: Language not supported
goblint.opam: Language not supported
goblint.opam.locked: Language not supported
src/cdomain/value/cdomains/mutexAttrDomain.ml: Language not supported
src/cdomain/value/dune: Language not supported
src/common/util/messages.ml: Language not supported
src/config/options.schema.json: Language not supported
src/dune: Language not supported
src/goblint_lib.ml: Language not supported
src/lifters/wideningTokenLifter.ml: Language not supported
src/solver/dune: Language not supported
src/util/parallel/domainsafeLazy.ml: Language not supported
src/util/parallel/domainsafeLazy.mli: Language not supported
src/util/parallel/dune: Language not supported
src/util/parallel/gobMutex.domainslib.ml: Language not supported
src/util/parallel/gobMutex.no-domainslib.ml: Language not supported
src/util/parallel/threadpool.domainslib.ml: Language not supported

Comments suppressed due to low confidence (1)

.github/workflows/unlocked.yml:255

[nitpick] Consider using consistent capitalization for 'GobView' across workflow configurations to align with the documentation.

gobview:

docs/user-guide/inspecting.md

sim642 · 2025-04-09T06:50:15Z

Looks like the Copilot reviews won't be too useful for us right now since it doesn't want to review .ml files.

src/util/parallel/threadpool.no-domainslib.ml

sim642 · 2025-04-17T09:02:12Z

src/util/parallel/dune

+ (name goblint_parallel)
+ (public_name goblint.parallel)
+ (libraries
+   batteries


Where is batteries used here?

sim642 · 2025-04-17T09:02:27Z

src/util/parallel/dune

+   (select threadpool.ml from 
+      (domainslib -> threadpool.domainslib.ml)
+      (-> threadpool.no-domainslib.ml)
+      )


Suggested change

)

)

sim642 · 2025-04-17T09:03:25Z

src/util/parallel/domainsafeLazy.mli

@@ -0,0 +1,6 @@
+(** Lazy type which protects against concurrent calls of 'force'. *)


Suggested change

(** Lazy type which protects against concurrent calls of 'force'. *)

(** Lazy type which protects against concurrent calls of {!force}. *)

sim642 · 2025-04-17T09:09:27Z

src/util/parallel/domainsafeLazy.ml

If we're taking the mutex implementation from domain-local-await, why not the lazy? https://github.com/ocaml-multicore/domain-local-await?tab=readme-ov-file#example-concurrency-safe-lazy (pending the licence question below)

In particular, that one seems to properly handle exceptions, whereas the one here would royally break: the mutex wouldn't be unlocked even and any future attempts to lock it will block forever.

src/util/parallel/gobMutex.domainslib.ml

sim642 · 2025-04-17T09:14:23Z

src/util/parallel/dune

+   (select gobMutex.ml from
+      (domainslib -> gobMutex.domainslib.ml)
+      ( -> gobMutex.no-domainslib.ml)
+   )
+   (select threadpool.ml from 
+      (domainslib -> threadpool.domainslib.ml)
+      (-> threadpool.no-domainslib.ml)


I think it's a good idea to have .mli files for these as well (not dependent on domainlib presence).

src/util/parallel/threadpool.no-domainslib.ml

+
+  let await_all pool promises =
+    List.iter (fun promise -> Domain.join promise) promises;
+    print_endline "All threads finished."


sim642 · 2025-04-29T14:03:28Z

src/util/parallel/threadpool.no-domainslib.ml

+  let create n = ()
+
+  let add_work pool f =
+    let promise = Domain.spawn f in


The dummy implementation is supposed to be OCaml 4 compatible, so it can't use Domain at all.

Domain is provided by domain_shims, which is already included here. It acts as Domain on Ocaml5 and provides async parallelism on OCaml4.

domain_shims implements Domain via Thread though, so it still allows interleaved execution (but not parallel execution). Even for that, output needs to be done under a real mutex, not a dummy one.
If the non-parallel mutex is a dummy, then the non-parallel thread pool probably should be even stupider: just run in the same thread entirely.

arkocal and others added 7 commits March 11, 2025 10:16

Parallelism: Add domain_shims

1667683

This works async in Ocaml4 and truly parallel in OCaml5

Parallelism: Make messages thread-safe

f9ed034

fix printing issue by using BatFormat in messages.ml

Parallelism: Introduce thread-pool

bc33346

This is a high level abstraction AND a backward compat. wrapper

Parallelism: Introduce domain safe lazy

67a1c61

Parallelism: Apply thread-safe Lazy on mutexAttrDomain

3b9d901

Possibly, this could be needed elsewhere, where state is involved

Parallelism: Workout for timing

539a853

Make stack DLS and initialize for each domain Actually implemented by Felix Krayer

arkocal force-pushed the parallelism_backwards_compat_1 branch from 522315f to 80cac2a Compare March 11, 2025 09:36

Parallelism: Docs for utils

3f7d226

arkocal force-pushed the parallelism_backwards_compat_1 branch from 80cac2a to 3f7d226 Compare March 11, 2025 09:38

arkocal added the parallel Parallel Goblint label Mar 11, 2025

arkocal and others added 2 commits March 11, 2025 13:05

Make wideningTokenLifter thread safe

48c76c0

Parallelism: adding parallel_domains option. Default set to 2 for dev…

7fe63ef

…elopment purposes

sim642 self-requested a review March 11, 2025 12:52

arkocal added 3 commits March 21, 2025 10:17

Gobview: Drop support for Ocaml < 5.0.0

490d047

Gobview: Drop support for Ocaml < 5.0.0

16db900

Gobview: Drop support for Ocaml < 5.0.0

dec26b3

Gobview: Move to unlocked test to use Ocaml 5.0.0

f423d8e

sim642 reviewed Mar 26, 2025

View reviewed changes

sim642 added the setup Dependencies, CI, releasing label Mar 26, 2025

arkocal added 3 commits April 8, 2025 15:07

Merge branch 'master' of github.com:goblint/analyzer into parallelism…

ccb2a6f

…_backwards_compat_1

Parallelism: Update documentation for parallel domains

a18cd77

Parallelism: Timing: Only use DLS when necessary

9e1614d

michael-schwarz requested a review from Copilot April 8, 2025 22:32

Copilot AI reviewed Apr 8, 2025

View reviewed changes

docs/user-guide/inspecting.md Show resolved Hide resolved

sim642 self-requested a review April 9, 2025 06:50

This was referenced Apr 17, 2025

Parallelism support: PoC/Suggestion #1694

Closed

Audit for domain-unsafe global code #1730

Open

sim642 reviewed Apr 17, 2025

View reviewed changes

Parallelism: Introduce mock thread pool

92043ca

github-advanced-security bot found potential problems Apr 25, 2025

View reviewed changes

sim642 reviewed Apr 29, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introduce backwards compatible infrastructure for parallelism #1708

Introduce backwards compatible infrastructure for parallelism #1708

arkocal commented Mar 11, 2025

arkocal commented Mar 11, 2025 •

edited

Loading

michael-schwarz commented Mar 12, 2025

michael-schwarz commented Mar 21, 2025

sim642 Mar 26, 2025

arkocal Apr 8, 2025

sim642 Apr 17, 2025

sim642 Mar 26, 2025

arkocal Apr 8, 2025

sim642 Apr 17, 2025

arkocal Apr 29, 2025

Copilot AI left a comment

sim642 commented Apr 9, 2025

sim642 Apr 17, 2025

sim642 Apr 17, 2025

sim642 Apr 17, 2025

sim642 Apr 17, 2025

sim642 Apr 17, 2025

Check warning

sim642 Apr 29, 2025

arkocal Apr 29, 2025

sim642 Apr 30, 2025

		let enabled_dls = Domain.DLS.new_key (fun () -> false)
		let options_dls = Domain.DLS.new_key (fun () -> dummy_options)

		@@ -0,0 +1,6 @@
		(** Lazy type which protects against concurrent calls of 'force'. *)

Introduce backwards compatible infrastructure for parallelism #1708

Are you sure you want to change the base?

Introduce backwards compatible infrastructure for parallelism #1708

Conversation

arkocal commented Mar 11, 2025

arkocal commented Mar 11, 2025 • edited Loading

michael-schwarz commented Mar 12, 2025

michael-schwarz commented Mar 21, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Copilot AI left a comment

Choose a reason for hiding this comment

sim642 commented Apr 9, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Check warning

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arkocal commented Mar 11, 2025 •

edited

Loading