VeriFix：验证原子性违规修复
软件工程
2025-04-24 v1
摘要
原子性违规是并发程序中最严重的错误类型之一。通常会使用同步机制来强制执行原子性。然而，由于复杂的线程交互和大输入空间，正确且充分地放置同步机制非常具有挑战性。本文提出了\textsf{VeriFix}，一种用于验证原子性违规修复的新方法。给定一个暴露原子性违规的错误痕迹及其对应的修复，\textsf{VeriFix}有效地验证该修复是否引入足够的同步机制来修复原子性违规而不会引入新的死锁。关键思想是，\textsf{VeriFix}将修复验证问题转化为属性验证问题，其中将观察到的原子性违规和潜在死锁编码为安全属性，将输入和调度编码为符号约束。通过与SMT求解器进行约束推理，\textsf{VeriFix}系统性地探索所有可达路径(从整个调度和输入空间)并验证是否存在具体的\textit{调度+输入}组合来表现出预期的原子性或任何新的死锁。我们在一组真实世界的C/C++程序上实现并评估了\verifix。结果显示，\textsf{VeriFix}显著优于最新的方法。
引用
@article{arxiv.2504.16354,
title = {VeriFix: Verifying Your Fix Towards An Atomicity Violation},
author = {Zhuang Li and Qiuping Yi and Jeff Huang},
journal= {arXiv preprint arXiv:2504.16354},
year = {2025}
}