View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2022(2022)
摘要
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.
更多查看译文
关键词
Persistent memory, x86-TSO, Owicki-Gries, Isabelle/HOL, verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要