Decidable verification under causal consistency via potential-based semantics

Abstract

While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, until recently the decidability of safety verification for concurrent programs running under causally consistent shared memories has been unclear. We establish the decidability of this problem for two standard and well-studied variants of causal consistency. To do so, for each variant, we develop an equivalent “lossy” operational semantics, whose states track possible futures, rather than more standard semantics that record the history of the execution. We show that these semantics constitute well-structured transition systems, thus enabling decidable verification.

The talk is based on joint work with Udi Boker, published in PLDI’20 and TOPLAS’22.

Bio

Ori Lahav is a theoretical computer scientist whose main research is in programming languages and verification, focusing on concurrency and relaxed memory models. Ori is currently a professor at Tel Aviv University. Previously, he was a postdoctoral researcher at Max Planck Institute for Software Systems (MPI-SWS), and a PhD student in Tel Aviv University in the field of logic for computer science. He was the recipient of an ERC starting Grant in 2019 for a project titled “Verification-Aware Programming Language Concurrency Semantics”. His work received multiple distinguished and best paper awards in several top conferences such as PLDI, OOPSLA, and ECOOP.