Abstract Transformers for Thread Correlation Analysis
Abstract Transformers for Thread Correlation Analysis
复制标题
用于线程相关性分析的抽象变压器
DOI：
10.1007/978-3-642-10672-9_5
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Sagiv
中科院分区：
文献类型：
--
作者：
M. Segalov;T. Lev;R. Manevich;Ramalingam Ganesan;M. Sagiv
我们提出了一种新的技术，用于加速（共享内存）并发程序的静态分析。我们专注于计算线程相关性的分析：这样的分析推断出捕获不同线程的局部状态（以及全局状态）之间的相关性的不变量。这样的不变量是验证并发程序的许多自然属性所必需的。
然而，跟踪不同线程状态之间的相关性非常昂贵。使这种分析昂贵的一个重要因素是应用抽象变压器的成本。在本文中，我们介绍了一种技术，利用足迹和memoization的概念来计算个人的抽象变压器更有效。
我们已经在我们的并发形状分析框架中实现了这种技术。我们已经使用这个实现证明了细粒度的并发程序的属性与共享的，可变的，堆在无限数量的对象和线程的存在。我们验证的属性包括内存安全性，数据结构不变，部分正确性和线性化。我们的经验评估表明，我们的新技术大大减少了分析时间（例如，在一个案例中，增加了35倍）。
We present a new technique for speeding up static analysis of (shared memory) concurrent programs. We focus on analyses that compute thread correlations : such analyses infer invariants that capture correlations between the local states of different threads (as well as the global state). Such invariants are required for verifying many natural properties of concurrent programs.
Tracking correlations between different thread states, however, is very expensive. A significant factor that makes such analysis expensive is the cost of applying abstract transformers. In this paper, we introduce a technique that exploits the notion of footprints and memoization to compute individual abstract transformers more efficiently.
We have implemented this technique in our concurrent shape analysis framework. We have used this implementation to prove properties of fine-grained concurrent programs with a shared, mutable, heap in the presence of an unbounded number of objects and threads. The properties we verified include memory safety, data structure invariants, partial correctness, and linearizability. Our empirical evaluation shows that our new technique reduces the analysis time significantly (e.g., by a factor of 35 in one case).