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.
['Ralf Jung', 'David Swasey', 'Filip Sieczkowski', 'Kasper Svendsen', 'Aaron Turon', 'Lars Birkedal', 'Derek Dreyer']
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning