Patent ID: 8200474

Claim:
A method for dynamic data race detection for concurrent systems, comprising: computing lockset information using a processor for different components of a concurrent system; performing a controlled execution of the system where the controlled execution explores different interleavings of the concurrent components; utilizing the lockset information during the controlled execution to check whether a search subspace associated with a state in the execution is free of data races; and dynamically pruning a race-free search subspace to reduce resource usage; where for each pair of segments (seg i , seg j ) with tid(seg i )≠tid(seg j ) and each variable x, checking whether ∃lksetSet(seg i , x), lkset 2 εlksetSet(seg j , x)such that lkset 1 ∩lkset 2 =0, where set lksetSet(seg i , x) includes locksets associated with accesses of x in seg i and tid(t) denotes a thread index of transition t.