SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 11:05 - 11:20 at Zurich F - PLDI 2020 Papers 1 Chair(s): Luís Pina

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.

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
PLDI 2020 Papers 1SIGPLAN Papers at Zurich F
Chair(s): Luís Pina University of Illinois at Chicago
10:50
15m
Talk
Armada: Low-Effort Verification of High-Performance Concurrent Programs
SIGPLAN Papers
Jacob R. Lorch Microsoft Research, n.n., Yixuan Chen 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 University of Washington, Xueyuan Zhao Carnegie Mellon University, USA
DOI
11:05
15m
Talk
Decidable Verification under a Causally Consistent Shared Memory
SIGPLAN Papers
Ori Lahav Tel Aviv University, Udi Boker IDC Herzliya, Israel
11:20
15m
Talk
Efficient Handling of String-Number Conversion
SIGPLAN Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Julian Dolby IBM Research, USA, Petr Janků Brno University of Technology, Czechia, Hsin-Hung Lin Academia Sinica, Taiwan, Lukáš Holík Brno University of Technology, Wei-Cheng Wu University of Southern California, USA
11:35
15m
Talk
Verifying Concurrent Search Structure Templates
SIGPLAN Papers
Siddharth Krishna Microsoft Research, Nisarg Patel New York University, Dennis Shasha New York University, Thomas Wies New York University
11:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers