BYU

Abstract by Benjamin Ogles

Personal Infomation


Presenter's Name

Benjamin Ogles

Co-Presenters

Jacob Powell

Degree Level

Undergraduate

Co-Authors

None

Abstract Infomation


Department

Computer Science

Faculty Advisor

Eric Mercer

Title

Minimizing Schedule Enumeration for Proving Data Race Freedom

Abstract

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.