Compositional Bitvector Analysis for Concurrent Programs with Nested Locks

We propose a new technique to perform bitvector data flow analysis for concurrent programs. Our algorithm works for concurrent programs with nested locking synchronization. We show that this algorithm computes precise solutions (meet over all paths) to bitvector problems. Moreover, this algorithm is compositional: it first solves a local (sequential) data flow problem, and then efficiently combines these solutions leveraging reachability results on nested locks [Kahlon et al]. We have implemented our algorithm on top of an existing sequential data flow analysis tool, and demonstrate that the technique performs and scales well.

SAS10 slides

@inproceedings{Farzan2010,
author    = {Azadeh Farzan and
Zachary Kincaid},
title     = {Compositional Bitvector Analysis for Concurrent Programs
with Nested Locks},
booktitle = {SAS},
year      = {2010},
pages     = {253-270},
ee        = {http://dx.doi.org/10.1007/978-3-642-15769-1_16},
bibsource = {DBLP, http://dblp.uni-trier.de},
}