Race Condition Detection for Debugging Parallel Programs

点击翻译按钮获取中文摘要

The first objective of this project is to develop a formal model for reasoning about program executions and race conditions, allowing different types of race conditions to be precisely defined and properties of various techniques to be proven and compared. This model will distinguish between the program's actual behavior, its potential behavior, and its observed behavior. The second objective is to develop dynamic techniques for detecting race conditions as accurately as possible given the constraint of limited run-time information. These techniques aid the programmer in debugging by locating those races that are direct manifestations of program bugs and not artifacts caused by other races, imprecise run-time traces (causing false races to appear real), or implicit synchronization (caused by shared-memory references). These techniques analyze the observed behavior to conservatively speculate on races that either did occur or had the potential of occurring, and that were unaffected by any other race in the execution. The result of this research is both a theory in which to reason about race conditions and prove properties of techniques for race condition detection, and techniques that aid the programmer by efficiently locating those race conditions that are of interest for debugging.