Effective Program Verification for Relaxed Memory Models
Effective Program Verification for Relaxed Memory Models
复制标题
DOI：
10.1007/978-3-540-70545-1_12
复制
发表时间：
2008-07
期刊：
影响因子：
--
通讯作者：
S. Burckhardt;M. Musuvathi
中科院分区：
文献类型：
--
作者：
S. Burckhardt;M. Musuvathi
程序验证宽松的内存模型是困难的。这种模型的高度不确定性对标准验证技术提出了挑战。本文提出了一种新的验证技术，最常见的松弛，存储缓冲区。这种技术的关键是观察到所有程序员，包括那些使用低锁技术来提高性能的程序员，都希望他们的程序是顺序一致的。我们首先提出了一个监控算法，可以检测程序执行的存在，不顺序一致，由于存储缓冲区，而只是探索顺序一致的执行。然后，我们联合收割机将这个监视器与一个无状态的模型检查器结合起来，该检查器验证每个顺序一致的执行是正确的。我们已经实现了这个算法的原型工具，称为Sober和目前的实验，证明了我们的方法的精度和可扩展性。我们在几个程序中发现了宽松的内存模型错误，包括两个以前未知的生产级并发库中的错误，这些错误很难通过其他方式找到。
Program verification for relaxed memory models is hard. The high degree of nondeterminism in such models challenges standard verification techniques. This paper proposes a new verification technique for the most common relaxation, store buffers. Crucial to this technique is the observation that all programmers, including those who use low-lock techniques for performance, expect their programs to be sequentially consistent. We first present a monitor algorithm that can detect the presence of program executions that are not sequentially consistent due to store buffers whileonlyexploring sequentially consistent executions. Then, we combine this monitor with a stateless model checker that verifies that every sequentially consistent execution is correct. We have implemented this algorithm in a prototype tool called Sober and present experiments that demonstrate the precision and scalability of our method. We find relaxed memory model bugs in several programs, including two previously unknown bugs in a production-level concurrency library that would have been difficult to find by other means.