Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-37036-6_28 | european symposium on programming |
Keywords | DocType | Volume |
weak memory,present experiment,sc tool,broad variety,additional cost,weak memory model,software verification,program transformation,verification tool,sequential consistency,verification w,sound transformation | Conference | abs/1207.7264 |
ISSN | Citations | PageRank |
0302-9743 | 51 | 1.32 |
References | Authors | |
36 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jade Alglave | 1 | 608 | 26.53 |
| Daniel Kroening | 2 | 3084 | 187.60 |
| Vincent Nimal | 3 | 75 | 2.51 |
| Michael Tautschnig | 4 | 425 | 25.84 |