TY - GEN
T1 - Semantic reduction of thread interleavings in concurrent programs
AU - Kahlon, Vineet
AU - Sankaranarayanan, Sriram
AU - Gupta, Aarti
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70350225022&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350225022&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-00768-2_12
DO - 10.1007/978-3-642-00768-2_12
M3 - Conference contribution
AN - SCOPUS:70350225022
SN - 3642007678
SN - 9783642007675
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 124
EP - 138
BT - Tools and Algorithms for the Construction and Analysis of Systems - 15th International Conference, TACAS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc.
T2 - 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009
Y2 - 22 March 2009 through 29 March 2009
ER -