Enable IPO / LTO and -O3 #6011
Enable IPO / LTO and -O3 #6011
Conversation
|
ubuntu 18 failed: I went with silencing this wrong warning |
rurban
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6011 +/- ##
===========================================
+ Coverage 74.13% 74.26% +0.13%
===========================================
Files 1444 1444
Lines 157322 157322
===========================================
+ Hits 116637 116843 +206
+ Misses 40685 40479 -206
Continue to review full report at Codecov.
|
|
@rurban Would you be able to provide numbers to back up "good performance improvement?" I once tried this myself, and didn't see much of a difference, but perhaps I didn't use a good-enough compiler version or did not try all the options. |
|
FWIW, we already have #3407, which should likely be closed, but equally needed more data. |
|
Performance numbers: Typically 10-20% faster, which aligns to my other projects where -O3 -flto brought about the same improvements. For my project rurban/ctl (the C++ STL in C): make verify
$ time for f in tests/verify/*.c; do /usr/bin/cbmc --bounds-check --pointer-check --memory-leak-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --compact-trace --depth 6 --unwind 6 -I. $f >/dev/null; done
real 0m3.673s
user 0m2.245s
sys 0m0.337s
$ time for f in tests/verify/*.c; do /usr/local/bin/cbmc --bounds-check --pointer-check --memory-leak-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --compact-trace --depth 6 --unwind 6 -I. $f >/dev/null; done
real 0m2.819s
user 0m2.196s
sys 0m0.335s
when I add diff --git CMakeLists.txt CMakeLists.txt
index fe1bd4ca7..dc0602cf5 100644
--- CMakeLists.txt
+++ CMakeLists.txt
@@ -202,6 +202,21 @@ if(ipo_supported)
message(STATUS "IPO / LTO enabled")
set_property(GLOBAL PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
add_definitions(-DLTO)
+ if ((CMAKE_SYSTEM_PROCESSOR STREQUAL "x86_64")
+ OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "i386")
+ OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "i586")
+ OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "i686")
+ OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "amd64") # freebsd
+ OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "AMD64") # windows
+ OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "x86"))
+ set(PROCESSOR_FAMILY "Intel")
+ if(CMAKE_COMPILER_IS_GNUCC
+ OR (CMAKE_C_COMPILER_ID STREQUAL AppleClang)
+ OR (CMAKE_C_COMPILER_ID STREQUAL Clang)
+ OR (CMAKE_C_COMPILER_ID STREQUAL Intel))
+ add_definitions(-march=native)
+ endif()
+ endif()
else()
message(STATUS "IPO / LTO not supported: <${error}>")
endif() |
src/config.inc
Outdated
| @@ -76,7 +79,7 @@ endif | |||
| OSX_IDENTITY="Developer ID Application: Daniel Kroening" | |||
|
|
|||
| # Detailed version information | |||
| CBMC_VERSION = 5.26.0 | |||
| CBMC_VERSION = 5.26.1 | |||
There was a problem hiding this comment.
I think you may have rebased on to a branch other than develop?
There was a problem hiding this comment.
On top of the version PR #6014
|
@rurban Thank you for the timing results. Normally our focus tends to be on run-times in the 10s--1200s run-times. If we get a 10-20% performance benefit on those then that would be a very compelling argument. Am I reading your comments correctly that you are using SatAbs? If so, which version? |
|
I'm using satabs 3.2 with boom 1.8. |
src/util/CMakeLists.txt
Outdated
| @@ -14,7 +14,7 @@ if(GIT_FOUND) | |||
| OUTPUT_STRIP_TRAILING_WHITESPACE | |||
| WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} | |||
| ) | |||
| configure_file(\${CUR}/version.cpp.in version.cpp) | |||
| configure_file(\${CUR}/version.cpp.in \${CBMC_SOURCE_DIR}/util/version.cpp) | |||
There was a problem hiding this comment.
🚫 Please drop this commit as this "fix" is not needed.
There was a problem hiding this comment.
without it version.cpp gets generated in the build dir. and the new version is ignored.
There was a problem hiding this comment.
The version.cpp in the build dir is compiled and linked into the build. Ignoring this file would result in a failed build as it would not exist elsewhere. The latest Ubuntu build on our release page shows the correct version number when I download and install it and it was built without this proposed change. I also end up with CBMC builds showing the correct version number for builds I produce locally, with altered version numbers in config.inc. Under what conditions have you seen incorrect version numbers?
If you have also built cbmc using make and the makefiles, then you can end up with a version.cpp in the cbmc/src/util directory. that would be a stale build artefact, from the build in place nature of the make build. It should not be committed to git. To my knowledge it is correctly ignored and neither overwritten or linked by the cmake build, if it exists.
There was a problem hiding this comment.
Sorry. You are right. My mistake with the wrong prefix.
In the general case build vs src mixup, you need to build out of src to get wrong version.cpp files
|
Would you mind including the following patch (or something to that effect): --- a/src/solvers/CMakeLists.txt
+++ b/src/solvers/CMakeLists.txt
@@ -109,7 +109,13 @@ elseif("${sat_impl}" STREQUAL "cadical")
)
message(STATUS "Building CaDiCaL")
- execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+ if("${CMAKE_BUILD_TYPE}" STREQUAL "Release")
+ execute_process(COMMAND make CXXFLAGS=${CMAKE_CXX_FLAGS_RELEASE} WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+ elseif("${CMAKE_BUILD_TYPE}" STREQUAL "RelWithDebInfo")
+ execute_process(COMMAND make CXXFLAGS=${CMAKE_CXX_FLAGS_RELWITHDEBINFO} WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+ else()
+ execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+ endif()
target_compile_definitions(solvers PUBLIC
SATCHECK_CADICAL HAVE_CADICALto ensure the CaDiCaL solver is also built with the new options? |
rurban
force-pushed
the
develop
branch
2 times, most recently
from
7b54c81 to
6ca4ab2
Compare
There was a problem hiding this comment.
Is there a reliable way in CMake to obtain the actual compile flags? As a CMake noob the best I could find is not using add_definitions and instead going for set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} ...") so that CMAKE_CXX_FLAGS_RELEASE can be used. I'm asking to make sure the CaDiCaL build actually benefits.
| if(ipo_supported) | ||
| message(STATUS "IPO / LTO enabled") | ||
| set_property(GLOBAL PROPERTY INTERPROCEDURAL_OPTIMIZATION True) | ||
| add_definitions(-DLTO) |
There was a problem hiding this comment.
CMake noob here: could we use set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -DLTO") instead?
There was a problem hiding this comment.
Yes, but this is easier. It only adds it to the Release flags anyway, because only there ipo_supported will be true.
There was a problem hiding this comment.
Understood, but then I wasn't able to find a way to surface this to the CaDiCaL build configuration. You might know how to make this work?
CMakeLists.txt
Outdated
| if(CMAKE_COMPILER_IS_GNUCC | ||
| OR (CMAKE_C_COMPILER_ID STREQUAL AppleClang) | ||
| OR (CMAKE_C_COMPILER_ID STREQUAL Clang) | ||
| OR (CMAKE_C_COMPILER_ID STREQUAL Intel)) | ||
| add_definitions(-march=native) |
There was a problem hiding this comment.
| if(CMAKE_COMPILER_IS_GNUCC | |
| OR (CMAKE_C_COMPILER_ID STREQUAL AppleClang) | |
| OR (CMAKE_C_COMPILER_ID STREQUAL Clang) | |
| OR (CMAKE_C_COMPILER_ID STREQUAL Intel)) | |
| add_definitions(-march=native) | |
| if(CMAKE_COMPILER_IS_GNUCC | |
| OR (CMAKE_CXX_COMPILER_ID STREQUAL AppleClang) | |
| OR (CMAKE_CXX_COMPILER_ID STREQUAL Clang) | |
| OR (CMAKE_CXX_COMPILER_ID STREQUAL Intel)) | |
| set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -march=native") |
There was a problem hiding this comment.
CXX compiler! good catch
There was a problem hiding this comment.
I think you might actually need both the C and CXX variants?
|
On Tue, 2021-04-06 at 12:30 -0700, Reini Urban wrote:
I'm using satabs 3.2 with boom 1.8.
I haven't checked for updated versions there. I still run into WIP
array stuff there.
```
Refining set of predicates according to counterexample (WP)
*** CEGAR Loop Iteration 2
Computing Predicate Abstraction for Program
sorry, wp(array_copy...) not implemented
```
At the risk of side-tracking this PR, I am surprised to run find
someone using SatAbs. I had thought it long dead.
The last version I have was built on CBMC 4.7 which was released in Jan
2014. As far as I know that was a case of light maintainance and the
last time it had active development was probably pre-2012.
I am not aware of any currently available copies of the source code. I
have a check out of the subversion from late 2015 and I can send you
that / post it on github if you would like. I believe at least one of
@tautschnig or @Schrammel has a more up-to-date one. I don't know
which version I have and it will almost certainly take a non-trivial
amount of work to get it to build / work with more modern versions of
CPROVER.
Given the improvements we have made to CPROVER, I do wonder whether it
might be better to just rewrite it completely if there is interest.
|
|
Cannot repro the ubuntu20 cmake-gcc crash, but looks bad. Was introduced by I also notized that the GLOBAL target did not enable all targets to be compiled with |
|
Hello @martin-cs! I never had the source code of this project, sorry,I believe that you have marked the wrong person... |
| OR (CMAKE_C_COMPILER_ID STREQUAL AppleClang) | ||
| OR (CMAKE_C_COMPILER_ID STREQUAL Clang) | ||
| OR (CMAKE_C_COMPILER_ID STREQUAL Intel)) | ||
| add_definitions(-march=native) |
There was a problem hiding this comment.
I'm a bit nervous of the -march=native - if I'm reading the CMake correctly (a big if :-) ) then this is enabled by default on release builds, but thats quite likely to cause problems building CBMC release distributions (or at least, be a trap waiting to cause problems). native means "use any instructions available on the build machine" I believe - but we've got no real guarantee that our build machines are not higher spec/newer CPUs/whatever than any of the downstream users of our binary packages, meaning they run the risk of getting illegal instruction crashes/traps from our released binaries. While we could override default options for our binary packaging, I'd feel much more comfortable if we didn't have to...
There was a problem hiding this comment.
True. Packagers need to get rid of that somehow. Maybe only add it to CFLAGS and CXXFLAGS via env. The idea was to find sloppy visibility and alignment, and test it in develop. Also have locally fast binaries
|
While I'm definitely supportive of "free speed" form -O3/LTO - I must admit I'm a bit weary of enabling both of these by default. In all honesty, I may just be being paranoid for the decade I spent working as a compiler engineer, :-) but I've seen an awful lot of codegen bug reports where '-O3' was a common factor - and codegen bugs are insidious to discover. Given what CBMC is, and that this PR enables |
|
The Same for |
That suggests 1) adding code to permit building with that configuration and 2) adding a further GitHub action using that configuration rather than making it the default? Also, can you provide some hints on how to best debug this? I wasn't able to reproduce the failure on a 20.04 system myself. |
LTO and -O3 give a good performance improvement. I would not recommend -O3 with bad compiler versions though, such as gcc-9. WIP: GLOBAL properties are not enough, add the IPO property to all targets. Which leads to various problems still.
not valid on arm or other archs. Only for gcc-compatible compilers. 30% faster on small samples than -flto
Create version.cpp in the src dir, where it is picked up. And not in the build dir. Update only if different to avoid needless recompilations. Repro: check bin/cbmc --version for the correct version.
|
I'll redo in a new branch, because of the blockers |
|
It might be worth considering |
|
LTO is harder to achieve. O3 is riskier to fall into compiler bugs. I found several. |
LTO and -O3 give a good performance improvement.
I would not recommend -O3 with bad compiler versions though, such
as gcc-9