Advertisement
Published in:
2013 | OriginalPaper | Chapter
Software Verification for Weak Memory via Program Transformation
Authors : Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Multiprocessors implement weak memory models, but program verifiers often assume
Sequential Consistency
(SC), and 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) 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.