Abstract by Benjamin Ogles
Proving an Efficient Data Race Detection Algorithm Correct
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.