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...

• Type: Journal
• Year: 2011
• Where: PPOPP
• Authors: Jaeheon Yi, Caitlin Sadowski, Cormac Flanagan
• Keywords: Analysis Algorithms, Distributed And Parallel Computing, Legacy Software, PPOPP 2011, Sequential Reasoning