|
Effective Static Race Detection for Java Mayur Naik Alex Aiken
|
tarix | 20.09.2018 | ölçüsü | 257,5 Kb. | | #69567 |
|
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 Two broad classes
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
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
Step 1 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
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
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
Dostları ilə paylaş: |
|
|