Cooperative reasoning for preemptive execution

12 years 2 months ago
Cooperative reasoning for preemptive execution
We propose a cooperative methodology for multithreaded software, where threads use traditional synchronization idioms such as locks, but additionally document each point of potential thread interference with a “yield” annotation. Under this methodology, code between two successive yield annotations forms a serializable transaction that is amenable to sequential reasoning. This methodology reduces the burden of reasoning about thread interleavings by indicating only those interference points that matter. We present experimental results showing that very few yield annotations are required, typically one or two per thousand lines of code. We also present dynamic analysis algorithms for detecting cooperability violations, where thread interference is not documented by a yield, and for yield annotation inference for legacy software. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs–specification techniqu...
Jaeheon Yi, Caitlin Sadowski, Cormac Flanagan
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Authors Jaeheon Yi, Caitlin Sadowski, Cormac Flanagan
Comments (0)