Effective Static Race Detection for Java Mayur Naik Alex Aiken

Effective Static Race Detection for Java

• Mayur Naik

• Alex Aiken

• John Whaley

• Stanford University

The Problem

• A multi-threaded program contains a race if:

• Two threads can access a memory location
• At least one access is a write
• No ordering between the accesses

• As a rule, races are bad

• And common …
• And hard to find …

Previous Work

• A lot of previous work

• Dozens of papers in on-line citation indices
• Spanning decades

• Two broad classes

• Dynamic
• Static

Dynamic Race Detectors

• Three kinds

• happens-before (Lamport, 1978)
• lockset (Savage et al., 1997)
• hybrid (e.g., O’Callahan and Choi, 2003)

• Drawbacks

• Unsound
• Cannot analyze open programs (e.g., libraries)
• Need sufficient input data for closed programs

Static Race Detectors

• Three kinds

• Type systems (e.g., rccjava, LOCKSMITH)
• Dataflow analyses (e.g., RacerX)
• Model checkers (e.g., BLAST, KISS)

• Drawback: all find relatively few bugs

• Precise techniques not applied to large programs
• Coarse techniques find a few bugs in > 1 MLOC

# Bugs Found Using Our Approach

Our Static Race Detection Algorithm

Architecture of Chord

Flow Insensitivity

• Helps scalability

• Hurts precision

• Affects kinds of synchronization idioms we can handle

• Lexically-scoped, lock-based synchronization
• fork/join synchronization (42 annotations in 1.5 MLOC)
• wait/notify synchronization

• Simplifies handling of open programs

• Simplifies counterexample generation

Context Sensitivity

• Precise alias analysis is crucial

• Central to call graph, thread-escape, and lock analyses
• Most alias analyses are too imprecise
• CHA, context-insensitive analysis, k-CFA

• What works: k-object-sensitive analysis

• Proposed by Milanova et al., 2003
• Our implementation leverages BDD-based context-sensitive program analysis
• k = 3 necessary in our experiments

Running Example

Computing Original Pairs

• All pairs of accesses such that:

• Both access the same instance field or the same static field or array elements
• At least one is a write

Example: Original Pairs

Computing Reachable Pairs

• Step 1

• Access pairs with at least one write to same field

• Step 2

• Consider access pair (e1, e2)
• To have a race, e1 must be reachable from a thread-spawning call site s1 without “switching” threads
• And s1 must be reachable from main
• And similarly for e2

Example: Reachable Pairs

Example: Two Object-Sensitive Contexts

Example: 1st Context

Example: 2nd Context

Example: Reachable Pairs

Computing Aliasing Pairs

• Steps 1-2

• Access pairs with at least one write to same field
• And both are reachable from some thread

• Step 3

• To have a race, both must access the same memory location
• Use alias analysis

Example: Aliasing Pairs

Computing Escaping Pairs

• Steps 1-3

• Access pairs with at least one write to same field
• And both are reachable from some thread
• And both can access the same memory location

• Step 4

• To have a race, the memory location must also be thread-shared
• Use thread-escape analysis

Example: Escaping Pairs

Computing Unlocked Pairs

• Steps 1-4

• Access pairs with at least one write to same field
• And both are reachable from some thread
• And both can access the same memory location
• And the memory location is thread-shared

• Step 5

• Discard pairs where the memory location is guarded by a common lock in both accesses
• Needs must-alias analysis
• We use approximation of may-alias analysis, which is unsound

Example: Unlocked Pairs

Example: Counterexample

Benchmarks

• vect1.1

• htbl1.1

• htbl1.4

• vect1.4

• tsp

• hedc

• ftp

• pool

• jdbm

• jdbf

• jtds

• derby

Running Time and Annotation Counts

• vect1.1

• htbl1.1

• htbl1.4

• vect1.4

• tsp

• hedc

• ftp

• pool

• jdbm

• jdbf

• jtds

• derby

Pairs Retained After Each Stage (Log scale)

Classification of Unlocked Pairs

• vect1.1

• htbl1.1

• htbl1.4

• vect1.4

• tsp

• hedc

• ftp

• pool

• jdbm

• jdbf

• jtds

• derby

Conclusions

The End