Parameterized verification of transactional memories
Parameterized verification of transactional memories
复制标题
事务存储器的参数化验证
DOI：
10.1145/1806596.1806613
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
R. Manevich
中科院分区：
文献类型：
--
作者：
M. Emmi;R. Majumdar;R. Manevich
我们描述了一个自动验证方法来检查是否事务存储器确保严格的串行化的一个关键属性假设的事务接口。我们的主要贡献是有效地验证参数化系统的技术。该技术融合了来自参数化硬件和协议验证的想法-通过不可见的不变量和对称性简化进行验证-与来自软件验证的想法-基于模板的不变式生成和量化公式（模理论）的可满足性检查。这种结合使我们能够精确地建模和分析无界系统，同时驯服状态爆炸。
我们的技术可以自动证明两阶段锁定（TPL），动态软件事务内存（DSTM）和事务锁定II（TL 2）系统确保严格的可串行化。验证是具有挑战性的，因为系统在几个维度上是无界的：并发执行事务的数量和长度，以及它们访问的共享内存的大小，没有有限的限制。相比之下，国家的最先进的软件模型检查工具，如BLAST和TVLA是无法验证任何一个系统，由于固有的表现力的限制或状态爆炸。
We describe an automatic verification method to check whether transactional memories ensure strict serializability a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized systems. The technique merges ideas from parameterized hardware and protocol verification--verification by invisible invariants and symmetry reduction--with ideas from software verification--template-based invariant generation and satisfiability checking for quantified formulæ (modulo theories). The combination enables us to precisely model and analyze unbounded systems while taming state explosion.
Our technique enables automated proofs that two-phase locking (TPL), dynamic software transactional memory (DSTM), and transactional locking II (TL2) systems ensure strict serializability. The verification is challenging since the systems are unbounded in several dimensions: the number and length of concurrently executing transactions, and the size of the shared memory they access, have no finite limit. In contrast, state-of-the-art software model checking tools such as BLAST and TVLA are unable to validate either system, due to inherent expressiveness limitations or state explosion.