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.