Detecting data races in Cilk programs that use locks

摘要: When two parallel threads holding no locks in common access the same memory location and at least one of modifies location, a “data race” occurs, which is usually bug. This paper describes algorithms strategies used by debugging tool, called Nondeterminator-2, checks for data races programs coded Cilk multithreaded language. Like its predecessor, Nondeterminator, simple “determinacy” races, Nondeterminator-2 not verifier, since it only computation generated serial execution program on given input. We give an algorithm, ALL-SETS, that determines whether input contains race. For runs serially time T , accesses V shared locations, uses total n locks, holds most k simultaneously, ALL-SETS O(nkT α(V;V )) O(nkV ) space, where α Tarjan’s functional inverse Ackermann’s function. Since may be too inefficient worst case, we propose much more efficient algorithm can to detect obey “umbrella” locking discipline, programming methodology flexible than similar disciplines proposed literature. present BRELLY, detects violations umbrella discipline O(kT using O(kV space. also prove any “abelian” program, whose critical sections commute, produces determinate final state if deadlock free generates datarace free. Thus, Nondeterminator-2’s verify determinacy deadlock-free abelian running Keywords