SAAPP: Relatated work
In this section we give a short survey of related work. Together with formal foundations, important static and dynamic methods are described.
Models for reasoning about and characterizing race conditions
A formal model that characterizes the actual, observed and potential behaviour was first proposed by Netzer [NET91,NEM92]. This model provides a conceptual framework on which the theoretical and practical aspects of dynamic race detection and debugging for shared memory parallel program can be based [RAM95].
Netzer defines actual behavior of parallel programs as that which precisely represents program execution, observed behavior as the partial information that can be recorded and potential behaviour as the alternate executions possibly allowed by the nondeterminism in the program. These behaviors of parallel programs are used to characterize the races into general and data races. General races generally apply to programs intended to be deterministic. Data races apply to nondeterministic parallel programs that contain critical sections [RAM95].
Algorithms that compute guaranteed orderings
Emrath, Ghosh and Padua [EMP88,EGP92,EGP92] presents methods for detecting general races in programs using event synchronization. They present two algorithms for post-mortem analysis, namely the Exhaustive Pairing Algorithm (EPA) and the Common Ancestor Algorithm (CAA) to compute guaranteed orderings.
Netzer and Ghosh [NEG92] present a precise and efficient algorithm for trace analysis of programs with post-wait synchronization, without clears; the complexity of their algorithm is O(np) where n is the number of synchronization events and p is the number of processes.
Static and dynamic analysis
Most approaches to detection of races in parallel programs are a combination of static analysis and dynamic methods, since neither of the two provide sufficient information when used alone. Static analysis is faster but may report nondeterminism (due to a race) where one may not exist. Dynamic methods collect trace data during execution for either post-mortem or on-the-fly analysis and are usually more accurate than static analysis. Static analysis is valid for a wider range of data as compared to trace analysis that is just valid for the input data used in a particular execution. Practical approaches to race detection therefore usually use static analysis to determine ranges of input data which might exhibit races (and therefore identify potential races) and use trace analysis to examine these cases one by one and pinpoint the sources of nondeterminism [RAM95].
Conceptually, the various data race detection methods differ mainly in the types of synchronization primitives supported. Most static analysis methods for race detections assumes that all execution paths are possible. Under this assumption, it suffices to only examine the explicit synchronizations to determine whether sections of code may execute concurrently [NET91]. An exception is the work by Young and Taylor [YOT88], which employs symbolic execution to discover more information about possible execution paths.
Allen and Padua [ALP87] describe a method for the post-mortem analysis of Fortran programs in a shared memory parallel machine. They use static analysis to reduce the trace information collected. In [MEC93] Meller-Crummy presents a static method for Fortran programs to find which variables cannot be involved in data races, and therefore need not be checked or guarded at runtime. The method can be used to enforce strict compliance for every variable access, or to cut down considerably on the runtime overhead of dynamic checking for data races. Choi, Miller and Netzer [CMN91] describes a technique called flowback analysis for debugging parallel programs. A static program dependency graph is used together with incremental tracing to divide the program into emulation blocks. Coarse execution-time traces are used to produce incrementally more detailed traces. Similar to binary rewriting techniques, a compiler is used to insert monitoring code in a preparation phase, hence the method is likely to suffer from probe effects. For C programs using counting semaphores and the fork/join construct, Miller and Choi [MIC88] present a parallel debugger using post-mortem data race analysis. The methods in [MEC93,CMN91,MIC88] described above, typically detect data races and not general races.
Helmbold, McDowell and Wang [HDW90,HDW93] present models and algorithms to find possible event orderings in traces of programs that use anonymous synchronisation. On-the-fly analysis techniques for detecting data races in programs using fork/join and arbitrary synchronization have been developed by Schoenberg [SCH89]. A technique for detecting data races in Fortran programs using parallel do loops and synchronization using send and wait primitives, is described by Hood, Kennedy and Mellor-Crummy [HKM90].
Ramanujam and Mathew [RAM95] present an efficient and precise method for detection of nondeterminism due to errors in synchronization in parallel programs. The proposed algorithm constructs an augmented task graph, and then uses a modification of depth-first search to classify the edges in the augmented graph. The edges are analysed and the nodes that are guaranteed to execute before an event are linked to these events by edges representing guaranteed ordering among events. This ordering is used to detect both data races and general races.
Based on Lamport's happens-before partial order and Mattern's virtual time (vector clocks) DJIT [ISZ99] is a dynamic method for detection of apparent data-races in lock-based multi-threaded programs. DJIT have been implemented in Millipede and Multipage systems. The method detects the first apparent data race in a program when it actually occurs. It is based on the assumption that is enough to announce only the very first data race, since later races can be after-effects of the first one. After a race is found and fixed, the search for other races can proceed in an ordinary debug fashion. The main disadvantage of the technique is that it is highly dependent on the scheduling order.