Seq optimization #965

KhalilCK · 2023-01-12T15:05:12Z

We replaced certain List methods with Seq package.
The sanity check passed without errors using make test and the benchmarking using the following flags:

./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.interval --enable ana.int.interval_threshold_widening

On my local machine the Seq implementation took 820.1s.
We will choose between the Seq and iter packages, which one is better based on the results of the benchmarking on the cluster that you can find in the Iter PR #964.

…def_exc_widen_by_join

Also split config value records into multiple smaller records

…analyzer into int-domain-code-optimizations

jerhard

Hey, thanks for your pull request!
Good to see that you could find places where it looks like it makes sense to introduce Seq!

I left some comments, mainly about the case when only one operation on a list is replaced by an operation on Seq, and some conversion back and forth (from and to lists) is done. I would assume that in such cases, there would be no performance benefit of doing this, as still the same number of allocations has to be done to create the result list -- only in List.of_seq instead of, say List.map.

jerhard · 2023-01-18T16:02:58Z

make.sh

+  opam update
+  # Note: the `--update-invariant` option is needed for replacement of the previous ocaml compiler switch invariant of Goblint
+  opam switch -y create . --deps-only ocaml-variants.4.14.0+options ocaml-option-flambda --locked --update-invariant
+}


Are these changes necessary or already subsumed by the merged flambda PR?

jerhard · 2023-01-18T16:04:15Z

src/analyses/base.ml

   **************************************************************************)

-  let is_privglob v = GobConfig.get_bool "annotation.int.privglobs" && v.vglob
+   let is_privglob v = get_bool "annotation.int.privglobs" && v.vglob


Is this change in indentation intentional?

jerhard · 2023-01-18T16:08:34Z

src/analyses/base.ml

    (* Return the list of elements that have been visited. *)
    if M.tracing then M.traceu "reachability" "All reachable vars: %a\n" AD.pretty !visited;
-    List.map AD.singleton (AD.elements !visited)
+     List.of_seq @@ (Seq.map AD.singleton) @@ List.to_seq (AD.elements !visited)


Since there is only operation (List.map) that is replaced, can one hope that this change actually has a positive performance impact?

jerhard · 2023-01-18T16:09:33Z

src/analyses/base.ml

          | (e1, e2) :: eqs ->
            let eqs_for_all_mem e = List.for_all (fun (e1, e2) -> CilType.Exp.(equal e1 e || equal e2 e)) eqs in
-            let eqs_map_remove e = List.map (fun (e1, e2) -> if CilType.Exp.equal e1 e then e2 else e1) eqs in
+            let eqs_map_remove e = List.of_seq @@ Seq.map (fun (e1, e2) -> if CilType.Exp.equal e1 e then e2 else e1) @@ List.to_seq eqs in


Same question as above, as there is only a List.map that is replaced.

jerhard · 2023-01-18T16:09:51Z

src/analyses/base.ml

          let* (e, es) = find_common eqs in
          let v = eval_rv a gs st e in (* value of common exp *)
-          let vs = List.map (eval_rv a gs st) es in (* values of other sides *)
+          let vs = List.of_seq @@ (Seq.map (eval_rv a gs st)) @@ List.to_seq es in (* values of other sides *)


Same question as above, as there is only a List.map that is replaced.

jerhard · 2023-01-18T16:16:58Z

src/analyses/base.ml

          match arg with
          | Some x -> [x]
-          | None -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals
+          | None -> List.of_seq @@ Seq.map (fun x -> MyCFG.unknown_exp) @@ List.to_seq fd.sformals


Same question as above, as there is only a List.map that is replaced.

jerhard · 2023-01-18T16:17:11Z

src/analyses/base.ml

        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
      end
-    | _, _ when get_bool "sem.unknown_function.spawn" ->
+      | _, _ when get_bool "sem.unknown_function.spawn" ->


Is this change in indentation intentional?

jerhard · 2023-01-18T16:17:27Z

src/analyses/base.ml

    in
    let forks = forkfun ctx lv f args in
-    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," d_varinfo) (List.map BatTuple.Tuple3.second forks);
+    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," d_varinfo) (List.of_seq @@ Seq.map BatTuple.Tuple3.second @@ List.to_seq forks);


Same question as above, as there is only a List.map that is replaced.

jerhard · 2023-01-18T16:17:40Z

src/analyses/base.ml

          begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
            | `Thread a ->
-              let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in
+              let v = List.fold VD.join (VD.bot ()) (List.of_seq @@ Seq.map (fun x -> G.thread (ctx.global (V.thread x))) @@ List.to_seq (ValueDomain.Threads.elements a)) in


Same question as above, as there is only a List.map that is replaced.

jerhard · 2023-01-18T16:18:56Z

src/cdomains/intDomain.ml

+  (* This is a container variable for holding the config value of ana.int.interval_threshold_widening *)
+(*  let interval_threshold_widening_ref: float_precision option ref = ref None
+
+  let get_interval_threshold_widening_ref (): float_precision option =
+    if !interval_threshold_widening_ref = None then
+      let config_value = Some (get_bool "ana.int.interval_threshold_widening") in
+      interval_threshold_widening_ref := config_value; !interval_threshold_widening_ref
+    else
+      !interval_threshold_widening_ref
+
+  let extract_from_option (x: float_precision option): float_precision =
+    match x with
+    | None -> failwith "Config option not read"
+    | Some x -> x
+*)


Please remove the blocks of commented code (here and below). Any changes related to the configuration should be separated out.

KhalilCK · 2023-01-19T12:24:56Z

As we discussed I removed all the Seq that are performed on only one single List operation.

sim642 · 2023-01-31T11:33:21Z

Closing in favor of #975.

sxprz and others added 25 commits November 24, 2022 11:29

Update README.md

52c7671

Update README.md

40b919b

Update make.sh to also install ocaml with flambda

acfcba0

Update make.sh for the right flambda switch + update goblint.opam.locked

cb20ac4

Remove eval from opam_setup_flambda

74c4df2

Update README with flambda installation info

bb6fcf1

Remove v2.9 for dune from goblint.opam

1f9674d

add flambda flags

4b81638

Add the flambda compiler version to unlocked.yml

fcda025

Add ocaml-option-flambda to 4.14.0+options compiler in unlocked.yml

5f3f798

Use -O3 in src/dune for flambda optimizations

0534c15

Replace frequent get_bool calls with variable lookups

de67425

added lazy evaluation

dbb9d8b

added lazy evaluation

bae92cc

Memoize config value for ana.int.interval_threshold_widening

7c0ce42

Memoize config value for ana.int.interval_narrow_by_meet and ana.int.…

e6a7681

…def_exc_widen_by_join

add record to store config variables

9072477

Create configUtil module and use it also in base.ml

786e31d

Using Sequence Module to perform map

7594b45

Refactor get_*_config functions to avoid string matching

696feb7

Also split config value records into multiple smaller records

Merge branch 'int-domain-code-optimizations' of github.com:adelavais/…

72c0975

…analyzer into int-domain-code-optimizations

Remove configUtil module and put everything back in intDomain

d7ada1c

Using Sequence Module to perform map on all methods on base.ml

619b634

Solving some errors of merge conflicts

abeffdb

Using Sequence Module to perform other list operations

9cf751f

montrie mentioned this pull request Jan 12, 2023

Iter optimization #964

Closed

sim642 added student-job performance Analysis time, memory usage pr-dependency Depends or builds on another PR, which should be merged before labels Jan 16, 2023

sim642 self-requested a review January 16, 2023 08:22

jerhard self-requested a review January 18, 2023 15:50

jerhard reviewed Jan 18, 2023

View reviewed changes

Removing Sequence on single List operation

0270f67

sim642 mentioned this pull request Jan 27, 2023

Iter optimization clean up #974

Closed

KhalilCK mentioned this pull request Jan 28, 2023

Seq-optimization clean version #975

Merged

sim642 closed this Jan 31, 2023

sim642 added this to the v2.2.0 milestone Apr 5, 2023

Seq optimization #965

Seq optimization #965

Uh oh!

Conversation

KhalilCK commented Jan 12, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jerhard left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jerhard Jan 18, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jerhard Jan 18, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

KhalilCK commented Jan 19, 2023

Uh oh!

sim642 commented Jan 31, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

KhalilCK commented Jan 12, 2023 •

edited

Loading

jerhard Jan 18, 2023 •

edited

Loading

jerhard Jan 18, 2023 •

edited

Loading