View-Based Owicki-Gries Reasoning for Persistent x86-TSO


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, fences, and flushes. Our logic, called 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. In this paper, 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 programs.