Introduce backwards compatible infrastructure for parallelism #1708
Conversation
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
force-pushed
the
parallelism_backwards_compat_1
branch
from
522315f to
80cac2a
Compare
arkocal
force-pushed
the
parallelism_backwards_compat_1
branch
from
80cac2a to
3f7d226
Compare
|
Turns out introducing domain_shims breaks GobView. The application than outputs on the console and hangs indefinitely. |
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? |
|
I guess we either need to turn the gobview job into an unlocked one, or provide a different lockfile for the gobview job somehow? |
| "parallel_domains" :{ | ||
| "title": "solvers.td3.parallel_domains", | ||
| "description": "Maximal number of Domains that the solver can use in parallel. Only applies, when a solver of the 'td_parallel_*' family is used.", | ||
| "type": "integer", | ||
| "default": 2 |
There was a problem hiding this comment.
Seems like the existing jobs option would also work for this.
There was a problem hiding this comment.
I think it's worth having the concurrency settings for non-core stuff (g2html, preprocessing) separate from the solver concurrency, especially when comparing runtimes.
| let pp_print_option ?(none = fun _ () -> ()) pp_v ppf = function | ||
| | None -> none ppf () | ||
| | Some v -> pp_v ppf v | ||
| in |
There was a problem hiding this comment.
What's this about? Isn't it just a copy of what's in Stdlib.Format?
| let recursive_int = lazy ( | ||
| let recursive_int = DomainsafeLazy.from_fun (fun () -> |
There was a problem hiding this comment.
Why is DomainsafeLazy only used here? There are other top-level lazy values like
Offset.Index.Exp.allCilfacade.any_index_expLibraryFunctions.intmax_t
There's also ResettableLazy which is used all over. Are all of those safe then?
There was a problem hiding this comment.
Good point! Also what about LazyEval? Are we fine with force being called concurrently there?
| let add_ref: (Token.t -> unit) ref = ref (fun _ -> | ||
| let add_ref: (Token.t -> unit) Domain.DLS.key = Domain.DLS.new_key (fun () _ -> |
There was a problem hiding this comment.
Similar question here: we have a lot of top-level refs around, but only this one is made domain-local. Are all others fine then?
| let enabled_dls = Domain.DLS.new_key (fun () -> false) | ||
| let options_dls = Domain.DLS.new_key (fun () -> dummy_options) |
There was a problem hiding this comment.
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.
| @@ -38,9 +39,13 @@ let traceTag (sys : string) : Pretty.doc = | |||
| let rec ind (i : int) : string = if (i <= 0) then "" else " " ^ (ind (i-1)) in | |||
| (text ((ind !indent_level) ^ "%%% " ^ sys ^ ": ")) | |||
|
|
|||
| let trace_mutex = GobMutex.create () | |||
There was a problem hiding this comment.
Tracing isn't the only output from Goblint. Why don't others (like Logs and Messages) also need locks?
There was a problem hiding this comment.
Those should happen at the end in postprocessing, which is not concurrent afaik.
This contains the rather harmless parts. As discussed, all variations of modules have been implemented using
domain_shimsand the select stanza in dune.ppx_optcompis not involved anymore.The PR is rather large, but can be reviewed commit-by-commit.