Checking Atomicity for Improved Multithreaded Software Reliability

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

The construction and validation of highly dependable softwarecurrently requires extraordinary effort, especially when usingmultiple threads of control, due to the need to consider all possiblethread interleavings. This research focuses on the strong,widely-applicable non-interference property of atomicity. A routineis atomic if its execution is not affected by concurrently-executingthreads. This non-interference guarantee reduces the challengingproblem of reasoning about the routine's behavior in a multithreadedcontext to the substantially simpler problem of reasoning about theroutine's sequential behavior.This work develops both dynamic and static (type-based) techniques forformally specifying and verifying atomicity properties ofmultithreaded programs in a cost-effective manner. It is expectedthat atomicity checkers developed will 1) detect atomicity violationsthat are resistant to both traditional testing techniques and existingtools focused on race conditions; 2) facilitate code inspection anddebugging; and 3) encourage a modular design methodology that avoidsunnecessary interference between threads.