Decidable Verification under a Causally Consistent Shared Memory
Causal consistency is one of the most fundamental and widely used consistency models weaker than sequential consistency. In this paper, we study the verification of safety properties for finite-state concurrent programs running under a causally consistent shared memory model. We establish the decidability of this problem for a standard model of causal consistency (called also "Causal Convergence" and "Strong-Release-Acquire"). Our proof proceeds by developing an alternative operational semantics, based on the notion of a thread potential, that is equivalent to the existing declarative semantics and constitutes a well-structured transition system. In particular, our result allows for the verification of a large family of programs in the Release/Acquire fragment of C/C++11 (RA). Indeed, while verification under RA was recently shown to be undecidable for general programs, since RA coincides with the model we study here for write/write-race-free programs, the decidability of verification under RA for this widely used class of programs follows from our result. The novel operational semantics may also be of independent use in the investigation of weakly consistent shared memory models and their verification.
Wed 17 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00 | Verification I PLDI Research Papers at PLDI Research Papers live stream Chair(s): Stephen N. Freund Williams College | ||
10:40 20mTalk | Verifying Concurrent Search Structure Templates PLDI Research Papers Siddharth Krishna Microsoft Research, Cambridge, Nisarg Patel New York University, USA, Dennis Shasha New York University, USA, Thomas Wies New York University, USA | ||
11:00 20mTalk | Armada: Low-Effort Verification of High-Performance Concurrent Programs PLDI Research Papers Jacob R. Lorch Microsoft Research, USA, Yixuan Chen University of Michigan, USA / Yale University, USA, Manos Kapritsos University of Michigan, USA, Bryan Parno Carnegie Mellon University, USA, Shaz Qadeer Novi, USA, Upamanyu Sharma University of Michigan, USA, James R. Wilcox Certora, USA, Xueyuan Zhao Carnegie Mellon University, USA DOI | ||
11:20 20mTalk | Decidable Verification under a Causally Consistent Shared Memory PLDI Research Papers | ||
11:40 20mTalk | Inductive Sequentialization of Asynchronous Programs PLDI Research Papers Bernhard Kragl IST Austria, Constantin Enea University of Paris Diderot, France, Thomas A. Henzinger IST Austria, Austria, Suha Orhun Mutluergil IRIF, France / University of Paris, France / CNRS, France, Shaz Qadeer Novi, USA |