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.
|School:||University of California, Santa Cruz|
|School Location:||United States -- California|
|Source:||DAI-B 73/06, Dissertation Abstracts International|
|Keywords:||Concurrency, Cooperability, Multithreading, Parallelism|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be