Software Verification for Weak Memory via Program Transformation

TL;DR

This paper introduces a sound program transformation technique that allows existing sequential consistency verification tools to effectively verify programs under weak memory models, broadening verification capabilities.

Contribution

The authors propose a novel program transformation method that enables verification of weak memory models using existing SC tools, with demonstrated effectiveness across various architectures.

Findings

Transformation is sound and applicable to multiple architectures

Verification cost can be significantly reduced in certain cases

Benchmarks include real-world PostgreSQL code

Abstract

Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. 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/ARM) 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.