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 Rodriguez, Matthew Dwyer, John Hatcliff, Gary T. Leavens, and Robby.
Papers
- Adversarial
Memory for Detecting Destructive Races
Cormac Flanagan and Stephen N. Freund
ACM Symposium on Principles of Programming Languages, 2010.
- The
RoadRunner Dynamic Analysis Framework for Concurrent Programs
Cormac Flanagan and Stephen N. Freund
ACM Workshop on Program Analysis for Software Tools and Engineering,
2010.
- Effects
for Cooperable and Serializable Threads
Jaeheon Yi and Cormac Flanagan
ACM Workshop on Types in Language Design and Implementation, 2010.
- FastTrack:
Efficient and Precise Dynamic Race Detection
Cormac Flanagan and Stephen N. Freund
ACM Symposium on Principles of Programming Languages, 2009.
- SingleTrack:
A Dynamic Determinism Checker for Multithreaded Programs
Caitlin Sadowski, Stephen N. Freund, and Cormac Flanagan
European Symposium on Programming, 2009.
- Velodrome:
A Sound and Complete Dynamic Analysis for Atomicity
Cormac Flanagan and Stephen N. Freund
ACM Symposium on Principles of Programming Languages, 2008.
- Types
for Atomicity: Static Checking and Inference for Java (appendix)
Cormac Flanagan, Stephen N. Freund, Marina Lifshin, and Shaz Qadeer.
ACM Transactions on Programming Languages and Systems, 2008.
- Proving
correctness of a dynamic atomicity analysis in Coq
Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, and Cormac Flanagan
Third Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, 2008.
- Atomizer:
A Dynamic Atomicity Checker for Multithreaded Programs
Cormac Flanagan and Stephen N. Freund
Science of Computer Programming, 2008.
- Type
Inference Against Races
Cormac Flanagan and Stephen N. Freund
Science of Computer Programming, 2007.
- Types
for Safe Locking: Static Race Detection for Java
Martin Abadi, Cormac Flanagan, and Stephen N. Freund
ACM Transactions on Programming Languages and Systems, 2006.
- Dynamic
Architecture Extraction
Cormac Flanagan and Stephen N. Freund
Formal Approaches to Testing and Runtime Verification, 2006.
- Automatic
Synchronization Correction
Cormac Flanagan and Stephen N. Freund
Workshop on Synchronization and Concurrency in Object-Oriented
Languages, October 2005.
- Type
Inference for Atomicity
Cormac Flanagan, Stephen N. Freund, and Marina Lifshin
ACM Workshop on Types in Language Design and Implementation, 2005.
- Dynamic
Partial-Order Reduction for Model Checking Software
Cormac Flanagan and Patrice Godefroid
Principles of Programming Languages, 2005.
- Modular
Verification of Multithreaded Programs
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer,
and Sanjit A. Seshia.
Theoretical Computer Science, 338 (1-3), June 2005.
- Exploiting
Purity for Atomicity
Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer
ACM International Symposium on Software Testing and Analysis, July
2004.
Extended
journal version appeared in IEE Transactions on Software
Engineering
Additional details and correctness proofs are in Williams College
Technical
Note 04-05, July 2004.
- Extending
JML for Modular Specification and Verification of Multi-Threaded
Programs
Edwin Rodriguez, Matthew Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, and Robby
European Conference on Object-Oriented Programming, July 2005.
- Type
Inference for Atomicity
Cormac Flanagan, Stephen N. Freund and Marina Lifshin.
Types in Language Design and Implementation, January 2005.
- Type
Inference Against Races
Cormac Flanagan and Stephen N. Freund
Static Analysis Symposium, August, 2004.
Extended paper available as Williams College
Technical
Note 04-06, Sept. 2004.
- Partial
Type And Effect Inference for Rcc/Java in NP-Complete
Cormac Flanagan and Stephen
N. Freund
Williams College Technical Note 04-01,
Feb 2004.
- Checking
Concise Specifications For Multithreaded
Software
Stephen N. Freund and Shaz Qadeer
Journal of Object Technology, 2004.
Extended paper available as Williams College
Technical
Note 02-01, Dec. 2002.
- Verifying
Commit-Atomicity using Model-Checking
Cormac Flanagan
SPIN Workshop on Model Checking of Software, 2004.
- Atomizer:
A Dynamic Atomicity Checker for Multithreaded Programs
Cormac Flanagan and Stephen N. Freund
ACM Symposium on Principles of Programming Languages, 2004.
- Transactions
for Software Model Checking
Cormac Flanagan and Shaz Qadeer
Workshop on Software Model Checking, 2003.
- Checking
Concise Specifications for Multithreaded Software
Stephen N. Freund and Shaz Qadeer
Workshop on Formal Techniques for Java-like Programs, 2003.
- A Type and
Effect System for Atomicity
Cormac Flanagan and Shaz Qadeer
ACM Conference on Programming Language Design and Implementation, 2003.
- Types for
Atomicity
Cormac Flanagan and Shaz Qadeer
ACM Workship on Types in Language Design
and Implementation, 2003.
- Thread-Modular
Verification for Shared-Memory Programs
Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer
SRC Technical Note 2001-003, November 2001.
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.