Impredicative Concurrent Abstract Predicates

by Kasper Svendsen and Lars Birkedal

Impredicative concurrent abstract predicates – iCAP – a program logic for modular reasoning about concurrent, higher-order, reentrant, imperative code. Building on earlier work, iCAP uses protocols to reason about shared mutable state. A key novel feature of iCAP is the ability to define impredicative protocols; protocols that are parameterized on arbitrary predicates, including predicates that themselves refer to protocols. We demonstrate the utility of impredicative protocols through a series of examples, including the specification and verification, in the logic, of a spin-lock, a reentrant event loop, and a concurrent bag implemented using cooperation, against modular specifications.

Paper (ESOP 2014) | Appendix | Technical report