SymmPa

What is SymmPa

SymmPa is a model checker for concurrent ANSI-C programs with dynamic thread-creation. It verifies properties, such as array bounds (buffer overflows) and user-specified assertions for a bounded number of threads.

For questions about SymmPa contact alastair.donaldson@imperial.ac.uk, michael.tautschnig@cs.ox.ac.uk or alexander.kaiser@cs.ox.ac.uk.

You should also read the license.

New: see a video of Alastair presenting SymmPa.

Read the paper!

Download and installation

We currently distribute binaries for 64-bit Linux only. In order to use SymmPa you will also need to download the Model Checker B-Boom.

Date x86 Windows Linux
25-Oct-2011
on request
SymmPa-0.1-linux-x86-64.tar.gz
26-Oct-2011
bboom-0.5-win-x86-32.tar.gz
bboom-0.5-linux-x86-64.tar.gz

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).