Abstract by Benjamin Ogles
Minimizing Schedule Enumeration for Proving Data Race Freedom
3M. Race conditions in concurrent programs are notoriously hard to detect and can cause numerous bugs that surface infrequently. Much work has been done by Nakade et al. to prove data race freedom in task parallel programs for a given input set. Their use of computation graphs proved model checking as a viable method for detecting data race by only requiring the model checker to enumerate the schedules around mutual exclusion blocks. We will expand upon this optimization by using Weak Causally-Precedes instead of Happens-Before to construct each computation graph, further reducing the number of schedules enumerated by the model checker. We will also use the BigFoot algorithm to eliminate redundant checks on shared memory locations. We will provide empirical results on the performance of Nakade’s method with and without each of these optimizations as well as compared to the fully combined algorithm.