Thread-Modular Shape Analysis

12 years 10 months ago
Thread-Modular Shape Analysis
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. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Languages, Theory, Verification Abstract interpretation, concurrent programming, shape analysis, static a...
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sa
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Authors Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
Comments (0)