Cooperability: A new property for multithreading

Multithreading is a prominent technique that enables software to effectively utilize multiple cores on modern hardware. Unfortunately, multithreading is challenging to use properly, as problems like race conditions and atomicity violations are easy to create yet difficult to find and fix. These anomalies are all due to unintended thread interference, in which the actions of one thread are influenced in an unexpected way by the actions of another thread. The typical result of unintended thread interference is unreliable software that is prone to exhibit irreproducible errors.;We present an approach in which all program points susceptible to thread interference are documented with a lightweight specification called a yield annotation. This correctness property is called cooperability. Cooperability guarantees that a program's behavior under a preemptive scheduler (context switching at any program point) is equivalent to that under a cooperative scheduler (context switching only at yields).;With this approach, the hard problem of determining multithreaded program correctness decomposes into two simpler subproblems: • Cooperative correctness. Is the program correct under a cooperative scheduler? • Ensuring cooperability. Are all thread interference points documented via yield? In other words, if a program is correct under a cooperative scheduler, and satisfies cooperability, then the same program is correct under a preemptive scheduler. Hence yield annotations enable cooperative reasoning while preserving runtime behavior.;We demonstrate program analysis techniques to mechanically verify cooperability. These techniques work either at compile time or at runtime. We also describe a tool to automatically infer yield annotations for un-annotated programs.;Cooperative correctness is much simpler than the original correctness problem. The use of a cooperative scheduler allows us to leverage these desirable properties: • Sequential reasoning is correct by default, except at yields. • Yields are the only place to examine for unintended thread interference.;Experimental results on standard benchmarks demonstrate that the number of yield annotations required is quite low -- just 13 yields per thousand lines of code. Yields can help find concurrency bugs: over our benchmarks, unintended yields identify known race conditions and atomicity violations. Finally, a preliminary user study shows that yield annotations are correlated with a statistically significant improvement in the ability of programmers to identify concurrency bugs.