一句话：提出适用于 SC、TSO 和 PSO 内存模型的序一致性理论及 SMT 求解器 Zord，显著提升并发程序验证性能。
自动验证多线程程序面临线程交错数量巨大的挑战，弱内存一致性进一步加剧该问题。偏序能够简洁表示大量线程交错，但此前没有专门的偏序约束判定过程。本文提出一种新的序一致性理论，用于并发程序验证，不仅适用于顺序一致性（SC），也适用于 TSO 和 PSO 弱内存模型。作者进一步设计高效的理论求解器，支持增量一致性检查、生成最小冲突子句，并加入定制传播过程。该求解器实现为工具 Zord，并在 SV-COMP 2020 ConcurrencySafety 基准上开展大量实验。结果表明，该方法相比现有最先进技术有显著提升。
Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, there is no dedicated decision procedure for solving partial-order constraints. In this article, we propose a novel ordering consistency theory for concurrent program verification that is applicable not only under sequential consistency, but also under the TSO and PSO weak memory models. We further develop an efficient theory solver, which checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. We have implemented our approach in a tool, called Zord , and have conducted extensive experiments on the SV-COMP 2020 ConcurrencySafety benchmarks. Our experimental results show a significant improvement over the state-of-the-art.
@article{paperbot2138,
title = {Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models},
author = {Hongyu Fan and Zhihang Sun and Fei He},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {1},
year = {2023},
doi = {10.1145/3579835}
}