Portal de Periódicos da CAPES

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

2022; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-99336-8_9

1611-3349

Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson,

Logic, programming, and type systems

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.