Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

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.