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

UPMARC 2014 Summer School: Analysis Techniques to Detect Concurrency Errors

Papers

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.