Software Verification for Weak Memory via Program Transformation
This addresses verification gaps for concurrent software on multiprocessors with weak memory models, offering a practical solution for developers and verification engineers.
The authors tackled the problem of software verification for weak memory models by proposing a sound program transformation that enables existing Sequential Consistency verification tools to handle weak memory models, demonstrating effectiveness across various architectures (x86/TSO to Power/ARM) and tools while quantifying transformation costs.
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.