Sciweavers

POPL
2015
ACM

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

7 years 11 months ago
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...
Ralf Jung 0002, David Swasey, Filip Sieczkowski, K
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Ralf Jung 0002, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
Comments (0)