Optimal Stateless Model Checking for Causal Consistency.

We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, CCv , CM , CC . Our approach is based on exploring traces under the program order [inline-graphic not available: see fulltext] and the reads from [inline-graphic not available: see fulltext] relations. Our SMC algorithm is provably optimal in the sense that it explores each [inline-graphic not available: see fulltext] and [inline-graphic not available: see fulltext] relation exactly once. We have implemented our framework in a tool called Conschecker. Experiments show that Conschecker performs well in detecting anomalies in classical distributed databases benchmarks.