@InProceedings{pierogi,
author="Bila, Eleni Vafeiadi
and Dongol, Brijesh
and Lahav, Ori
and Raad, Azalea
and Wickerson, John",
editor="Sergey, Ilya",
title="View-Based Owicki--Gries Reasoning for Persistent x86-TSO",
booktitle="Programming Languages and Systems",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="234--261",
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.",
isbn="978-3-030-99336-8"
}