Thread-modular shape analysis

Thread-modular shape analysis,10.1145/1273442.1250765,Sigplan Notices,Alexey Gotsman,Josh Berdine,Byron Cook,Mooly Sagiv

Thread-modular shape analysis  
BibTex | RIS | RefWorks Download
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.
Journal: Sigplan Notices - SIGPLAN , vol. 42, no. 6, pp. 266-277, 2007
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.