RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency

This conference talk from POPL 2025 presents RELINCHE, a model checker designed to automatically verify linearizability of concurrent libraries under relaxed memory consistency models. Learn how researchers Pavel Golovin, Michalis Kokologiannakis, and Viktor Vafeiadis developed a tool that establishes refinement between concurrent library implementations and their atomic specifications in parallel client environments. Discover how RELINCHE scales to verify correctness of standard concurrent library benchmarks for client programs with up to 7-9 library method invocations, while efficiently identifying minimal counterexamples of linearizability bugs caused by weak memory consistency with only 4-7 method calls. The presentation includes discussion of the verification approach that strengthens refinement to capture all possible constrained clients of a library. The research paper and supplementary artifacts are available online, with the artifacts having been evaluated as reusable.