Checking Atomicity for Improved Multithreaded Software Reliability

目前，高度可靠的软件的构建和验证需要付出巨大的努力，特别是在使用多线程控制时，因为需要考虑所有可能的线程交错。本研究重点关注原子性强、适用范围广的非干涉性。 如果例程的执行不受并发执行线程的影响，则该例程是原子的。 这种无干​​扰保证将多线程上下文中例程行为推理的挑战性问题减少为例程顺序行为推理的简单问题。这项工作开发了动态和静态（基于类型）技术，以经济高效的方式正式指定和验证多线程程序的原子性属性。 预计开发的原子性检查器将 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.