Name
Abstract | ||
|---|---|---|
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fences, as well as persistency primitives such as flushes. Our logic, Pierogi, benefits from a simple underlying operational semantics based on views, is able to handle optimised flush operations, and is mechanised in the Isabelle/HOL proof assistant. We detail the proof rules of Pierogi and prove them sound. We also show how Pierogi can be used to reason about a range of challenging single- and multi-threaded persistent programs. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/978-3-030-99336-8_9 | PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2022 |
Keywords | DocType | Volume |
Persistent memory, x86-TSO, Owicki-Gries, Isabelle/HOL, verification | Conference | 13240 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eleni Vafeiadi Bila | 1 | 0 | 0.34 |
| Brijesh Dongol | 2 | 0 | 0.68 |
| Ori Lahav | 3 | 0 | 1.01 |
| Azalea Raad | 4 | 0 | 1.01 |
| John Wickerson | 5 | 142 | 10.08 |