Duet: static analysis for unbounded concurrency

About

Duet¹ is a static analysis tool designed for analyzing concurrent programs, where the number of threads cannot be statically bounded. It accomplishes this task by decomposing the analysis problem into two components – one that analyzes data, and one that analyzes control. These two components interact with eachother to compute a sound overapproximation of the dynamic behaviours of a program.

People

Azadeh Farzan

Zachary Kincaid

Download

An x86_64 Debian package for Duet is available here. If you have trouble installing this package, please contact Zak.

Duet is available on github.

Using Duet

The most common mode of operation (which runs the analysis from [FK12]) is as follows:

duet -parameterized -coarsen FILE

Duet supports three file types (and guesses which to use by file extension): C programs (.c), Boolean programs (.bp), and Goto programs (.goto) (not included in this release).
By default, Duet checks user-defined assertions. Alternatively, it can also instrument assertions as follows:

duet -check-array-bounds -check-null-deref -parameterized -coarsen FILE

Experiments

The experiments for [FK12] are divided into three groups:

Publications

[FK13]	Azadeh Farzan and Zachary Kincaid. Duet: static analysis for unbounded parallelism. CAV, 2013. [ abstract \| bib ]
[FK12]	Azadeh Farzan and Zachary Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. POPL, pages 297-308, 2012. [ abstract \| bib ]
[FK10]	Azadeh Farzan and Zachary Kincaid. Compositional bitvector analysis for concurrent programs with nested locks. In SAS, pages 253-270, 2010. [ abstract \| bib ]

Related work

Tools for model checking parameterized Boolean programs

Boom (implements dynamic cutoff detection)
Getafix (implements linear interfaces)

Footnotes:

¹ This work is partially supported by a National Science and Engineering Research Council (NSERC) Discovery Grant