Software Verification for Weak Memory


Modern multi-core microprocessors implement weak memory consistency models; prog­ramming for these architectures is a challenge. We want to adapt and use existing static analysis techniques to verify programs with respect to weak memory consistency, guided by the following objectives:

April 4th 2014A fixed version of musketeer is now available
Dec 4th 2013Release of musketeer
Oct 5th 2012New sound, optimised strategy for instrumenting critical cycles implemented in Goto-instrument
Jul 4th 2012We now analyse Apache's fdqueue module
Jun 24th 2012Concurrent CBMC added to the set of model checkers used for the experiments
Feb 22nd 2012We report distinct results for Poirot with integer vs. bitvector arithmetic
Feb 8th 2012SatAbs is now able to handle RCU!
Jan 23rd 2012Release of the instrumentation tool and the Coq proofs

Don't Sit on the Fence: A static analysis approach to automatic fence insertion

Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency between threads. As both the semantics of the program under these architectures and the semantics of these fences may be subtle, the automation of their placement is highly desirable. However, precise methods to restore strong consistency do not scale to the size of deployed systems code. We choose to trade some precision for genuine scalability: we present a novel technique suitable for interprocedural analysis of large code bases. We implement this method in our new musketeer tool, and detail experiments on more than 350 executables of packages found in a Debian Linux distribution, e.g. memcached (about 10000 LoC).

``En garde !''

              / |
              / |

CAV 2013: Partial Orders for Efficient Bounded Model Checking of Concurrent Software

The number of interleavings of a concurrent program makes automatic analysis of such software very hard. Modern multiprocessors' execution models make this problem even harder. Modelling program executions with partial orders rather than interleavings addresses both issues: we obtain an efficient encoding into integer difference logic for bounded model checking that enables first-time formal verification of deployed concurrent systems code. We implemented the encoding in the CBMC tool and present experiments over a wide range of memory models, including SC, Intel x86 and IBM Power. Our experiments include core parts of PostgreSQL, the Linux kernel and the Apache HTTP server.


ESOP 2013: Software Verification for Weak Memory via Program Transformation

In this paper, we propose a sound transformation of the program to verify, enabling SC tools to perform verification w.r.t. weak memory. We present experiments for a broad variety of models (from x86-TSO to Power) and a vast range of verification tools, quantify the additional cost of the transformation and highlight the cases when we can drastically reduce it. Our benchmarks include work-queue management code from PostgreSQL.


APLAS 2011: Soundness of Data-flow Analysis for Weak Memory Models

In this paper, we identify the data-flow analyses which are sound for weak memory models as is: the analyses based on non-relational domains. We also provide a non-trivial method for fixing analyses sound under sequential consistency but unsound for weaker consistency.


We are releasing binaries for x86 Linux, the source code and the papers proofs.

CProver & Goto-instrument (ESOP'13)

Download binaries, source code, installation instructions and manual.

Source code is also available via
svn co

Abstract machine proofs (ESOP'13)

Proof formalised in Coq.

Soundness condition proof (APLAS'11)

Proof formalised in Coq.