View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)

TL;DR

This paper introduces Pierogi, a program logic for reasoning about persistent x86 code with low-level operations and fences, supported by a view-based semantics and mechanized in Isabelle/HOL.

Contribution

It presents a novel view-based logic, Pierogi, for reasoning about persistent memory operations on x86, including optimizations and formal soundness proofs.

Findings

Pierogi can reason about complex persistent programs.

The logic handles optimized flush operations.

Pierogi is mechanized and proven sound in Isabelle/HOL.

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.