Yogar-CBMC-Parallel is a parallel version of Yogar-CBMC, which employs multiple engines to refine the abstraction in parallel.
It contains two parts, the master procedure and the single Yogar-CBMC.
The master procedure manages the shared resources and starts multiple processes of yogar-cbmc to perform the refinement.
The single Yogar-CBMC performs its own refinement and exchanges refinement constraints at its end of each iteration.
To compile the master procedure, enter the master directory and use the following command to obtain the procedure yogar-cbmc-parallel
g++ yogar-cbmc-parallel.cpp -o yogar-cbmc-parallel
To compile the single Yogar-CBMC, enter the yogar-cbmc/src directory and use the following command to obtain the procedure yogar-cbmc
Then copy the two procedures yogar-cbmc-parallel and yogar-cbmc into the same directory, when we run yogar-cbmc-parallel, it will start multiple yogar-cbmc processes.
- Usage (SV-COMP 2019) *
To run Yogar-CBMC-Parallel, use the following command-line from this directory:
./yogar-cbmc-parallel [--thread-num N]
where is the filename to be verified.
The counterexample will also be written in counterexample.witness.
To run Yogar-CBMC-Parallel for SV-COMP benchmark, use the following command-line from this directory:
PYTHONPATH=. benchexec -r "sv-comp19" -t Concurrency --no-container yogar-cbmc-parallel.xml
We assume that benchexec has been installed already.
This binary of Yogar-CBMC-Parallel runs on Ubuntu of 64bit.
Liangze Yin, Wei Dong, Wanwei Liu, Ji Wang, Haining Feng