ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

DOI

  • Dan Frumin, Radboud University
  • ,
  • Robbert Krebbers, Delft University of Technology
  • ,
  • Lars Birkedal

We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of our logic is a judgement e ≲ e': , which expresses that a program e refines a program e' at type . In contrast to earlier work on refinements for languages with higher-order state and concurrency, ReLoC provides type- and structure-directed rules for manipulating this judgement, whereas previously, such proofs were carried out by unfolding the judgement into its definition in the model. These more abstract proof rules make it simpler to carry out refinement proofs. Moreover, we introduce logically atomic relational specifications: a novel approach for relational specifications for compound expressions that take effect at a single instant in time. We demonstrate how to formalise and prove such relational specifications in ReLoC, allowing for more modular proofs. ReLoC is built on top of the expressive concurrent separation logic Iris, allowing us to leverage features of Iris such as invariants and ghost state. We provide a mechanisation of our logic in Coq, which does not just contain a proof of soundness, but also tactics for interactively carrying out refinements proofs. We have used these tactics to mechanise several examples, which demonstrates the practicality and modularity of our logic.

Original languageEnglish
Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Number of pages10
Place of publicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication year2018
Pages442-451
ISBN (print)978-1-4503-5583-4
ISBN (Electronic)9781450355834, 9781450355834
DOIs
Publication statusPublished - 2018
EventAnnual ACM/IEEE Symposium on Logic in Computer Science - University of Oxford, Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018
Conference number: 33
http://lics.siglog.org/lics18/

Conference

ConferenceAnnual ACM/IEEE Symposium on Logic in Computer Science
Nummer33
LocationUniversity of Oxford
LandUnited Kingdom
ByOxford
Periode09/07/201812/07/2018
Internetadresse
SeriesAnnual Symposium on Logic in Computer Science
Number33
ISSN1043-6871

    Research areas

  • Atomicity, Fine-grained concurrency, Iris, Logical relations, Separation logic

See relations at Aarhus University Citationformats

ID: 138166894