Software Verification for Weak Memory Via Program Transformation
Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. The authors propose a sound transformation of the program to verify, enabling SC tools to perform verification w.r.t. weak memory. They 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 they can drastically reduce it. Their benchmarks include work-queue management code from PostgreSQL.