The widespread adoption of multicore processors requires multithreaded software to exploit these hardware resources. Unfortunately, the construction and validation of reliable concurrent software currently requires extraordinary effort, due to unanticipated interactions between concurrent threads. Thus, developing better programming techniques and tools for concurrent programming is essential. This research develops a cooperative programming methodology for multithreaded software, based on the philosophy that all thread interference must be explicitly documented via source-level "yield" annotations by the programmer.
The project will investigate both static and dynamic checking techniques to verify the correctness of yield annotations. Once verified, these annotations guarantee that code executed between successive yields is serializable and thus amenable to sequential reasoning. Moreover, yield-free code is deterministic. Despite provided these strong safety guarantees, this methodology does not impact program performance. The cooperative methodology provides a robust foundation for multithreaded software and can potentially transform the principles and practices of multithreaded software engineering. This work on cooperability will also provide research opportunities for graduate and undergraduate students, and it will support endeavors to provide access to science education for all students.
