无回归的并发程序综合
编程语言
2014-07-15 v1 计算机科学中的逻辑
摘要
在修复并发错误时，程序修复算法可能会引入新的并发错误。我们提出了一种避免此类回归的算法。解空间由我们在修复过程中考虑的一组程序变换给出。这些变换包括线程内指令的重排序和插入原子区段。新算法从正例（无错误轨迹）和反例（错误轨迹）中学习候选解空间的约束。从每个反例中，算法学习消除错误所必需的约束。从每个正例中，它学习防止修复将轨迹转变为错误轨迹所必需的约束。我们实现了该算法，并在具有已知错误的简化 Linux 设备驱动程序上进行了评估。
引用
@article{arxiv.1407.3681,
title = {Regression-free Synthesis for Concurrency},
author = {Pavol Černý and Thomas A. Henzinger and Arjun Radhakrishna and Leonid Ryzhyk and Thorsten Tarrach},
journal= {arXiv preprint arXiv:1407.3681},
year = {2014}
}
备注
for source code see https://github.com/thorstent/ConRepair