Mechanized proofs of opacity: a comparison of two techniques
Mechanized proofs of opacity: a comparison of two techniques
复制标题
DOI：
10.1007/s00165-017-0433-3
复制
发表时间：
2018-09-01
影响因子：
1
通讯作者：
Wehrheim, Heike
中科院分区：
文献类型：
--
作者：
Derrick, John;Doherty, Simon;Wehrheim, Heike
软件事务存储器(STM)为程序员提供了用于并行进程同步的高级编程抽象，允许以交错方式执行的代码块被视为原子块。这种原子性属性被称为不透明度的正确性标准捕获，该标准将STM实现的行为与顺序原子规范的行为联系起来。在本文中，我们证明了最近提出的一种STM实现的不透明性：Dalessandro等人提出的事务互斥锁(TML)。为此，我们使用了两种不同的方法：第一种方法直接将TML的所有历史显示为不透明的(通过归纳证明)，使用TML的线性化证明作为辅助；第二种方法将TML显示为对已有的称为TM 2的中间规范的精化，该中间规范是已知的不透明的(通过模拟证明)。这两种证明都是在互动的证明者中进行的，第一次是使用KIV，第二次是使用Isabelle和KIV。这不仅允许比较原则上的证明技术，而且允许比较它们在机械化方面的复杂性。结果表明，第二种方法已经利用了TM 2的现有不透明性证明，允许证明以线性化证明不同的方式被分解为两个独立的证明。
Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as atomic blocks. This atomicity property is captured by a correctness criterion called opacity, which relates the behaviour of an STM implementation to those of a sequential atomic specification. In this paper, we prove opacity of a recently proposed STM implementation: the Transactional Mutex Lock (TML) by Dalessandro et al. For this, we employ two different methods: the first method directly shows all histories of TML to be opaque (proof by induction), using a linearizability proof of TML as an assistance; the second method shows TML to be a refinement of an existing intermediate specification called TMS2 which is known to be opaque (proof by simulation). Both proofs are carried out within interactive provers, the first with KIV and the second with both Isabelle and KIV. This allows to compare not only the proof techniques in principle, but also their complexity in mechanization. It turns out that the second method, already leveraging an existing proof of opacity of TMS2, allows the proof to be decomposed into two independent proofs in the way that the linearizability proof does not.