profiling and optimizations

[vogler]

Originally posted by @vogler in #188 (comment)

This likely needs some more in-depth profiling (like most of Goblint really...) because it's not obvious at all. For example, if using just DefExc in a 4-component IntDomTuple, most operations would also be doing lots of BatOption.map calls on None.

The assumption was that for n activated out of m total domains you have for a binop

• n * (1+2) (List.map2 + both args) match for IntDomList
• m match for IntDomTuple.

I think I ran some test where it was faster, but would be better to have some inline benchmarks [1] in bench for questions like this.
The main motivation was to reduce boilerplate and make adding domains easier.

Or for example, create/create2 in IntDomTuple make repeated get_bool calls each time, which involves a lot more than looking up a locally cached bool variable (some places do this with options).

create/create2 shouldn't be called often compared to map*.
But good point in general. Maybe it's a good idea to include some memoization for GobConfig.get_* instead letting consumers implement it repeatedly.
Edit: done: 5c73008

My general suspicion and experience with #164 is that we have subtle but massive performance bottlenecks in all sorts of subtle places, but nobody has ever profiled Goblint properly. Which isn't surprising because OCaml profiling tooling is almost non-existent. I tried and still ended up just guessing and using Stats.time to pin the problem.

True, perf report [2] works but it's hard to find bottlenecks, for example it does not list things like get_bool. Haven't tried if enabling frame pointers helps.
The equality stuff in bench/hashcons also looks interesting. What speaks against let (=) a b = a == b || a = b?

[1] https://github.com/Chris00/ocaml-benchmark
[2] https://ocaml.org/learn/tutorials/performance_and_profiling.html#Using-perf-on-Linux

[vogler]

• how to profile? Is perf the best option?
  • do frame pointers help to filter for functions like get_bool?
• 5c73008: memoize GobConfig.get_* -> ~10%?
• is IntDomTuple faster than IntDomList or some Obj list impl. like in MCP2?
• What speaks against let (=) a b = a == b || a = b to speed up everything? See bench/hashcons.
• Profile derived implementations Reduce equal & compare boilerplate using deriving eq & ord #227, see inf-recursion now runs ~6x longer before stack overflow #265 (comment)

[vogler]

Example of profiling with perf that shows how name mangling and inlining make it hard to use: #265 (comment)

[sim642]

Regarding name mangling I found this but didn't try it: https://discuss.ocaml.org/t/ann-perf-demangling-of-ocaml-symbols-a-short-introduction-to-perf/7143. Supposedly those improvements are also going upstream into perf.

[michael-schwarz]

We currently have a practical course at TUM investigating this and related issues.

[jerhard]

I would suggest to close this issue as we already had a look at optimizing by introducing short-circuiting, caching of options, and using flambda. The remaining issue of profiling and optimization then seems overly broad.

[michael-schwarz]

Close as overly broad for now. We should open dedicated issues if we have new ideas.