The Essence of Higher-Order Concurrent Separation Logic

Robbert Krebbers*, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal

*Corresponding author for this work

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

61 Citations (Scopus)

Abstract

Concurrent separation logics (CSLs) have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids (PCMs) and invariants. However, the realization of these concepts in Iris still bakes in several complex mechanisms—such as weakest preconditions and mask-changing view shifts—as primitive notions. In this paper, we take the Iris story to its (so to speak) logical conclusion, applying the reductionist methodology of Iris to Iris itself. Specifically, we define a small, resourceful base logic, which distills the essence of Iris: it comprises only the assertion layer of vanilla separation logic, plus a handful of simple modalities. We then show how the much fancier logical mechanisms of Iris—in particular, its entire program specification layer—can be understood as merely derived forms in our base logic. This approach helps to explain the meaning of Iris’s program specifications at a much higher level of abstraction than was previously possible. We also show that the step-indexed “later” modality of Iris is an essential source of complexity, in that removing it leads to a logical inconsistency. All our results are fully formalized in the Coq proof assistant.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication26th European Symposium on Programming, ESOP 2017 - Proceedings
EditorsHongseok Yang
Place of PublicationBerlin
PublisherSpringer
Pages696-723
Number of pages28
ISBN (Electronic)978-3-662-54434-1
ISBN (Print)978-3-662-54433-4
DOIs
Publication statusPublished - 2017
EventESOP 2017: 26th European Symposium on Programming - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017
Conference number: 26

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10201 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceESOP 2017
Country/TerritorySweden
CityUppsala
Period22/04/1729/04/17
OtherHeld as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017

Fingerprint

Dive into the research topics of 'The Essence of Higher-Order Concurrent Separation Logic'. Together they form a unique fingerprint.

Cite this