Software Verification for Weak Memory
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.
|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|
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 !'' \ ~__ |) /|_____ / | /| / |
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.
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.
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.