|
|
Paper
S. Burckhardt, M. Musuvathi.
Effective Program Verification for Relaxed Memory Models.
Computer-Aided Verification (CAV 2008).
Download
- Regular paper, as acrobat
pdf
- MSR Tech Report, (contains more proofs) as acrobat
pdf
- Presentation at CAV,
powerpoint
pptx
- Presentation at ETH Zurich,
powerpoint
pptx
Abstract
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.
Citation
@inproceedings{burckhardt-musuvathi-CAV08,
author = {S. Burckhardt and M. Musuvathi},
title = {Effective Program Verification for Relaxed Memory Models},
booktitle = {Computer-Aided Verification (CAV)},
pages = {107--120},
year = {2008},
}
|
