Semantic Reduction of Thread Interleavings in Concurrent ProgramsVineet Kahlon , Sriram Sankaranarayanan and Aarti Gupta |
|
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
these analyses. We use abstract interpretation to automatically derive
program 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 of Linux
device drivers.
|
| Tools and Algorithms for Construction and Analysis of Systems (TACAS 2009), Volume 5505/2009 of Lecture Notes in Computer Science, pp. 124-138, Springer-Verlag. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |