P. Ferrara.
A fast and precise analysis for data race detection

in Proceedings of the Third Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2008), ENTCS, Elsevier, Budapest, Hungary, April 5-6, 2008

Final version: Pdf (220 KB)
Slides: Pdf (150 KB)

Abstract: When two threads access the shared memory without being synchronized, and at least one performs a write operation, they form a data race. Data races are widely considered the symptom of bugs in multithreaded programs, and a huge amount of work has been done in order to detect them. The key issue in order to statically discover data races via abstract interpretation in Java programs is to develop a specific alias analysis that abstracts references, as (i) the shared memory is the heap, and it is accesses by reference (ii) monitors are defined on objects, and so they are identified by reference. This paper presents a combination of may- and must- alias analyses, in order to capture precise information on accesses and synchronization. Moreover, we provide information on missing locks if a possible data race is detected. The analysis has been implemented and tested. Our approach is based on abstract interpretation theory and it analyzes a subset of Java bytecode.

Keywords: Static Analysis, Abstract Interpretation, Data Race, Alias Analysis

Bibtex:

@inproceedings{Ferr08a,
  author = {Pietro Ferrara},
  title = {A fast and precise alias analysis for data race detection},
  booktitle = {Proceedings of the Third Workshop on Bytecode Semantics, Verification,
               Analysis and Transformation (Bytecode'08)},
  year = {2008},
  publisher = {Elsevier},
  volume = {Electronic Notes in Theoretical Computer Science},
  month = {April},
}