Effective program verification for relaxed memory models. (English) Zbl 1155.68428

Gupta, Aarti (ed.) et al., Computer aided verification. 20th international conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70543-7/pbk). Lecture Notes in Computer Science 5123, 107-120 (2008).
Summary: 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 while only exploring 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.
For the entire collection see [Zbl 1139.68005].


68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)


Checkfence; veriSoft
Full Text: DOI