Compositional bitvector analysis for concurrent programs with nested locks

Azadeh Farzan; Zachary Kincaid

doi:10.1007/978-3-642-15769-1_16

Compositional bitvector analysis for concurrent programs with nested locks

Azadeh Farzan, Zachary Kincaid

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

9 Scopus citations

Abstract

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 [6,7]. We have implemented our algorithm on top of an existing sequential data flow analysis tool, and demonstrate that the technique performs and scales well.

Original language	English (US)
Title of host publication	Static Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages	253-270
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-642-15769-1_16
State	Published - 2010
Externally published	Yes
Event	17th International Static Analysis Symposium, SAS 2010 - Perpignan, France Duration: Sep 14 2010 → Sep 16 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6337 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	17th International Static Analysis Symposium, SAS 2010
Country/Territory	France
City	Perpignan
Period	9/14/10 → 9/16/10

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-15769-1_16

Cite this

Farzan, A., & Kincaid, Z. (2010). Compositional bitvector analysis for concurrent programs with nested locks. In Static Analysis - 17th International Symposium, SAS 2010, Proceedings (pp. 253-270). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS). https://doi.org/10.1007/978-3-642-15769-1_16

@inproceedings{eb9e385cb25b485d9a04a194d7bca5e1,

title = "Compositional bitvector analysis for concurrent programs with nested locks",

abstract = "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 [6,7]. We have implemented our algorithm on top of an existing sequential data flow analysis tool, and demonstrate that the technique performs and scales well.",

author = "Azadeh Farzan and Zachary Kincaid",

year = "2010",

doi = "10.1007/978-3-642-15769-1_16",

language = "English (US)",

isbn = "3642157688",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "253--270",

booktitle = "Static Analysis - 17th International Symposium, SAS 2010, Proceedings",

}

Farzan, A & Kincaid, Z 2010, Compositional bitvector analysis for concurrent programs with nested locks. in Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6337 LNCS, pp. 253-270, 17th International Static Analysis Symposium, SAS 2010, Perpignan, France, 9/14/10. https://doi.org/10.1007/978-3-642-15769-1_16

Compositional bitvector analysis for concurrent programs with nested locks. / Farzan, Azadeh; Kincaid, Zachary.
Static Analysis - 17th International Symposium, SAS 2010, Proceedings. 2010. p. 253-270 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Compositional bitvector analysis for concurrent programs with nested locks

AU - Farzan, Azadeh

AU - Kincaid, Zachary

PY - 2010

Y1 - 2010

N2 - 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 [6,7]. We have implemented our algorithm on top of an existing sequential data flow analysis tool, and demonstrate that the technique performs and scales well.

AB - 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 [6,7]. We have implemented our algorithm on top of an existing sequential data flow analysis tool, and demonstrate that the technique performs and scales well.

UR - http://www.scopus.com/inward/record.url?scp=78149248231&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78149248231&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-15769-1_16

DO - 10.1007/978-3-642-15769-1_16

M3 - Conference contribution

AN - SCOPUS:78149248231

SN - 3642157688

SN - 9783642157684

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 253

EP - 270

BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings

T2 - 17th International Static Analysis Symposium, SAS 2010

Y2 - 14 September 2010 through 16 September 2010

ER -

Compositional bitvector analysis for concurrent programs with nested locks

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this