Thread-modular shape analysis
Thread-modular shape analysis
复制标题
螺纹模形状分析
DOI：
10.1145/1250734.1250765
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Shmuel Sagiv
中科院分区：
文献类型：
--
作者：
Alexey Gotsman;Josh Berdine;Byron Cook;Shmuel Sagiv
我们提出了第一个形状分析多线程程序，避免了显式枚举的执行交织。我们的方法是自动推断与每个锁相关联的资源不变式，该资源不变式描述了由锁保护的堆的部分。这允许我们对每个线程使用顺序形状分析。我们表明，资源不变量的某一类可以表征为至少不动点，并通过重复应用程序的形状分析计算，只有在每个单独的线程。基于这种方法，我们已经实现了一个线程模块化的形状分析工具，并将其应用于并发堆操作代码从Windows设备驱动程序。
We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.