Conference item
Software verification for weak memory via program transformation
- Abstract:
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 499.7KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-642-37036-6_28
- Publisher:
- Springer
- Host title:
- Lecture Notes in Computer Science: ESOP 2013: Programming Languages and Systems
- Journal:
- Lecture Notes in Computer Science: ESOP 2013: Programming Languages and Systems More from this journal
- Volume:
- 7792
- Pages:
- 512-532
- Publication date:
- 2013-12-31
- DOI:
- ISSN:
-
0302-9743
- ISBN:
- 9783642370359
- Keywords:
- Pubs id:
-
pubs:576512
- UUID:
-
uuid:33ec5926-faaa-4759-aec8-ece0cfa0fee9
- Local pid:
-
pubs:576512
- Source identifiers:
-
576512
- Deposit date:
-
2017-01-28
Terms of use
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- 2013
- Notes:
- © Springer-Verlag Berlin Heidelberg 2013. This is the Accepted Manuscript version of the article. The final version is available online from Springer at: https://doi.org/10.1007/978-3-642-37036-6_28
If you are the owner of this record, you can report an update to it here: Report update to this record