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...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
• Keywords: Resource Invariants, Shape Analysis, Software Engineering, VMCAI 2009, first Shape Analysis