A Proposal for Weak-Memory Local Reasoning
A Proposal for Weak-Memory Local Reasoning
复制标题
弱内存局部推理的提案
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Josh Berdine
中科院分区：
文献类型：
--
作者：
Ian Wehrman;Josh Berdine
程序逻辑是用于对软件程序进行说明和推理的形式化系统。大多数程序逻辑都假设所有线程在任何时候都对共享内存的值保持一致。这个假设对于有竞争的程序来说可能是不合理的，就像许多并发数据结构一样。这些困难的程序的验证必须考虑到它们执行的架构所提供的较弱的内存模型。在本文中，我们描述了一个程序逻辑的进展，本地推理racy并发程序执行弱，x86-like内存模型。
Program logics are formal systems for specifying and reasoning about software programs. Most program logics make the strong assumption that all threads agree on the value of shared memory at all times. This assumption can be unsound though for programs with races, like many concurrent data structures. Verification of these difficult programs must take into account the weaker models of memory provided by the architectures on which they execute. In this paper, we describe progress toward a program logic for local reasoning about racy concurrent programs executing on a weak, x86-like memory model.