TY - GEN
T1 - Parallel assertions for architectures with weak memory models
AU - Schwartz-Narbonne, Daniel
AU - Weissenbacher, Georg
AU - Malik, Sharad
PY - 2012
Y1 - 2012
N2 - Assertions are a powerful and widely used debugging tool in sequential programs, but are ineffective at detecting concurrency bugs. We recently introduced parallel assertions which solve this problem by providing programmers with a simple and powerful tool to find bugs in parallel programs. However, while modern computer hardware implements weak memory models, the sequentially consistent semantics of parallel assertions prevents these assertions from detecting some feasible bugs. We present a formal semantics for parallel assertions that accounts for the effects of weak memory models. This new formal semantics allows us to prove the correctness of two key optimizations which significantly increase the speed of a runtime assertion checker on a set of PARSEC benchmarks. We discuss the probe effect caused by checking these assertions at runtime, and show how our new semantics allows the detection of bugs that were undetectable in the previous semantics.
AB - Assertions are a powerful and widely used debugging tool in sequential programs, but are ineffective at detecting concurrency bugs. We recently introduced parallel assertions which solve this problem by providing programmers with a simple and powerful tool to find bugs in parallel programs. However, while modern computer hardware implements weak memory models, the sequentially consistent semantics of parallel assertions prevents these assertions from detecting some feasible bugs. We present a formal semantics for parallel assertions that accounts for the effects of weak memory models. This new formal semantics allows us to prove the correctness of two key optimizations which significantly increase the speed of a runtime assertion checker on a set of PARSEC benchmarks. We discuss the probe effect caused by checking these assertions at runtime, and show how our new semantics allows the detection of bugs that were undetectable in the previous semantics.
UR - http://www.scopus.com/inward/record.url?scp=84868218058&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84868218058&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-33386-6_21
DO - 10.1007/978-3-642-33386-6_21
M3 - Conference contribution
AN - SCOPUS:84868218058
SN - 9783642333859
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 254
EP - 268
BT - Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Proceedings
T2 - 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
Y2 - 3 October 2012 through 6 October 2012
ER -