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

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta
• Keywords: Algorithms, Concurrent Programs, Product Graph, Static Analyses, TACAS 2009