Software Verification for Weak Memory

Objectives

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:

• 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.

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.

People

• Jade Alglave
• Daniel Kroening
• John Lugton
• Vincent Nimal
• Michael Tautschnig