Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants enable us to enforce— user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a view shift, Iris supports the encoding of logically atomic specifications, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs Keywords Separation logic, fine-grained concurrency, atomicity, partial commutative monoids, invariants, higher-order logic, compositional veri�...

• Type: Journal
• Year: 2015
• Where: POPL
• Authors: Ralf Jung 0002, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
• Keywords: POPL 2015, Programming Languages