This directory builds a set of SVCOMP benchmarks based on libvsync. With these benchmarks we hope to reduce the gap between academic tools and industry needs.
The benchmark code is modified in a few ways:
- all atomic accesses are upgraded to be sequentially consistent,
- some algorithms have injected bugs that cause safety violations.
To build the benchmark, you need:
- git, gcc and cmake
- gcc-multilib # to expand the headers for SVCOMP using -m32
With these tools/libraries installed, you can run:
git submodule update --init
cmake -S. -Bbuild
make -C build
The resulting benchmark is in build/target and should be published to
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
To run tests, it's better to use the same docker images used in SVCOMP. These images contain quite outdated compilers (gcc 5 and clang 3.9), and that might influence the tests. Here is how to run the clang compiler used in the competition:
cd sv-benchmarks
docker-runs registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/clang:3.9
make -C c/libvsync -j2 CC=clang-3.9
If some issue happen while building it, run the targets one by one to figure out where the issue is.
make -C build svcomp-copy # copy necessary files into build/...
make -C build svcomp-bugs # apply patch with bugs
make -C build svcomp-expand # expand header conforming SVCOMP requirements
make -C build svcomp-sanity # build the expanded files to check all is ok