Upgrade to OCaml 5.0 as default

[sim642]

Closes #1003.

We can finally do this because mlgmpidl and apron have been released on opam for OCaml 5.0.

TODO

• Merge Upgrade to OCaml 5.0 gobview#26.

[sim642]

I did an sv-benchmarks run comparing OCaml 4.14 with OCaml 5.0 and the results are concerning. We might have to postpone making OCaml 5.0 the default and simply cherry-pick the changes from here to at least make Goblint OCaml 5.0 compatible, even if we don't use it by default.

Memory usage is significantly higher, almost 10× in some cases:

CPU time is also affected but that could be simply due to working with more memory:

(Full results)

[michael-schwarz]

Should we investigate what the performance is like with OCaml 5.1?

[sim642]

I tried 5.1 at some point and it wasn't much better, still a regression from 4.14.
OCaml 5.2 is around the corner, so that's another thing to try.

[michael-schwarz]

Sounds like 5.2 (released today) also won't fix our problems: https://discuss.ocaml.org/t/ocaml-5-2-0-released/14638

OCaml 5.2.0 is still a somewhat experimental release compared to the OCaml 4.14 branch. In particular

• [...]
• Ephemeron performances need to be investigated.

[FelixKrayer]

Just as a quick note here:
The version of the dependency of camlidl will have to be changed to version 1.12, as the current camlidl = 1.11 requires ocaml < 5.0.

[sim642]

All the dependencies in the Goblint lock file are for 4.14 anyway: the lock file also specifies OCaml 4.14. The non-locked dependencies allow appropriate versions to be installed on OCaml 5.0, 5.1 and 5.2.

[sim642]

I might have to redo the 4.14 vs 5.x (5.3 now) runs now because a lot seems to have changed (in Goblint). I tried a few worst cases from my previous runs to see if they remain, but couldn't find an example of regression due to OCaml. Rather, some just got faster/slower on OCaml 4.14 even.

Having some significant examples of regression would allow us to open an issue with OCaml. The maintainers are interested in cases where performance regressions from OCaml 5 are holding things back: https://discuss.ocaml.org/t/ocaml-5-3-0-released/15916/4.

[DrMichaelPetter]

If it helps, I can set up a regular job on our servers, e.g. comparing runtimes of a sample set. We would need some way of building 4.14 and 5.x in an unsupervised fashion, though.

[sim642]

I now opened an issue with OCaml, including an updated benchmark for the current Goblint and OCaml 5.3: ocaml/ocaml#13733. The large blob of 10× memory usage cases seems gone, but performance isn't clearly on par with 4.14 either.

[michael-schwarz]

Random thought: Have you tried with the mitigation for #1513 for the example where we have a 5x slowdown?