一句话：提出 Relinche，全自动模型检测器，在弱内存一致性下验证并发库的原子性与功能正确性。
并发库（如栈、队列）是并发程序的基本构件，通常向客户端提供原子接口，并采用复杂同步机制以提升性能。本文研究如何在弱内存一致性下全自动验证这类库的正确性。作者开发了模型检测器 Relinche：它针对在完全并行客户端中使用该库的程序，建立并发库实现与其原子规约之间的精化（refinement）关系，再将结果加强以覆盖所有其他（更受限）的客户端，从而验证库方法被有界次数调用时的原子性与功能正确性。实验表明，Relinche 能扩展到标准并发库基准测试，验证所有客户端程序在最多 7–9 次库方法调用下的正确性；同时，对于由弱内存一致性导致的非平凡线性一致性缺陷，它能找到仅含 4–7 次方法调用的最小反例。
Concurrent libraries implement standard data structures, such as stacks and queues, in a thread-safe manner, typically providing an atomic interface to the data structure. They serve as building blocks for concurrent programs, and incorporate advanced synchronization mechanisms to achieve good performance. In this paper, we are concerned with the problem of verifying correctness of such libraries under weak memory consistency in a fully automated fashion. To this end, we develop R elinche , a model checker that verifies atomicity and functional correctness of a concurrent library implementation in any client program that invokes the library methods up to some bounded number of times. Our tool establishes refinement between the concurrent library implementation and its atomic specification in a fully parallel client, which it then strengthens to capture all possible other (more constrained) clients of the library. R elinche scales sufficiently to verify correctness of standard concurrent library benchmarks for all client programs with up to 7–9 library method invocations, and finds minimal counterexamples with 4-7 method calls of non-trivial linearizability bugs due to weak memory consistency.
@article{paperbot3229,
title = {RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency},
author = {Pavel Golovin and Michalis Kokologiannakis and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704906}
}