Research on Atomicity

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 are currently pursuing several analysis techniques for checking atomicity properties, include static analyses based on type checking and type inference, as well as dynamic (run-time) approaches.

People

We have also collaborated on some aspects of this work with other colleagues, including Edwin Rodríguez, Matthew Dwyer, John Hatcliff, Gary T. Leavens, and Robby.

Papers

Extended Talks

Earlier Work on Race Conditions

Funding

This material is based upon work supported by the National Science Foundation under Grant No. 0341179 and Grant No. 0341387 and by a Fellowship from the Sloan Foundation. 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.