Parallel assertions for architectures with weak memory models

Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Proceedings
Number of pages15
StatePublished - 2012
Event10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India
Duration: Oct 3 2012Oct 6 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7561 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Parallel assertions for architectures with weak memory models'. Together they form a unique fingerprint.

Cite this