并发高阶程序静态分析的一族抽象解释
编程语言
2011-06-15 v2
摘要
我们开发了一个框架，用于计算并发高阶程序的两种基础分析：(控制)流分析(CFA)和可能并行分析(MHP)。我们特别关注由一等续延与动态生成线程的无限制混合所带来的独特挑战。为奠定基础，我们构建了一个并发高阶程序的具体模型：P(CEK*)S 机器。我们发现，对该机器进行系统的抽象解释能够同时计算流分析和 MHP 分析。然而，进一步检查发现 MHP 的精度较差。作为补救措施，我们将一种形状分析技术——单例抽象——应用于动态生成的线程（而非堆中的对象）。然后我们证明，如果对 MHP 分析不感兴趣，可以通过第二层抽象折叠线程交错，从而大幅加速仅流分析的计算。
引用
@article{arxiv.1103.5167,
title = {A family of abstract interpretations for static analysis of concurrent higher-order programs},
author = {Matthew Might and David Van Horn},
journal= {arXiv preprint arXiv:1103.5167},
year = {2011}
}
备注
The 18th International Static Analysis Symposium (SAS 2011)