Cooperative reasoning for preemptive execution

12 years 7 months ago

Download users.soe.ucsc.edu

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–speciﬁcation techniqu...

Jaeheon Yi, Caitlin Sadowski, Cormac Flanagan

Real-time Traffic