Add ccache support to Dockerfiles and build workflow - #892
Conversation
|
It seems like using ccache together with precompiled headers (PCH) does not really work. You get a really low ccache hit rate like this: 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:
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. |
…kflow; add benchmark script for compile time analysis
|
Nice idea @lukovdm! I think it is good to try to decrease the building times in the CI. Some thoughts:
|
|
Thanks for the questions.
Also, some GitHub workflows are not properly caching yet, but the once that are, are running in 4-10 minutes. |
|
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. |
|
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). 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... |
|
I opened a discussion for a CI revision #894 |
|
Related to #763 |
|
I got some profiles.
|
|
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. |
|
I got spot to use ccache and this helped quite a bit again. These benchmarks also have ass tests enabled:
And warm cache with PCH off: |
|
Ok, what I gather from this are a few questios:
|
|
Regarding spot: We could
|
Things to try:
|
…om different sources. Currently we have the old every PR commit trigger and a PR label trigger. They can have different configs.
…and job configurations. Adress comments. Test if gcc exception is neccesary.
|
One storm parser test fails only on macos intel. It is quite a weird bug, this is what claude thinks about it:
I would suggest for now working around it and possibly making an issue. |
…p-object to source file, test where -Wno-deprecated-declarations of apple clang fails, small fixes
This reverts commit 3bf30bb.
|
The addition of |
This should indeed be a separate issue. Good thing that the CI now catches this issue. Support for Intel will also be dropped with the upcoming release of macOS 27 anyway. |
|
Not using PCH removed stdint as a header from a lot of files which used its int types. Thus they had to be added manually. |
|
Right, thanks for the clarification. So there are two main parts to this PR:
I guess it is not easily possible to cherry-pick the commits for 1. and make a separate PR for a nicer division of concerns? |
|
Yes correct, and indeed I think cherry picking out those commits will be quite difficult. |
|
Also, the latest CI run failed on a bus error in test-parser, I have no clue why this is going wrong. And it seems some caching is not working as the CI runs are taking around 40min again. |
|
The PCH changes were part of the separate #974 to clean up this PR a bit. |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 16 out of 17 changed files in this pull request and generated 7 comments.
Suppressed comments (8)
src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp:643
- These
#pragma GCC diagnosticdirectives should be guarded to avoid toolchains that don’t recognize the warning group (notably Clang warninging on unknown warning groups under -Werror/-Wunknown-warning-option). Consider wrapping them in a compiler/version check (e.g., GCC-only and__GNUC__ >= 15) so the suppression only applies where needed.
// GCC 15 raises a false positive -Wfree-nonheap-object when compiling SparseDtmcEliminationModelChecker
// with GMP rational functions (STORM_USE_CLN_RF=OFF) in Release mode: the inlined std::vector destructor
// for MatrixEntry<..., RationalFunction<..., GMP>> is incorrectly flagged. Not a real memory error.
// See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108846
#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wfree-nonheap-object"
src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp:884
- These
#pragma GCC diagnosticdirectives should be guarded to avoid toolchains that don’t recognize the warning group (notably Clang warninging on unknown warning groups under -Werror/-Wunknown-warning-option). Consider wrapping them in a compiler/version check (e.g., GCC-only and__GNUC__ >= 15) so the suppression only applies where needed.
#pragma GCC diagnostic pop
src/storm-parsers/parser/SpiritParserDefinitions.h:10
- This adds a conditional
#pragma clang diagnostic pushbut the diff doesn’t show a corresponding conditional#pragma clang diagnostic pop. Without a matching pop under the same#if, the deprecation suppression can leak beyond the intended include scope. Prefer placing a matching pop shortly after the Boost Spirit includes (and under the same#if defined(__clang__) && defined(__apple_build_version__)).
// Boost Spirit's utf8.hpp uses char_traits<ucs4_char> which Apple libc++ (Xcode 26+) deprecated
#if defined(__clang__) && defined(__apple_build_version__)
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wdeprecated-declarations"
#endif
resources/3rdparty/include_spot.cmake:70
- In the debug branch,
--disable-devellooks inconsistent with the intention of “building Spot in DEBUG mode” (previously this was--enable-devel). If Spot’s debug builds rely on devel mode (common for autotools projects), this may unintentionally reduce debug functionality or change build outputs; consider restoring--enable-devel(or clarifying why devel must be disabled).
set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--disable-debug;--enable-optimizations")
else()
message(WARNING "Storm - Building Spot in DEBUG mode.")
set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--enable-debug;--disable-optimizations")
endif()
if (CCACHE_FOUND)
set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};CC=ccache\\ ${CMAKE_C_COMPILER};CXX=ccache\\ ${CMAKE_CXX_COMPILER}")
endif()
CMakeLists.txt:161
- This unconditionally overrides
STORM_COMPILE_WITH_PCHwheneverSTORM_DEVELOPERis enabled, which can surprise users/CI callers explicitly setting-DSTORM_COMPILE_WITH_PCH=ON. Prefer only setting a default when the variable is not already defined (or making the behavior explicit via a separate option likeSTORM_DEVELOPER_DISABLE_PCH_BY_DEFAULT).
# Turn off PCH for faster ccache usage on warm caches. PCH compiled files cannot be properly cached currently.
# TODO: remove and explicitly set if needed
set(STORM_COMPILE_WITH_PCH OFF)
.github/workflows/test-mac.yml:57
- This cache key hashes
.github/workflows/buildtest.yml, but that workflow is removed in this PR.hashFiles(...)will become empty/constant, weakening invalidation when brew-related behavior changes. Consider hashing relevant current workflow files (or a dedicated dependency manifest) instead.
key: buildtest-brew-${{ inputs.distro }}-${{ hashFiles('.github/workflows/buildtest.yml') }}
.github/workflows/test-mac.yml:69
- Using
${{ github.run_id }}in the primary cache key guarantees a new cache entry every run. While restore-keys will reuse prior caches, saving with a run-unique key can create excessive cache churn and wastes cache quota. Consider using a stable key (e.g., based on branch/ref + buildType + relevant hashes) and rely on restore-keys for fallback.
key: buildtest-ccache-macos-${{ inputs.distro }}-${{ inputs.buildType }}-${{ github.run_id }}
.github/workflows/ci-weekly.yml:198
- Brand capitalization: change
Github ActionstoGitHub Actionsfor consistency.
from: Github Actions <you-broke-it@stormchecker.org>
| set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--enable-debug;--disable-optimizations") | ||
| endif() | ||
| if (CCACHE_FOUND) | ||
| set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};CC=ccache\\ ${CMAKE_C_COMPILER};CXX=ccache\\ ${CMAKE_CXX_COMPILER}") |
| RUN if ! command -v ccache >/dev/null 2>&1; then \ | ||
| if command -v apt-get >/dev/null 2>&1; then \ | ||
| apt-get update && apt-get install -y --no-install-recommends ccache && rm -rf /var/lib/apt/lists/*; \ | ||
| elif command -v apk >/dev/null 2>&1; then \ | ||
| apk add --no-cache ccache; \ | ||
| elif command -v pacman >/dev/null 2>&1; then \ | ||
| pacman -S --noconfirm ccache; \ | ||
| else \ | ||
| echo "No supported package manager found for ccache installation"; \ | ||
| fi; \ | ||
| fi |
| # Relax the caching keys | ||
| # pch_defines tries to ignore precompiled headers (but often does not succeed in our case) | ||
| # the time options ignore time macros when calculating the cache key, improving cache hit rates | ||
| set(ENV{CCACHE_SLOPPINESS} "pch_defines,time_macros,include_file_mtime,include_file_ctime") |
| - name: Run tests | ||
| working-directory: ./build | ||
| run: ctest test --output-on-failure |
| - name: Run tests | ||
| run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" |
| - name: Run tests | ||
| # Disabled sanitizer checks for now | ||
| #run: docker exec ci bash -c "cd /opt/storm/build; ASAN_OPTIONS=detect_leaks=0,detect_odr_violation=0 ctest test --output-on-failure" | ||
| run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" |
| - name: Run tests | ||
| run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" |
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.