Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-33386-6_21 | ATVA |
Keywords | Field | DocType |
parallel assertion,sequentially consistent semantics,weak memory model,debugging tool,powerful tool,previous semantics,new formal semantics,parallel program,new semantics,formal semantics | Programming language,Sequential consistency,Parsec,Concurrency,Computer science,Correctness,Assertion,Theoretical computer science,Probe effect,Semantics,Debugging | Conference |
Citations | PageRank | References |
0 | 0.34 | 12 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Daniel Schwartz-Narbonne | 1 | 20 | 4.24 |
Georg Weissenbacher | 2 | 271 | 22.71 |
Sharad Malik | 3 | 7766 | 691.24 |