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