一句话：提出最大路径因果性模型，把到达同一路径的调度与输入组合归为等价类，统一探索并发程序调度与输入空间。
并发程序验证需同时探索线程调度空间和输入空间，二者组合导致状态爆炸。本文提出最大路径因果性（MPC）模型，将能够到达同一程序路径的所有线程调度与程序输入组合视为一个等价类，并为每条路径生成唯一的调度+输入组合进行探索；基于该模型的技术还可自然并行化不同路径的探索。作者在常见并发基准和真实 C/C++ 应用上进行了广泛评估，结果表明 MPC 显著提升了现有技术的性能，能更高效地覆盖调度与输入交织的并发行为。
We present a technique that systematically explores the state spaces of concurrent programs across both the schedule space and the input space. The cornerstone is a new model called Maximal Path Causality (MPC), which captures all combinations of thread schedules and program inputs that reach the same path as one equivalency class, and generates a unique schedule+input combination to explore each path. Moreover, the exploration for different paths can be easily parallelized. Our extensive evaluation on both popular concurrency benchmarks and real-world C/C++ applications shows that MPC significantly improves the performance of existing techniques.
DOI 原文 ·
@inproceedings{paperbot4681,
title = {Concurrency verification with maximal path causality},
author = {Qiuping Yi and Jeff Huang},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3236048}
}