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.
|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 tool and the Coq proofs|
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.