从单线程到多线程：一种高效的静态分析算法
摘要：多线程程序的安全性分析是计算单线程程序安全属性的静态分析方法的一个重要方向。本文提出了一种系统的方法来扩展这类静态分析方法，使其能够处理具有多个 POSIX 风格线程的程序。从实用的操作语义出发，我们构建了一种表示 assume-guarantee 推理的指示语义。最后的算法通过抽象解释来得到。它按顺序分析每个线程，并传递线程间的干扰，以及其他语义信息。通过避免显式考虑所有可能的交错序列，我们避免了由此带来的组合爆炸。最坏情况下的复杂度只增加了一个因子 n，其中 n 是程序中的指令数。我们还实现了原型工具，证明了该方法的实用性。
作者：Jean-Loup Carre and Charles Hymans
论文ID：0910.5833
分类：Programming Languages
分类简称：cs.PL
提交时间：2009-11-02