View-Based Owicki–Gries Reasoning for Persistent x86-TSO
Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
Abstract
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.