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.