Software verification for weak memory via program transformation
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 fo...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2013
|
| _version_ | 1797062043623227392 |
|---|---|
| author | Alglave, J Kroening, D Nimal, V Tautschnig, M |
| author2 | Felleisen, M |
| author_facet | Felleisen, M Alglave, J Kroening, D Nimal, V Tautschnig, M |
| author_sort | Alglave, J |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T20:39:54Z |
| format | Conference item |
| id | oxford-uuid:33ec5926-faaa-4759-aec8-ece0cfa0fee9 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:39:54Z |
| publishDate | 2013 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:33ec5926-faaa-4759-aec8-ece0cfa0fee92022-03-26T13:22:56ZSoftware verification for weak memory via program transformationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:33ec5926-faaa-4759-aec8-ece0cfa0fee9Symplectic Elements at OxfordSpringer2013Alglave, JKroening, DNimal, VTautschnig, MFelleisen, MGardner, PMultiprocessors 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. |
| spellingShingle | Alglave, J Kroening, D Nimal, V Tautschnig, M Software verification for weak memory via program transformation |
| title | Software verification for weak memory via program transformation |
| title_full | Software verification for weak memory via program transformation |
| title_fullStr | Software verification for weak memory via program transformation |
| title_full_unstemmed | Software verification for weak memory via program transformation |
| title_short | Software verification for weak memory via program transformation |
| title_sort | software verification for weak memory via program transformation |
| work_keys_str_mv | AT alglavej softwareverificationforweakmemoryviaprogramtransformation AT kroeningd softwareverificationforweakmemoryviaprogramtransformation AT nimalv softwareverificationforweakmemoryviaprogramtransformation AT tautschnigm softwareverificationforweakmemoryviaprogramtransformation |