Duet (forked from https://github.com/zkincaid/duet)
Duet is a static analysis tool designed for analyzing concurrent programs.
Duet depends on several software packages. The following dependencies need to be installed manually.
- opam (version >= 2, with OCaml >= 4.08 & native compiler)
- If you have an older version of opam installed, you can install opam2 using
opam install opam-devel
- If you have an older version of opam installed, you can install opam2 using
- GMP and MPFR
- NTL: number theory library
- Java
- Python
On Ubuntu, you can install these packages with:
sudo apt-get install opam libgmp-dev libmpfr-dev libntl-dev default-jre python
On MacOS, you can install these packages (except Java) with:
brew install opam gmp mpfr ntl python
Next, add the sv-opam OPAM repository, and install the rest of duet's dependencies. These are built from source, so grab a coffee — this may take a long time.
opam remote add sv git://github.com/zkincaid/sv-opam.git#modern
opam install ocamlgraph batteries ppx_deriving z3 apron ounit menhir cil OCRS ntl
After Duet's dependencies are installed, it can be built as follows:
./configure
make
Duet's makefile has the following targets:
make
: Build duetmake srk
: Build the ark library and test suitemake apak
: Build the apak library and test suitemake doc
: Build documentationmake test
: Run test suite
There are three main program analyses implemented in Duet:
- Data flow graphs:
duet.native -coarsen FILE
- Proof spaces:
duet.native -proofspace FILE
- Compositional recurrence analysis:
duet.native -cra FILE
Duet supports two file types (and guesses which to use by file extension): C programs (.c), Boolean programs (.bp).
By default, Duet checks user-defined assertions, which are specified by the built-in function __VERIFIER_assert
. Alternatively, it can also instrument assertions as follows:
duet.native -check-array-bounds -check-null-deref -coarsen FILE
The -coarsen
flag implements an invariant generation procedure for multi-threaded programs with an unbounded number of threads. The analysis is described in
- Azadeh Farzan and Zachary Kincaid: Verification of Parameterized Concurrent Programs By Modular Reasoning about Data and Control. POPL 2012.
The -proofspace
flag implements a software model checking procedure for multi-threaded programs with an unbounded number of threads. The procedure is described in
- Azadeh Farzan, Zachary Kincaid, Andreas Podelski: Proof Spaces for Unbounded Parallelism. POPL 2015.
The -cra
flags an invariant generation procedure for sequential programs. The analysis is described in
- Azadeh Farzan and Zachary Kincaid: Compositional Recurrence Analysis. FMCAD 2015.
- Zachary Kincaid, John Cyphert, Jason Breck, Thomas Reps: Non-Linear Reasoning For Invariant Synthesis. POPL 2018.
Typically, it is best to run CRA with -cra-split-loops
. By default, the -cra
runs the analysis as described in POPL'18. The FMCAD'15 analysis can be run by setting the -cra-no-matrix
flag.
The interprocedural variant is described in
- Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, Thomas Reps: Compositional Recurrence Analysis Revisited. PLDI 2017.
is available in the Newton-ark2 branch of this repository. Build instructions to come.
Duet is split into several packages:
-
srk
Symbolic reasoning kit. This is a high-level interface over Z3 and Apron. Most of the work of compositional recurrence analysis lives in srk.
-
pa
Predicate automata library.
-
duet
Implements program analyses, frontends, and anything programming-language specific.