Hybrid Atomicity Checking

Stephen N. Freund

Research Overview

Multithreaded programs often exhibit erroneous behavior because of unintended interactions between threads. Much work on this problem has focused on simultaneous-access race conditions, but the absence of race conditions is insufficient to ensure the absence of errors due to unintended thread interactions.

We focus on the more fundamental non-interference property of atomicity. A method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. In other words, for every execution there is an equivalent serial execution in which the actions of the atomic procedure are not interleaved with actions of other threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies formal and informal correctness arguments and subsequent validation activities such as code inspection and testing.

We have previously pursued several analysis techniques for checking atomicity properties, include static analyses based on type checking and type inference, as well as dynamic (run-time) approaches. Our current research develops hybrid checkers that synthesize the best aspects of both techniques without suffering from the limitations of either individual approach.

The impacts of hybrid atomicity checkers, and their integration into a broad educational program, include improved software quality and better software engineering practices. Specifically, hybrid checkers provide a cost-effective mechanism for finding errors resistant to testing, are more usable and scalable than existing tools, and support a design methodology that encourages precisely specifying interactions between threads.

As part of this work, we have designed and released the RoadRunner Dynamic Analysis Framework, which is available here.

Collaborators

Related Projects

Extended Presentations

Support

This material is based upon work supported by the National Science Foundation under Grant No. 0644130. Previous support was provided by the National Science Foundation under Grant No. 0341387.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.