Software verification for weak memory via program transformation. (English) Zbl 1381.68143

Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-37035-9/pbk). Lecture Notes in Computer Science 7792, 512-532 (2013).
Summary: 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 with respect to 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.
For the entire collection see [Zbl 1268.68016].


68Q60 Specification and verification (program logics, model checking, etc.)
68M07 Mathematical problems of computer architecture
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Full Text: DOI arXiv