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 society’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. Also see the RoadRunner Project.

People

Cormac Flanagan, University of California at Santa Cruz

Stephen Freund, Williams College

Tim Disney, University of California at Santa Cruz

Caitlin Sadowski, University of California at Santa Cruz

Jaeheon Yi, University of California at Santa Cruz

Papers

Types for Precise Thread Interference.   Jaeheon Yi, Tim Disney, Stephen N. Freund, Cormac Flanagan. UCSC Tech Report (UCSC-SOE-11-22), 2011.

Cooperative Reasoning for Preemptive Execution.   Jaeheon Yi, Caitlin Sadowski, Cormac Flanagan. Symposium on Principles and Practice of Parallel Programming (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. Workshop on Types in Language Design and Implementation (TLDI), 2010.