一句话：提出 TruSt 算法，使并发程序动态偏序归约同时做到每等价类仅探索一个交错且内存消耗为线性。
动态偏序归约（DPOR）通过按 Mazurkiewicz 迹等价类探索交错来验证并发程序，但现有算法难以兼顾空间与时间：探索最优的算法可能消耗指数级内存，而多项式内存的算法可能探索大量冗余交错。本文提出 TruSt，首次同时实现每等价类仅探索一个交错且内存消耗为线性。TruSt 在 Coq 中形式化，不仅适用于顺序一致性，也适用于满足若干基本假设的弱内存模型（如 TSO、PSO 和 RC11）。此外，TruSt 天然可并行：不同探索选项间无共享状态，可完全并行执行。实验表明，TruSt 在内存和/或时间上均优于现有最先进方法。
Dynamic partial order reduction (DPOR) verifies concurrent programs by exploring all their interleavings up to some equivalence relation, such as the Mazurkiewicz trace equivalence. Doing so involves a complex trade-off between space and time. Existing DPOR algorithms are either exploration-optimal (i.e., explore exactly only interleaving per equivalence class) but may use exponential memory in the size of the program, or maintain polynomial memory consumption but potentially explore exponentially many redundant interleavings. In this paper, we show that it is possible to have the best of both worlds: exploring exactly one interleaving per equivalence class with linear memory consumption. Our algorithm, TruSt, formalized in Coq, is applicable not only to sequential consistency, but also to any weak memory model that satisfies a few basic assumptions, including TSO, PSO, and RC11. In addition, TruSt is embarrassingly parallelizable: its different exploration options have no shared state, and can therefore be explored completely in parallel. Consequently, TruSt outperforms the state-of-the-art in terms of memory and/or time.
@article{paperbot1573,
title = {Truly stateless, optimal dynamic partial order reduction},
author = {Michalis Kokologiannakis and Iason Marmanis and Vladimir Gladstein and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498711}
}