The construction and validation of highly dependable software currently requires extraordinary effort, especially when using multiple threads of control, due to the need to consider all possible thread interleavings. This research focuses on the strong, widely-applicable non-interference property of atomicity. A routine is atomic if its execution is not affected by concurrently-executing threads. This non-interference guarantee reduces the challenging problem of reasoning about the routine's behavior in a multithreaded context to the substantially simpler problem of reasoning about the routine's sequential behavior.
This work develops both dynamic and static (type-based) techniques for formally specifying and verifying atomicity properties of multithreaded programs in a cost-effective manner. It is expected that atomicity checkers developed will 1) detect atomicity violations that are resistant to both traditional testing techniques and existing tools focused on race conditions; 2) facilitate code inspection and debugging; and 3) encourage a modular design methodology that avoids unnecessary interference between threads.
