Bfc - A Widening Approach to Multi-Threaded Program Verification

What is Bfc (aka Breach)

Bfc solves the coverability problem for multi-threaded programs. This problem subsumes classical safety properties like program location reachability, program assertions, mutual exclusion, etc. for an unbounded number of statically, or dynamically created threads. Bfc implements a variant of the Target Set Widening algorithm [1]. As input it takes a Monotone Dual-reference Program (MDRP), a model of concurrency that is equally expressive as Petri nets with transfer arcs [2].

For questions about Bfc contact Alexander Kaiser (alexander.kaiser@cs.ox.ac.uk), Daniel Kroening (kroening@cs.ox.ac.uk), or Thomas Wahl (wahl@ccs.neu.edu).

You should also read the license.

Content

  1. Download
  2. Input language
  3. Command line interface
  4. Proving the parameterized ticket algorithm
  5. Model Checking for Multi-Threaded ANSI-C Programs using Satabs
  6. C Program Benchmarks and Experimental Results
  7. Sources
  8. References

1. Download

We currently distribute binaries for 32-bit Windows and 64-bit Linux.

Date x86 Windows Linux
19-Jun-2015
bfc-2.0.2-win-x86-32.tar.gz
bfc-2.0.2-linux-x86-64.tar.gz
16-Jun-2015
on request
wrap-linux-1.1-x86-64.tar.gz
7-Feb-2013
on request
spec2tts-1.0-linux-x86-64.tar.gz
23-Jan-2012
bfc-1.0-win-x86-32.zip
bfc-1.0-linux-x86-64.tar.gz
31-Jan-2012
on request
ttstrans-1.0-linux-x86-64.tar.gz

The archives contain the executables bfc, a wrapper that is currently needed to use bfc as verification back-end for the C program model checker Satabs, and the tools ttstrans and spec2tts to translate a restricted class of MDRPs into various Petri nets formats and vice versa (used by, e.g., Ist-Bc, Csc-Km and Eec-Ar [3,5], Petr-Bc [4], and Tina-Km [6]).

2. Input Language

The tool bfc takes the following language as input:

<PROG> ::= <SDim> <LDim>
           [<TRANS>]*
<TRANS> ::= <THREADSTATE> ("->"|"+>) <THREADSTATE> [<LOCALTRANSFER>]*
<THREADSTATE> ::= SHAREDSTATE LOCALSTATE
<SHAREDSTATE> ::= "0"|"1"|...|"SDim-1"
<LOCALSTATE> ::= "0"|"1"|...|"LDim-1"
<LOCALTRANSFER> ::= <LOCALSTATE> ~> <LOCALSTATE>

Every non-recursive multi-threaded program with finite-domain variables gives rise to a MDRP as follows. Thread transitions with separator -> and +> define thread and spawn transitions, resp. Thread transitions affect the local state of exactly one existing thread and spawn transitions the local state of the new thread. Local transfer transitions affect the local state of all threads passive in a transition that reside in a source local state of the LOCALTRANSFER block.

Example The following program


Shared variable s (domain: 0,1,2,3)
Local program counter (domain: L0,L1,L2)
L0:  atomic {
     if(s!=0)
       goto 0;
     else
       s=3;}
L1:  atomic {
     if(s!=3)
       goto 1;}


L2:  atomic {
     if(s==2)
       goto 2;
     s=(s+1)mod4;
     goto 0;}

induces the following MDRP (intermediate states of atomic sections are omitted, character # starts a comment)

4 3
0 0 -> 3 1 #1st line
3 1 -> 3 2 #2st line
1 2 -> 2 0 #3st line
0 2 -> 1 0 #3st line
3 2 -> 0 0 #3st line

To illustration transfer transitions of passive threads: Suppose the execution of the first instruction shall i) swap the program counter of all passive threads in the last two instructions, and ii) permit (but not forcing) all passive threads in the first location to move into the last.This can be encoded by replacing the last transition with 0 0 -> 3 1 1 ~> 2 2 ~> 1 0 ~> 0 0 ~> 2.

3. Command line interface

For instructions on how to use Bfc, run the tool as follows:

bfc -h

The parameterized initial state is (0|0,0,...), that is, initially the shared state is 0 (number preceding "|"), and an arbitrary number of threads reside in local state 0 (sequence following "|"). The inital state can be changed via option -i.

Checking program properties

To check coverability of, e.g., the state (0|2,2), i.e. shared state is 0 and two threads reside in program location 2, in the example from above run

bfc --target "0|2,2" ./example.mdrp

This will produce the output

Input file ./example.mdrp successfully opened
Running coverability engine...
total time: 0.0031290000
VERIFICATION SUCCESSFUL

Hence, state (0|2,2) is uncoverable: no two thread threads can simultanously occupy the last program instruction when, at the same time, the shared variable evaluates to 0.

4. Proving the parameterized ticket algorithm using Bfc

The next example shows how the ticket busy-wait lock algorithm can be proved correct using Bfc. A simple implementation of the tickel lock algorithm is as follows:

struct Spinlock {
  natural s := 1; // ticket being served
  natural t := 1; }; // next free ticket

struct Spinlock lock; // shared

void spin_lock() {
  natural l := 0; // local
  L1: l := fetch_and_add(lock.t);
  L2: while (l != lock.s) /* spin */ ; }

void spin_unlock() {
  L3: lock.s++; }

Shared variable lock has two natural-number components: s holds the number of the ticket currently being served, while t holds the next free number (if no thread is currently served, we have s = t). To request access to the protected region, a thread atomically retrieves the value of t into local variable l and then increments t. The thread then spins until l equals s. To unlock, s is incremented.

The algorithm uses natural number and may be executed by an unbounded number of threads. While Bfc can deal with the former infinity, the latter would require infinitely many local and shared states. To eliminate the infinite-data variables we compute the monotone closure of the inter-thread predicate abstraction of the ticket algorithm, as described in [8,9]. We therefore use these three predicates: l != lP, t > max(l, lP) and s = l. The first two are inter-thread; the third is single-thread. The predicates assert the uniqueness of a ticket, that the next free ticket is larger than all tickets currently owned by threads, and that a thread's ticket is currently being served, respectively.

As a result of the abstraction process, we get the MDRP ticketabs.tts. The initial and error states are 0/24, meaning an unbounded number of threads intially resides in the first program location. The mapping between local state integers and predicate valuation is given in the MDRP program.

To prove that no two thread can simultaneously be between the calls to functions spin_lock and spin_unlock, run the tool as follows:

bfc --init "0/24" --target "1|25,25" ./ticketabs.tts

The error state 1|25,25 means that 2 threads have entered the critical section. This will produce the output

Input file ./ticketabs.tts successfully opened
Running coverability engine...
total time: 0.01
VERIFICATION SUCCESSFUL

The result confirms parameterized mutual exclusion: no matter how many threads try to acquire and release the lock concurrently, no two of them are simultaneously be between the calls to functions spin_lock and spin_unlock.

5. Model Checking for Multi-Threaded ANSI-C Programs using Satabs

Prior to using Satabs (get the lastest version here) with Bfc as model checking back-end, consider reading Section 5 of the Cprover manual which explains how to use nondeterminism, assumptions and assertions. An introduction to the concurrency component of Satabs is given in the C program benchmarks provided below.

To apply Satabs to a C program download the model checking wrapper from above, and ensure that bfc, satabs and the included files boom and bboom are on your path, and type

satabs --full-inlining --concurrency --build-tts ./main.c

where main.c is the C file to be verified. The option --build-tts activates the MDRP abstract language interface extension; abstract MDRPs are then generated on-the-fly. If the program is safe, the output will look like this:

file main.c: Parsing
Converting
Type-checking main
Generating GOTO Program
...
*** CEGAR Loop Iteration 4
Computing Predicate Abstraction for Program
Running BOOM
boom --stats -t --threadbound 2 cegar_tmp_abstract.bp
Time: 3.333 total, 1.118 abstractor, 1.623 model checker, 0.007 simulator, 0.576 refiner
Iterations: 4
Predicates: 3
VERIFICATION SUCCESSFUL

The result indicates that the program is safe for an arbitrary number of threads (bound 2 on the number of dynamically created threads only applied to the generation of counterexamples). If the program is found to be unsafe, satabs returns VERIFICATION FAILED in conjunction with a counterexample.

Note: Satabs does currently not support the counterexample format of Bfc and uses the finite-state model checker BBoom for this purpose (an extension of the Boom model checker). The full integration of Bfc will be part of the upcoming Satabs release (version 4.0); check www.cprover.org/satabs for the latest news. The Monabs tool mentioned in [9] has been fully integrated with Satabs.

6. C Program Benchmarks and Experimental Results

Our experiments were performed using the CPROVER Benchmarking Toolkit. To repeat our experiments, download informcomput15.cprover.bm.tar.gz and proceed as described on the CPROVER Benchmarking Toolkit's web page. For reference, all our log files and detailed results are available online.

Earlier benchmark sets

The program benchmarks used in [1] are available here; the BSD/Solaris sources are The program benchmarks used in [7] are available here.

7. Sources

The Bfc source code (C++) is available via

svn co http://www.cprover.org/svn/software/bfc/

The repository contains the Visual Studio solution bfc.sln with three sub-projects: bfc, boom_wrap and ttstrans. To compile bfc under Linux run make. For more details read the COMPILE.txt and LICENSE.txt files. The tools use the boost library which has to be installed before compiling bfc. Pre-compiled library binaries for Visual Studio are available here. On most Linux distributions it is available via the standard package manager; version 1.49 is available is, e.g., part of Ubuntu 12.10. Under Windows two system environment variables need to be defined prior compilation: BOOST_PATH and BOOST_LIB_PATH.

Bug reporting

If you found a bug, please send an E-Mail to alexander.kaiser@cs.ox.ac.uk.

8. References

[1] Alexander Kaiser, Daniel Kroening, Thomas Wahl: Efficient Coverability Analysis by Proof Minimization. CONCUR 2012.

[2] G. Ciardo, Petri nets with marking-dependent arc cardinality: Properties and analysis., in: R. Valette (Ed.), Application and Theory of Petri Nets, Vol. 815 of Lecture Notes in Computer Science, Springer, 1994.

[3] https://github.com/pierreganty/mist

[4] http://petruchio.informatik.uni-oldenburg.de/

[5] http://www.ulb.ac.be/di/verif/ggeeraer/CSC.html

[6] http://homepages.laas.fr/bernard/tina

[7] Alexander Kaiser, Daniel Kroening, Thomas Wahl: Dynamic Cutoff Detection in Parameterized Concurrent Programs. CAV 2010.

[8] Alexander Kaiser, Daniel Kroening, Thomas Wahl: Wahl: Lost in Abstraction: Monotonicity in Multi-threaded Programs. CONCUR 2014.

[9] Alexander Kaiser, Daniel Kroening, Thomas Wahl: Lost in Abstraction: Monotonicity in Multi-threaded Programs. (Under submission)

This research was sponsored by the EPSRC grant 'Efficient Verification of Software with Replicated Components' (G026254).