AI, Data Science & Cloud Certificates from Google, IBM & Meta — 40% Off
One plan covers every Professional Certificate on Coursera. 40% off Coursera Plus Annual.
Unlock All Certificates
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.
