Quick note about tests and checking if semantics were compromised with flambda:

• I ran make test once with the original setup (i.e., after running make setup) -> everything went through smoohtly
• I ran make test once with the flambda setup (i.e., after running make setup-flambda) -> everything went through smoohtly here as well

Hence, I presume that if make test works in both cases, then we shouldn't have messed up anything semantics-wise.

Thanks for the PR! There are currently some merge conflicts so the diff also shows some unrelated things that are actually already on master.

Is this just to add the flambda setup or is there already also evidence that flambda indeed provides some speedup?

is there already also evidence that flambda indeed provides some speedup?

Iirc there was a gain of about 1/4 for the SQLite amalgamation when testing locally, but I am sure @mrstanb et al will have the exact numbers.

Thanks for the PR! There are currently some merge conflicts so the diff also shows some unrelated things that are actually already on master.

Is this just to add the flambda setup or is there already also evidence that flambda indeed provides some speedup?

There are indeed some performance improvements. Me and my teammates will make sure to post a follow-up with some stats.

Iirc there was a gain of about 1/4 for the SQLite amalgamation when testing locally, but I am sure @mrstanb et al will have the exact numbers.

Indeed, we'll make sure to post the different results that we had as a follow-up.

From my side the stats are as follows:

• Running Goblint with the base configuration, no optimizations and with the SQLite amalgamation, I got a walltime of 8073.680s
• Running Goblint with the base configuration, with flambda flag -O3 and with the SQLite amalgamation, I got a walltime of 6877.092s

To add such a workflow, you may add a file in .github/workflows that contains the regression job, which is already present in both the locked.yml (this uses a fixed version of compiler and dependencies) and unlocked.yml files.

There's no need to make a new workflow altogether. It suffices to just add one extra compiler version to the unlocked matrix.
A locked version isn't possible with flambda anyway, because the lock file is locked into a non-flambda compiler.

I updated the .github/workflows/unlocked.yml file to include the OCaml compiler version 4.14.x+options. However, I'm not sure if this would be sufficient as a change, since I saw that in the Downgrade dependencies step of lower-bounds-downgrade job ocaml-base-compiler is used which is not the same as the compiler version ocaml-variants which we use with flambda.
Hence, my question: should there be some further changes to the unlocked.yml file? Also, should we specify somewhere the ocaml-option-flambda setting as we do in the golbint.opam.locked file? Otherwise, flambda wouldn't be enabled in the compiler and thus we might remain in the same position as originally.

I think just +options does nothing on its own. You need to actually specify the options like the setup-ocaml documentation shows: https://github.com/ocaml/setup-ocaml#inputs.

The lower bounds jobs are completely separate and need not be modified.

TLDR: After testing out the effects of activating different Flambda flags, we opted for using -O3 without any further options. This leads to a speed-up of approx. 15%. The specification of further inlining options lead to mitigated results, being responsible for alternately improved or worse run-times depending on the system, hence why my teammates and I decided against them.

We started out by running Goblint with different flags over the SQLite Amalgamation. On our private machines, the flag combination -O3 -inline-toplevel=400 -inline-max-depth=1 -inline-max-unroll=0 seemed to be the most promising choice.

To confirm those results, we then proceeded with benchmarking on the CoolMUC-2 HPC of the LRZ in order to achieve reproducible results. Using this configuration, the following measurements were made (format: hours:minutes:seconds):

• No optimizations: 02:37:47
• Flambda with -O2: 02:22:28
• Flambda with -O3: 02:14:31
• Flambda with -O3 -inline-toplevel=400 -inline-max-depth=1 -inline-max-unroll=0: 02:20:23

The runs on the HPC-cluster confirmed our assumption of a noticeable time benefit of using Flambda. However, using just -O3 was the fastest configuration.

To ultimately take a decision on which flags to use, we continued our benchmarking with the coreutils programs of the bench repository. We activated some ana.int.* domains to see if there was some significant changes in the ordering of the above listed combinations.

On our local systems, we marked down this results: coreutils_benchmarks.md. The fastest configuration, again contradicting what we had observed on the HPC, was -O3 -inline-toplevel=400 -inline-max-depth=1 -inline-max-unroll=0.

We then made some further batch jobs on the LRZ-cluster with ana.int.interval, ana.int.def_ecx, ana.int.enums and ana.int.congruence enabled. Only one CPU was used to achieve greater run-times, which allows for better differentiation between all measurements. The cumulated run-times over all coreutils programs were:

• No optimizations: 00:03:00
• Flambda with -O2: 00:02:36
• Flambda with -O3: 00:02:24
• Flambda with -O3 -inline-toplevel=400 -inline-max-depth=1 -inline-max-unroll=0: 00:02:33

Once more, on the HPC, the fastest choice was just -O3. Therefore, as no clear advantage of activating the additional inlining options can be established, we decided that it would be wisest to stick with just -O3, which is now reflected in our PR.

What are the built times on your machines with the flambda compiler with the regular make and with the release profile (make release) compared to the non-flambda compiler switch? That information would help us decide whether we should only keep the flambda switch, or keep it a separate option.

I've benchmarked make release both with Goblint as in the master branch and with flambda -O3 as in this PR. Here are the results for 5 builds each:

No flambda: AVERAGE = 9,777s

• 9,681s
• 9,792s
• 9,812s
• 9,731s
• 9,869s

Flambda with -O3: AVERAGE = 26,075s

• 26,296s
• 26,001s
• 25,992s
• 26,183s
• 25,903s

Thanks! Could you also get the numbers for development build (make)? Hopefully there the slowdown isn't as significant, because it would be slightly annoying.

So for make:

No flambda: AVERAGE = 9,175s

• 9,148s
• 9,245s
• 9,092s
• 9,180s
• 9,208s

Flambda with -O3: AVERAGE = 13,829s

• 13,845s
• 13,765s
• 13,864s
• 13,844s
• 13,828s

I think this sort of slowdown for make is acceptable here.

I would suggest given these numbers that we should default to flambda. @sim642 @stilscher @jerhard 👍 or 👎 ?

Sure, and actually there's probably no need to have -O3 in dev profile anyway because it disables cross-module optimizations. That probably brings the development mode overhead down even further.

Yes, I would also be in favor of making flambda the default and removing the -O3 flag for the dev profile.

In my latest commit, I removed the -O3 flag for make, which lead to slightly improved compilation times:

Flambda with no options: AVERAGE = 12,200s

• 12,487s
• 11,876s
• 12,164s
• 12,482s
• 11,990s

Furthermore, I made the ocaml-variants.4.14.0+options compiler with flambda enabled default (make setup). To still be able to use the ocaml-base-compiler if wished, I added the make setup-base command.