|
|
Paper
S. Burckhardt, R. Alur, M. Martin.
CheckFence: Checking Consistency of Concurrent Data Types
on Relaxed Memory Models.
Programming Language Design and Implementation (PLDI 2007).
Download
- Full text, as acrobat
pdf or postscript
ps
- Presentation,
acrobat
pdf, powerpoint
ppt,
or openoffice sxi
Abstract
Concurrency libraries can facilitate the development of
multi-threaded
programs by providing concurrent implementations of familiar data
types such as queues or sets. There exist many optimized algorithms
that can achieve superior performance on multiprocessors by allowing
concurrent data accesses without using locks. Unfortunately, such
algorithms can harbor subtle concurrency bugs. Moreover, they require
memory ordering fences to function correctly on relaxed memory models.
To address these difficulties, we propose a verification approach that
can exhaustively check all concurrent executions of a given test
program on a relaxed memory model and can verify that they are
observationally equivalent to a sequential execution. Our
CheckFence prototype automatically translates
the C
implementation code and the test program into a SAT formula, hands the
latter to a standard SAT solver, and constructs counterexample traces
if there exist incorrect executions. Applying CheckFence
to
five previously published algorithms, we were able to (1) find several
bugs (some not previously known), and (2) determine how to place
memory ordering fences for relaxed memory models.
Citation
@inproceedings{burckhardt-alur-martin-PLDI07,
author = {S. Burckhardt and R. Alur and M. Martin},
title = {{CheckFence}: Checking Consistency of Concurrent Data Types on Relaxed Memory Models},
booktitle = {Programming Language Design and Implementation (PLDI)},
pages = {12--21},
year = {2007},
}
|
