LFCS Seminar: 20 July 2022- Ori Lahav
Title: What's Decidable about Causally Consistent Shared Memory?
Abstract
While causal consistency is one of the most fundamental consistency
models weaker than sequential consistency, the decidability of
safety verification for (finite-state) concurrent programs running
under causally consistent shared-memories is still unclear. We
establish the decidability of this problem for two standard and
well-studied variants of causal consistency. To do so, for each of the
variants, we develop an equivalent "lossy" operational semantics,
and show that it constitutes a well-structured transition system,
which enables decidable verification. The two novel semantics are
based on similar key observations, which, we believe, may also be of
independent use in the investigation of weakly consistent shared
memory models and their verification. Interestingly, our results are
in contrast to the undecidability of this problem under the
Release/Acquire fragment of the C/C++11 memory model, which forms
another variant of a causally consistent memory that, in terms of
allowed outcomes, lies strictly between the two models we study.
Nevertheless, all these variants coincide for
write/write-race-free programs, which implies the decidability of
verification for such programs under Release/Acquire.
(Joint work with Udi Boker, partly presented at PLDI'20)
LFCS Seminar: 20 July 2022- Ori Lahav
IF G.03