一句话：提出基于 Datalog 的快速近似静态分析，通过识别差异化数据流边来计算并发程序的同步语义差异。
当并发程序因线程同步问题被修改时，需要确认修改不会引入意外行为。人工比较两个程序的语义差异费时且易错，而基于模型检测的方法计算代价高昂。为此，本文提出一种快速且近似的静态分析，用于计算两个程序的同步差异。该方法不依赖重量级模型检测，而是利用多项式时间的 Datalog 程序分析框架来计算差异化数据流边，即一个程序允许而另一个程序不允许的边。尽管采用近似，但通过精心设计的 Datalog 推理规则，并迭代增加表示差异所需的数据流边，方法仍具有足够精度。作者实现该方法并在大量多线程 C 程序上评估，通常在数秒内得到与人工判断一致的差异；相比之下，已有模型检测技术需要数分钟甚至数小时，慢 10 倍到 1000 倍。
When an evolving program is modified to address issues related to thread synchronization, there is a need to confirm the change is correct, i.e., it does not introduce unexpected behavior. However, manually comparing two programs to identify the semantic difference is labor intensive and error prone, whereas techniques based on model checking are computationally expensive. To fill the gap, we develop a fast and approximate static analysis for computing synchronization differences of two programs. The method is fast because, instead of relying on heavy-weight model checking techniques, it leverages a polynomial-time Datalog-based program analysis framework to compute differentiating data-flow edges, i.e., edges allowed by one program but not the other. Although approximation is used our method is sufficiently accurate due to careful design of the Datalog inference rules and iterative increase of the required data-flow edges for representing a difference. We have implemented our method and evaluated it on a large number of multithreaded C programs to confirm its ability to produce, often within seconds, the same differences obtained by human; in contrast, prior techniques based on model checking take minutes or even hours and thus can be 10x to 1000x slower.
DOI 原文 ·
@inproceedings{paperbot4779,
title = {Datalog-based scalable semantic diffing of concurrent programs},
author = {Chungha Sung and Shuvendu K. Lahiri and Constantin Enea and Chao Wang},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3238211}
}