Software Verification for Weak Memory

Objectives

Modern multi-core microprocessors implement weak memory consistency models; programming 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:

Identifying the existing automated techniques which already handle weak memory verification;
Adapting and fixing techniques which are not sound for this class of problems;
Providing automated tools which offer concrete information and help to developers for software engineering with weak memory.

News

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

Download

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