Add ccache support to Dockerfiles and build workflow

[lukovdm]

The PR CI actions where slowing me down quite a bit thus I investigated a bit into how it could be sped up. I added caching of the homebrew downloads and added ccache in all builds with a github cached ccache.

[lukovdm]

It seems like using ccache together with precompiled headers (PCH) does not really work. You get a really low ccache hit rate like this:

Cacheable calls:                     57 / 649 ( 8.78%)
  Hits:                              57 /  57 (100.0%)
    Direct:                          57 /  57 (100.0%)
  Misses:                             0 /  57 ( 0.00%)
Uncacheable calls:                  592 / 649 (91.22%)
  Could not use precompiled header: 592 / 592 (100.0%)

I have done a quick benchmark (on a 24 core machine) of turning PCH on and off with and without a warm cache. These are the results:

PCH	cache state	build (s)	cacheable calls	hits	misses	uncacheable calls
on	cold	178.33	57/649(8.78%)	0/57(0.00%)	57/57(100.0%)	592/649(91.22%)
on	warm	172.48	57/649(8.78%)	57/57(100.0%)	0/57(0.00%)	592/649(91.22%)
off	cold	200.38	648/648(100.0%)	0/648(0.00%)	648/648(100.0%)	0
off	warm	56.97	648/648(100.0%)	648/648(100.0%)	0/648(0.00%)	0

So with a cold cache disabling PCH costs time. But with a warm cache all compile calls actually hit the cache, and it is thus much faster. Most time was taken up by the dependencies.

For the GitHub actions CI we would always have a warmish cache, and thus it seems like it would be worth it to me to disable PCH for them.

For people building storm themselves I don't know, it depends on how much we value cold cache builds versus warm cache builds.

[volkm]

Nice idea @lukovdm! I think it is good to try to decrease the building times in the CI.
I like the idea of using a cache to have incremental builds.

Some thoughts:

• I would probably opt to use the caching for PRs and branches other than master. That way, all feature branches have faster CI by incrementally building new commits. Seeing that most PRs nowadays have multiple iterations, this would decrease the computation times. On the master branch, I would still build from scratch to catch potential issues not detected by the incremental build. In general, I would also run more tests on the master than on the feature branch.
• Interesting to see that PCH have such a negative influence on the cache. Could this be somehow mitigated? I briefly googled and it seems that it should not be a general issues (at least people implemented fixes throughout the years).
• Do you see any cache issues with dependencies? On my local machine, it sometimes feels to me that a large rebuild is triggered even though not much has changed. I suspect a bit that some of the 3rdpary dependencies could have an influence.
• In CMake, I suggest to add a new option STORM_COMPILE_WITH_PCH which allows to enable/disable the PCH. This is similar to STORM_COMPILE_WITH_CCACHE. Edit: According to precompiled headers #451 there is cmake_disable_precompiled_headers
• Why are all the includes necessary now? It is interesting that it compiled before.

[lukovdm]

Thanks for the questions.

• The includes are necessary I think because https://github.com/lukovdm/storm/blob/fc5220f3e1920dab08030f4d47c00111e1883250/CMakeLists.txt#L315 includes several headers for many files.
• About the PCH, looking at these docs, using PCH and pragma once might be the issue: https://ccache.dev/manual/latest.html#_precompiled_headers. But I did not want to change pragma once in all files. I tested a several things to get PCH and ccache to properly work but could not do it.
• The flag and branch things I can implement.
• I have not noticed anything with the dependencies, but they are the slowest part of a warm cache clean build folder build now.

Also, some GitHub workflows are not properly caching yet, but the once that are, are running in 4-10 minutes.

[volkm]

Thanks for the detailed answers.

One thing I noticed looking at the latest CI run, for example here is that carl and sylvan seem to be rebuild each time. I think that might be due to the way how we configure the fetchcontent.

[sjunges]

Thanks Luko!

Do you have any profiling of the compilation process with a warm start? We do have some ways of profiling storm compilation processes and it would be nice to know where the time is lost.

I second Matthias: For the main branch, PCH seems preferable, in particular as I care about the cold start compile time a lot. (Although this is shifting with more people using binaries).
Should we use cmake_disable_precompiled_headers in the STORM_DEVELOPER mode?

If your goal is to speedup the CI, I think it also really gets time to exclude some tests --, for runs where the CI is failing during compilation, that probably doesn't matter that much, but we sometimes have to wait for CI as we cannot run too many things in parallel...

[volkm]

I opened a discussion for a CI revision #894

[volkm]

Related to #763

[lukovdm]

I got some profiles.

• Ignoring the dependencies, with a cold cache, with PCH takes 3m40s, without PCH takes 4m25s. This difference is caused by most files taking a few extra seconds, not one that takes way longer.
• A warm Ccache and PCH results in all dependencies except spot to be compiled basically instantly. Spot is not affected.
• Warm ccache without pch is dominated by spot:

[volkm]

Thanks for the investigation. Looks like spot will be recompiled any time. I think we should figure out why this is happening and whether we can prevent this.

[lukovdm]

I got spot to use ccache and this helped quite a bit again. These benchmarks also have ass tests enabled:

pch	cache_state	build_seconds	cacheable_calls	hits	misses	uncacheable_calls
off	cold	331.26	1558/2004(77.74%)	81/1558(5.20%)	1477/1558(94.80%)	446/2004(22.26%)
off	warm	22.46	1528/1961(77.92%)	1528/1528(100.0%)	0/1528(0.00%)	433/1961(22.08%)
on	cold	286.60	526/2007(26.21%)	24/526(4.56%)	502/526(95.44%)	1481/2007(73.79%)
on	warm	239.90	496/1964(25.25%)	496/496(100.0%)	0/496(0.00%)	1468/1964(74.75%)

And warm cache with PCH off:

[sjunges]

Ok, what I gather from this are a few questios:

• The tests are still really slow. I know I never optimized for them, but why do they not profit from the cache.
• I wonder whether there is more that can be compiled while spot is being built.
• Spot configure seems to be one of the main bottlenecks.

[sjunges]

Regarding spot: We could

1. use system-versions of spot again
2. or we could cache the configure step? (autotools supports cache for the configure step).
3. There also seem to be a few a configure options (such as disabling python bindings) which probably are useful.

[volkm]

• The time for the tests could be mostly the linking time? But ideally they do not need to be rebuild if nothing changed.
• The storm CMake target requires the resources target which contains spot. Other resources such as Cudd, sylvan can be build in parallel with Spot, but Spot takes significantly longer than those.
• The Python bindings should already be disabled.

Things to try:

• System version of Spot: we could install spot via homebrew and try to install the Debian-based packages for Debian and Ubuntu (https://spot.lre.epita.fr/install.html). We currently only use preinstalled Spot in the Docker storm-dependencies.
• Caching the configuration steps could be a good option. But in principle, the reconfiguration should only be run if things changed anyway. So it would be good to figure out why it is reconfigured in the first place.