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
Papers
-
FastTrack: Efficient and Precise Dynamic Race Detection
Cormac Flanagan and Stephen N. Freund
Communications of the ACM, 2010.
-
Adversarial Memory for Detecting Destructive Races
Cormac Flanagan and Stephen N. Freund
ACM Conference on Programming Language Design and
Implementation, 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.
-
FastTrack: Efficient and Precise Dynamic Race Detection
Cormac Flanagan and Stephen N. Freund
ACM Conference on Programming Language Design and
Implementation, 2009.
-
SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
Caitlin Sadowski, Cormac Flanagan, and Stephen N. Freund
European Symposium on Programming, 2009.
-
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.
-
Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs
Cormac Flanagan and Stephen N. Freund
Science of Computer Programming, 2008.
-
Velodrome: A Sound and Complete Dynamic Analysis for Atomicity
Cormac Flanagan, Stephen N. Freund, and Jaeheon Yi
ACM Conference on Programming Language Design and
Implementation, 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.
-
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and
Dynamic
Kenneth Knowles, Aaron Tomb, Jessica Gronski,
Stephen N. Freund, Cormac Flanagan
Scheme and Functional Programming workshop, 2006
-
Hybrid Types, Invariants, and Refinements for Imperative Objects
Cormac Flanagan, Stephen N. Freund, and Aaron Tomb
FOOL 2006.
-
Dynamic Architecture Extraction
Cormac Flanagan and Stephen N. Freund
Formal Approaches to Testing and Runtime Verification, 2006.
-
Exploiting Purity for Atomicity
Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer
IEEE Transactions on Software Engineering, 2005.
-
Automatic Synchronization Correction
Cormac Flanagan and Stephen N. Freund
Workshop on Synchronization and Concurrency in Object-Oriented Languages, October 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.
-
Type Inference for Atomicity
Cormac Flanagan, Stephen N. Freund, and Marina Lifshin
ACM Workshop on Types in Language Design and Implementation, 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 to appear in
Transactions on Software Engineering
- 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.
- Atomizer: A Dynamic
Atomicity Checker for Multithreaded Programs
Cormac Flanagan and Stephen N. Freund
ACM Symposium on Principles of Programming Languages, 2004.
- Checking
Concise Specifications for Multithreaded Software
Stephen N. Freund and Shaz Qadeer
Workshop on Formal Techniques for Java-like Programs, 2003.
- Thread-Modular
Verification for Shared-Memory Programs
Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer
SRC Technical Note 2001-003, November 2001.
- Detecting
Race Conditions in Large Programs
Cormac Flanagan and Stephen N. Freund
ACM Workshop on Program Analysis for Software Tools and Engineering, 2001.
- Type-Based
Race Detection for Java
Cormac Flanagan and Stephen N. Freund
ACM Conference on Programming Language Design and Implementation, 2000.
- Type-Based Race
Detection for Java (summary)
Cormac Flanagan and Stephen N. Freund
LICS, 2000
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.