What is a data race?
Happens before.
In lock-based programs.
Approximating whether there can be a race at two accesses:
- locations disjoint
- locks same - unsound approximation in absence of must analysis (“unlikely races”)
- locations same, then locks same (conditional may alias analysis)
Open programs and harness synthesis
- called sites using stubs or no-ops
- non-deterministic code that calls libraries
Phases of the analysis
- OriginalPairs: based on static types
- reachable pairs: alias analysis + call graph analysis
- aliasing-pairs: k-object sensitive alias analysis + bddbddb
- Escaping-Pairs: thread escape analysis
- Unlocked-Pairs
- Error-reporting
Annotations
Unsoundess summary
Experimental results
POPL'07 extensions - sound, no annotations
- separate method and thread creation context
- disjoint reachability to check conditional may alias analysis
- more precise escape analysis
- may-happen in parallel analysis: if thread and call context can execute at the same time
- intraprocedural must alias analysis for field accesses
Disjoint reachability analysis: approximate transitive closure of (o1,o2) such that there was some o1.f=o2 assignment during execution.