Abstract by Benjamin Ogles

Personal Infomation

Presenter's Name

Benjamin Ogles


Jacob Powell

Degree Level




Abstract Infomation


Computer Science

Faculty Advisor

Eric Mercer


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.