Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings
Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings
复制标题
编程语言和系统 - 第 31 届欧洲编程研讨会，ESOP 2022，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2022，德国慕尼黑，2022 年 4 月 2-7 日，会议记录
DOI：
10.1007/978-3-030-99336-8_9
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Bila E
中科院分区：
文献类型：
--
作者：
Bila E
持久内存的兴起正在颠覆计算的核心。我们的工作旨在帮助程序员导航这个勇敢的新世界，通过提供一个程序逻辑推理x86代码，使用低级操作，如内存访问和围栏，以及持久化原语，如刷新。我们的逻辑，Pierogi，受益于一个简单的底层操作语义的基础上的意见，是能够处理优化的刷新操作，并在Isabelle/HOL证明助手机械化。我们详细介绍了Pierogi的证明规则，并证明了它们的声音。我们还展示了如何Pierogi可以用来推理一系列具有挑战性的单线程和多线程持久化程序。
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.