storm
storm copied to clipboard
moves-rwth
Compile Times
Generally, we are still fighting relatively long compile times despite major efforts to reduce them. I wanted to open this issue for some time to push us to improve here a bit further.
Earlier today, I generated a ninjatrace for building storm, completely, as a release build. This took 8m20s on my laptop, running 8 threads in parallel.
I attach the file here, you can open it in chrome://tracing to inspect it yourself. I also attach a screenshot
You can see that on storm-main, many files actually compile rather quickly, however, towards the later stages, compile times increase drastically. I believe that this effect is mostly due to earlier efforts to reduce the compile times of often-recompiled parts.
I inspected one file, CtmcCslModelCheckerTest.cpp. This file took a whopping 30 seconds to compile. Why? With clang-profiling (see our Cmake option to enable this), it turned out that around 23s were due to including FormulaParser.h and PrismParser.h. There was a simple improvement to compile this file in 7 seconds rather than in 30: Do not include these two files. The code still compiles.
Regarding header includes
I did some further experiments. E.g., every file that includes in some way or the other carl's multivariate polynomials also includes the carl file FunctionSelector which depends on boost/mpl and this adds roughly 100ms of compilation time. Negligble for an an individual file, but maybe not negligible overall.
Furthermore, quite a significant amount of time is spent on standard headers. My experiments show that precompiled headers are a solution here and can speed up the overall compilation from around 8 to around 6 minutes! :-)
Quite some files include the expression-evaluator, which includes exprtk.h (700ms).
Finally, every file that includes logging includes the filesystem header (also 100ms) as l3pp is a header-only library. I think that we may want to move the implementation of file handling to a dedicated file.
Regarding instantiations Some instantiations indeed add a lot of time, e.g., some key operations on multivariate polynomials (together roughly 600 ms?) and the json library (700ms) I think we may want to use extern template instantiations to compile them only once.
Regarding unity builds Switching on unity builds is currently not working as there are some carl headers which can only be included in a specific order and this somehow failed with cmake unity builds. It may be possible to fix this issue.
Regarding storm-pars and tests The main issue is actually the use of storm headers that include many parsers and therefore cost various seconds to include.
Another issue seems to be the use of carl::formula. However, we hardly use them and the use-cases for them are mostly gone, so I would argue to switch to storm::expressions.
Regardint tests Another header that is currenlty widely used in tests that is very expensive is the parser/DirectEncodingParser.h as this includes the valueparser.h and thus all the spirit-definitions. This seems not necessary ...
Significant include optimisations for tests and libraries: https://github.com/moves-rwth/storm/pull/450
Instantiations for json objects are significantly reduced by: https://github.com/moves-rwth/storm/pull/459
Just for (my) documentation:
- traces can also be viewed with Firefox profiler, Speedscope or Perfetto.
- ninjatracing for creating json files from ninja build log
