Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Wed 17 Jun 2020 11:20 - 11:40 at PLDI Research Papers live stream - Verification I Chair(s): Stephen N. Freund

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 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

10:40 - 11:00
Verifying Concurrent Search Structure Templates
PLDI Research Papers
Siddharth KrishnaMicrosoft Research, Cambridge, Nisarg PatelNew York University, USA, Dennis ShashaNew York University, USA, Thomas WiesNew York University, USA
11:00 - 11:20
Armada: Low-Effort Verification of High-Performance Concurrent Programs
PLDI Research Papers
Jacob R. LorchMicrosoft Research, USA, Yixuan ChenUniversity of Michigan, USA / Yale University, USA, Manos KapritsosUniversity of Michigan, USA, Bryan ParnoCarnegie Mellon University, USA, Shaz QadeerNovi, USA, Upamanyu SharmaUniversity of Michigan, USA, James R. WilcoxCertora, USA, Xueyuan ZhaoCarnegie Mellon University, USA
11:20 - 11:40
Decidable Verification under a Causally Consistent Shared Memory
PLDI Research Papers
Ori LahavTel Aviv University, Israel, Udi BokerIDC Herzliya, Israel
11:40 - 12:00
Inductive Sequentialization of Asynchronous Programs
PLDI Research Papers
Bernhard KraglIST Austria, Constantin EneaUniversity of Paris Diderot, France, Thomas A. HenzingerIST Austria, Austria, Suha Orhun MutluergilIRIF, France / University of Paris, France / CNRS, France, Shaz QadeerNovi, USA