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