Checking Atomicity for Improved Multithreaded Software Reliability

高可靠性软件的构建和验证通常需要付出非凡的努力，特别是在使用多线程控制时，因为需要考虑所有可能的线程交织。本研究的重点是原子性强、适用范围广的非干涉性。 如果例程的执行不受并发执行线程的影响，则例程是原子的。 这种非干扰保证减少了challengingproblem的推理有关例程的行为在multiprobedcontext的推理theroutine的顺序behavior.This工作开发了动态和静态（基于类型）的技术正式指定和验证atomicity属性的多线程程序在一个成本效益的方式大大简单的问题。 预计开发的原子性检查器将1）检测原子性违规，这些违规对传统测试技术和专注于竞争条件的现有工具都有抵抗力; 2）促进代码检查和调试; 3）鼓励模块化设计方法，避免线程之间不必要的干扰。

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.