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


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.