Effective Static Race Detection for Java Mayur Naik Alex Aiken



Yüklə 257,5 Kb.
tarix20.09.2018
ölçüsü257,5 Kb.
#69567


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



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

  • 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



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



Yüklə 257,5 Kb.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2023
rəhbərliyinə müraciət

    Ana səhifə