Compositional bitvector analysis for concurrent programs with nested locks

Azadeh Farzan, Zachary Kincaid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 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 languageEnglish (US)
Title of host publicationStatic Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages253-270
Number of pages18
DOIs
StatePublished - Nov 12 2010
Externally publishedYes
Event17th International Static Analysis Symposium, SAS 2010 - Perpignan, France
Duration: Sep 14 2010Sep 16 2010

Publication series

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

Other

Other17th International Static Analysis Symposium, SAS 2010
CountryFrance
CityPerpignan
Period9/14/109/16/10

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Compositional bitvector analysis for concurrent programs with nested locks'. Together they form a unique fingerprint.

Cite this