|
The archives contain the required executables
SymmPa and bboom. For code pre-processing SymmPa requires the gcc
environment. You must also add the directory containing the binary of
bboom to your PATH environment variable before
executing SymmPa.
SymmPa
uses the MiniSat 2 SAT solver during
abstraction and simulation. You do not need to download MiniSat; it is part
of the SymmPa executable.
Preparing Input Programs
Prior to using SymmPa, consider reading Section 5 of the Cprover manual which explains how to use
nondeterminism, assumptions and assertions.
In addition to the usual Cprover built-in functions __CPROVER_assume
and __CPROVER_assert, SymmPa supports the following new features:
- Magic labels in the form of
__CPROVER_ASYNC_1, __CPROVER_ASYNC_2 etc. to dynamically spawn new threads.
__CPROVER_atomic_begin() and __CPROVER_atomic_end() functions to declare critical sections with strong atomicity semantics.
SymmPa performs automatic
counterexample-guided abstraction refinement, thus in many cases it can
verify programs fully automatically. However, it can be useful to specify
predicates explicitly, either because automatic refinement is too weak, or
for comparison with other tools. This can be achieved using the following
built-in functions:
__CPROVER_predicate(cond) to specify user-defined predicates. __CPROVER_parameter_predicates() to add call-site relating predicates for parameters. __CPROVER_return_predicates() to add call-site relating predicates for return values.
The following test_and_set lock with
exponential backoff (source code: tsl.c) demonstrates how to use some
of these features. The program is adapted from Algorithms for
scalable synchronization on shared-memory multiprocessors (Algorithm 1).
enum lock_t {unlocked, locked};
volatile enum lock_t lock = unlocked;
void pause(int delay){
assert(delay >= 0);
return;
}
enum lock_t TestAndSet() {
enum lock_t oldValue;
__CPROVER_atomic_begin();
oldValue = lock;
lock = locked;
__CPROVER_atomic_end();
return oldValue;
}
void acquire_lock(){
int delay;
enum lock_t cond;
delay = 1;
cond = TestAndSet();
while(cond == locked){
pause(delay);
if(delay<2048) {
delay *= 2;
}
cond = TestAndSet();
}
assert(cond != lock);
}
void release_lock(){
assert(lock != unlocked);
lock = unlocked;
}
int c = 0;
void TAS_backoff__main(){
while(1){
acquire_lock();
c++; assert(c == 1); c--;
release_lock();
}
}
int main(){
while(1){
__CPROVER_ASYNC_1: TAS_backoff__main();
}
}
Command line interface
For instructions on how to use SymmPa, run the tool as follows:
SymmPa --help
For example to check the user-specified assertions in the example from above with up to 3 threads execute
SymmPa --full-inlining --concurrency --max-threads 3 ./tsl.c
SymmPa
will then first try to verify the properties for one thread. If it fails,
it reports an appropriate trace over the input program; if it succeeds it
continues with the next thread count. Note, that larger thread counts might
require additional predicates, and thus additional CEGAR iterations.
For the lock example, the output of the first iteration
is as follows:
*** CEGAR Loop Iteration 1
Predicates are:
cond == oldValue
pause::delay == acquire_lock::delay
delay >= 0
delay < 2048
cond == lock
c == 1
lock == enum(0)
Computing Predicate Abstraction for Program
Running B-BOOM
Simulating abstract counterexample on concrete program
Solving with MiniSAT2
Trace is spurious
Refining set of predicates according to counterexample (WP)
The initial set of predicates contains assertion conditions, as well as
predicates that are defined explicitly via __CPROVER_predicate
or implicitly via __CPROVER_parameter_predicates and
__CPROVER_return_predicates (here none). In iteration 3 B-Boom can verify the abstraction
safe for one thread, iteration 4 then suffices to do so for 2 and 3 threads,
whereupon SymmPa terminates
with the following output:
*** Results for 3 threads: ***
Time: 10.472 total, 3.624 abstractor, 6.57 model checker, 0.006 simulator, 0.004 refiner
Thread count: 3 of 3
Iterations: 4
Predicates: 13
Breakdown of predicate types:
shared: 4
local: 7
mixed: 2
VERIFICATION SUCCESSFUL
Note that SymmPa can prove the program correct even if the
user-defined predicates are removed. In the above example, verification is
actually significantly faster, since initial abstractions, with few
predicates, are very cheap to compute:
*** Results for 3 threads: ***
Time: 4.622 total, 1.749 abstractor, 2.614 model checker, 0.008 simulator, 0.006 refiner
Thread count: 3 of 3
Iterations: 5
Predicates: 12
Breakdown of predicate types:
shared: 4
local: 6
mixed: 2
VERIFICATION SUCCESSFUL
Benchmarks for CAV paper
You can either navigate the
benchmarks online, or download an archive of benchmarks to
try out with the tool.
To apply SymmPa to a benchmark, ensure that bboom
and SymmPa are on your path, and type (e.g. for up to 3
threads):
SymmPa --full-inlining --concurrency --max-threads 3 ./main.c
where main.c is the C file associated with the benchmark.
Bug reporting
If you found a bug, please report it using our SymmPa and B-Boom Bugzilla databases.
This research is supported by EPSRC
grants 'Efficient Verification of Software with Replicated Components'
(G026254) and 'Advanced Formal Verification Techniques for Heterogeneous
Multicore Programming' (G051100).
| 
