This is an old revision of the document!
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