Towards formally specifying and verifying transactional memory
Towards formally specifying and verifying transactional memory
复制标题
DOI：
10.1007/s00165-012-0225-8
复制
发表时间：
2013-09-01
影响因子：
1
通讯作者：
Moir, Mark
中科院分区：
文献类型：
--
作者：
Doherty, Simon;Groves, Lindsay;Moir, Mark
在过去的十年中，在开发实用交易记忆（TM）实现方面取得了巨大进展，但是精确地指定对他们正确或正式证明他们是正确的意义的关注很少。在本文中，我们介绍TMS1（交易内存规范1），这是TM运行时库正确行为的精确规范。 TMS1的目标是用于在不受管理的编程语言（例如C ++）中实现交易功能的TM Runtimes。在这种情况下，即使最终中止的交易也必须观察到一致的记忆状态。否则，即使在正确的程序中，如果在原子上执行事务，则可能发生错误的程序，即使在正确的程序中，也可能发生错误的错误。我们使用I/O自动机（IOA）精确地指定TMS1。这种方法使我们还可以使用IOAS建模TM实现，并使用良好的证明技术和工具为其构建正式和机器检查的正确性证明。我们概述了TM系统的关键要求。为了避免排除满足这些要求的任何实施，我们指定TMS1尽可能笼统地与这些要求一致。这种普遍性的成本在于，该条件并未与关于通用TM实施技术的直觉映射，因此很难证明这种实现能够满足该条件。为了解决这一问题，我们提出了TMS2，这是一种更加限制的条件，更紧密地反映了有关常见TM实施技术的直觉。我们提供了一个模拟证明TMS2实现TMS1的证明，因此表明证明实现满足TMS1，这足以证明其满足TMS2。我们已经使用PVS规范和验证系统对此证明进行了正式验证。
Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving that they are. In this paper, we present TMS1 (Transactional Memory Specification 1), a precise specification of correct behaviour of a TM runtime library. TMS1 targets TM runtimes used to implement transactional features in an unmanaged programming language such as C or C++. In such contexts, even transactions that ultimately abort must observe consistent states of memory; otherwise, unrecoverable errors such as divide-by-zero may occur before a transaction aborts, even in a correct program in which the error would not be possible if transactions were executed atomically. We specify TMS1 precisely using an I/O automaton (IOA). This approach enables us to also model TM implementations using IOAs and to construct fully formal and machine-checked correctness proofs for them using well established proof techniques and tools. We outline key requirements for a TM system. To avoid precluding any implementation that satisfies these requirements, we specify TMS1 to be as general as we can, consistent with these requirements. The cost of such generality is that the condition does not map closely to intuition about common TM implementation techniques, and thus it is difficult to prove that such implementations satisfy the condition. To address this concern, we present TMS2, a more restrictive condition that more closely reflects intuition about common TM implementation techniques. We present a simulation proof that TMS2 implements TMS1, thus showing that to prove that an implementation satisfies TMS1, it suffices to prove that it satisfies TMS2. We have formalised and verified this proof using the PVS specification and verification system.