Research on Cooperability
Research Overview
Shared memory and threads is the dominant programming model for multicore machines. Programs written in this paradigm take advantage of multicores by using a preemptive scheduler, which allows unrestricted context switches at any program point. However, reasoning about all possible thread interleavings has proven to be a brittle semantic foundation for our s software infrastructure.
We propose cooperability as a better semantic foundation for this paradigm: a program is cooperable if, by adding appropriate yield annotations, we can reason about all thread interleavings by using a cooperative scheduler, which context-switches at only these yield annotations. The program runs just as before, with a preemptive scheduler; the difference is that the yield annotations in a cooperable program simplify where to consider adversarial thread interference. Recent work indicates that the number of program points to consider for thread interference drops by at least an order of magnitude, compared to preemptive semantics and atomic semantics.
Several analysis projects are underway, including static and dynamic
analyses that both check and infer for this program property. As part
of this work, we continue to develop and maintain the
RoadRunner Dynamic Analysis Framework, which is
available here.
Project Members
- Cormac Flanagan, Unversity of California, Santa Cruz (PI)
- Stephen N. Freund, Williams College (PI)
- Parker Finch, Williams College
- Antal Spector-Zabusky, Williams College (now at University of Pennsylvania)
- James Wilcox, Williams College (now at University of Washington)
- Jaeheon Yi, Unversity of California, Santa Cruz (now at Google)
- Caitlin Sadowski, Unversity of California, Santa Cruz (now at Google)
- Tom Austin, Unversity of California, Santa Cruz (now at San Jose State)
- Tim Disney, Unversity of California, Santa Cruz
Papers
-
Using Escape Analysis in Dynamic Data Race Detection
Emma Harrington and Stephen N. Freund
Williams College Technical Report CSTR201401, 2014.
Poster presented at GHC 2014.
-
RedCard: Redundant Check Elimination For Dynamic Race Detectors
Cormac Flanagan and Stephen N. Freund
European Conference on Object-Oriented Programming, 2013.
(Best Paper Award)
-
Types for Precise Thread Interference
Jaeheon Yi, Tim Disney, Stephen N. Freund, Cormac Flanagan
ACM International Symposium on Software Testing and Analysis, 2012.
-
Faceted Execution of Policy-Agnostic Programs
Thomas H. Austin, Jean Yang, Cormac Flanagan, Armando Solar-Lezama
PLAS, 2012.
-
A Functional View of Imperative Information Flow
Thomas H. Austin, Cormac Flanagan, and Martin Abadi
APLAS, 2012.
-
Detecting Inconsistencies via Universal Reachability Analysis
Aaron Tomb, Cormac Flanagan
ACM International Symposium on Software Testing and Analysis, 2012.
-
Multiple Facets for Dynamic Information Flow
Thomas H. Austin, Cormac Flanagan
POPL 2012
-
Sound Predictive Race Detection in Polynomial Time
Yannis Smaragdakis, Jacob M. Evans, Caitlin Sadowski, Jaeheon Yi, Cormac Flanagan
POPL 2012
-
Types for Precise Thread Interference
Jaeheon Yi, Tim Disney, Stephen N. Freund, Cormac Flanagan
ISSTA 2012
(earlier version: UCSC Tech Report (UCSC-SOE-11-22))
-
Virtual Values for Language Extension
Thomas H. Austin, Tim Disney, Cormac Flanagan
OOPSLA 2011
-
Cooperative Concurrency for a Multicore World (invited talk)
Jaeheon Yi, Caitlin Sadowski, Stephen N. Freund, Cormac Flanagan
RV 2011
-
Cooperative Reasoning for Preemptive Execution
Jaeheon Yi, Caitlin Sadowski, Cormac Flanagan
PPoPP 2011
-
Applying Usability Studies to Correctness Conditions: A Case Study of Cooperability
Caitlin Sadowski and Jaeheon Yi
Onward! Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), 2010
-
Effects for Cooperable and Serializable Threads
Jaeheon Yi and Cormac Flanagan
TLDI 2010
Support
This material is based upon work supported by the National Science
Foundation under Grants No. 1116883 and 1116825.
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.