Optimal Reads-From Consistency Checking for C11-Style Memory Models

Explore a 15-minute video presentation from the PLDI 2023 conference that delves into the complexity of consistency checking for C11-style memory models. Learn about the researchers' study on reads-from consistency checking for popular variants of the C11 memory model, including RC20, release-acquire (RA), strong and weak RA, and the Relaxed fragment of RC20. Discover the rich complexity landscape drawn by the team, including nearly-linear-time algorithms for certain variants, fine-grained optimality results, and matching upper and lower bounds for others. Understand how this work characterizes the complexity of consistency checking for C11 memory models and its implications for applications in testing and model checking. Gain insights into the implementation of these algorithms in the TruSt model checker and C11Tester testing tool, and their performance improvements on standard benchmarks.