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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Intel 64 and IA-32 architectures software developer’s manual (March 2012)
Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models (extended version). Formal Methods in System Design 40(2) (2012)
Anderson, Z., Gay, D., Ennals, R., Brewer, E.: SharC: checking data sharing strategies for multithreaded C. In: PLDI. ACM (2008)
Boehm, H.-J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI. ACM (2008)
Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. In: ISSTA. ACM (2011)
Chong, N., Ishtiaq, S.: Reasoning about the ARM weakly consistent memory model. In: MSPC. ACM (2008)
International Standard 14882 (Programming Languages) C++, Final Committee Draft N3092 (March 2010), ISO/IEC
Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings (preliminary version). SIGARCH Comput. Archit. News 36(5) (2009)
Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Code Generation and Optimization. IEEE (2004)
Liu, F., Nedev, N., Prisadnikov, N., Vechev, M., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI. ACM (2012)
Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ASPLOS. ACM (2008)
Schwartz-Narbonne, D., Liu, F., August, D., Malik, S.: passert: A Tool for Debugging Parallel Programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 751–757. Springer, Heidelberg (2012)
Schwartz-Narbonne, D., Liu, F., Pondicherry, T., August, D.I., Malik, S.: Parallel assertions for debugging parallel programs. In: MEMOCODE. IEEE (2011)
Sen, K., Rosu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: ESEC/FSE. ACM (2003)
Vechev, M., Yahav, E., Yorsh, G.: Phalanx: parallel checking of expressive heap assertions. In: ISMM. ACM (2010)
Xu, M., Bodik, R., Hill, M.D.: A hardware memory race recorder for deterministic replay. IEEE Micro 27(1) (2007)
Yu, J., Narayanasamy, S.: A case for an interleaving constrained shared-memory multi-processor. In: ISCA. ACM (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schwartz-Narbonne, D., Weissenbacher, G., Malik, S. (2012). Parallel Assertions for Architectures with Weak Memory Models. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-33386-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33385-9
Online ISBN: 978-3-642-33386-6
eBook Packages: Computer ScienceComputer Science (R0)