Sciweavers

Share
TACAS
2009
Springer

Semantic Reduction of Thread Interleavings in Concurrent Programs

10 years 20 days ago
Semantic Reduction of Thread Interleavings in Concurrent Programs
Abstract. We propose a static analysis framework for concurrent programs based on reduction of thread interleavings using sound invariants on the top of partial order techniques. Starting from a product graph that represents transactions, we iteratively refine the graph to remove statically unreachable nodes in the product graph using the results of alyses. We use abstract interpretation to automatically derive invariants, based on abstract domains of increasing precision. We demonstrate the benefits of this framework in an application to find data race bugs in concurrent programs, where our static analyses serve to reduce the number of false warnings captured by an initial lockset analysis. This framework also facilitates use of model checking on the remaining warnings to generate concrete error traces, where we leverage the preceding static analyses to generate small program slices and the derived invariants to improve scalability. We describe our experimental results on a suite o...
Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupt
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where TACAS
Authors Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta
Comments (0)
books