Analysis of synchronization errors for multithreaded programs

This dissertation describes runtime, static, and hybrid analyses to detect synchronization errors in multi-threaded programs. Three kinds of synchronization errors are considered: deadlocks, data races, and atomicity violations. Deadlocks and data races are well known and have been studied for a long time. Atomicity violation is not as well-known and deeply studied. This dissertation focuses on detecting atomicity violations.;Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multi-threaded programs, executions of procedures (or methods) can be regarded as transactions. Correctness in the presence of concurrency typically requires atomicity of these transactions. Tools that automatically detect atomicity violations can uncover subtle errors that are hard to find with traditional debugging and testing techniques. Furthermore, an atomic code block can be treated as a single transition during subsequent analysis of the program; this can greatly improve the efficiency of the subsequent analysis.;This dissertation describes three algorithms for runtime detection of atomicity violations and compares their cost and effectiveness. The reduction-based algorithm checks atomicity based on commutativity properties of events in a trace. The block-based algorithm efficiently represents the relevant information about a trace as a set of blocks (i.e., pairs of events plus associated synchronization), and checks atomicity by comparing each block with other blocks. The commit-node algorithm organizes the events in each transaction into a tree, then detects atomicity violations by analyzing relationships between nodes in different trees.;We evaluated the algorithms on several benchmarks totaling 36 KLOC. Many synchronization errors were revealed, including some previously unknown errors in Sun's implementation of the Java standard library. The block-based algorithm is most accurate; the reduction-based algorithm is the least accurate; the commit-node algorithm is less accurate than the block-based algorithm in theory, but they have the same accuracy in practice. In practice, the commit-node algorithm is as fast as the reduction-based algorithm, and significantly faster than the block-based algorithm.;This dissertation also presents an automated static analysis of atomicity for programs that use non-blocking synchronization. The analysis determines commutativity of operations based primarily on how synchronization primitives (including locks, load-linked, store-conditional, and compare-and-swap) are used. A reduction theorem states that certain patterns of commutativity imply atomicity. We successfully applied the analysis to several well-known non-blocking algorithms that cannot be automatically analyzed using previous approaches.;We also developed more accurate and efficient runtime algorithms for detecting deadlocks and data races in multi-threaded programs.;We explored the use of static analysis to significantly decrease the overhead of runtime checking for synchronization errors. The analysis results of the type systems are used to identify parts of the program from which runtime checking can safely be omitted.