- Daniel Kroening
- Boolean Programs
- SMT Lists/Sets/Maps
- Google groups:
- SMT 2010
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
- Download
- Input language
- Command line interface
- Proving the parameterized ticket algorithm
- Model Checking for Multi-Threaded ANSI-C Programs using Satabs
- C Program Benchmarks and Experimental Results
- Sources
- References
1. Download
We currently distribute binaries for 32-bit Windows and 64-bit Linux.
The archives contain the executables 2. Input LanguageThe tool
Example
The following program
induces the following MDRP (intermediate states of atomic sections are omitted, character # starts a comment)
4 3
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 interfaceFor instructions on how to use Bfc, run the tool as follows:
The parameterized initial state is To check coverability of, e.g., the state ( bfc --target "0|2,2" ./example.mdrp
This will produce the output
Hence, state ( 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:
The error state
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 5. Model Checking for Multi-Threaded ANSI-C Programs using SatabsPrior 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
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:
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, 6. C Program Benchmarks and Experimental ResultsOur 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 setsThe program benchmarks used in [1] are available here; the BSD/Solaris sources are
7. SourcesThe Bfc source code (C++) is available via
The repository contains the Visual Studio solution Bug reportingIf 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). |