BYU

Abstract by Benjamin Ogles

Personal Infomation


Presenter's Name

Benjamin Ogles

Co-Presenters

Joshua Hooker

Degree Level

Undergraduate

Co-Authors

Eric Mercer

Abstract Infomation


Department

Computer Science

Faculty Advisor

Eric Mercer

Title

Proving an Efficient Data Race Detection Algorithm Correct

Abstract

Data race is a prevalent error in task-parallel programs. We have developed an algorithm, named Zipper to detect data race automatically during program executions. This algorithm uses efficient data structures to achieve better performance on some programs. However, unlike other automatic data race detectors, Zipper has not been proven sound (only detects real errors) and complete (always detects an error if it exists). We aim to prove these properties for Zipper using the Coq proof assistant. First we will formalize the notion of a well formed program execution. Then we will define the well known (sound and complete) Happens-before (HB) relation over these executions. We will then prove an equivalence between the unordered events of the HB relation and the potential data races that Zipper considers. Finally, we will prove that the first data race that Zipper detects is the first data race that the HB relation reveals.