ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer 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.

OriginalsprogEngelsk
TitelProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Antal sider10
UdgivelsesstedNew York, NY, USA
ForlagAssociation for Computing Machinery
Udgivelsesår2018
Sider442-451
ISBN (trykt)978-1-4503-5583-4
ISBN (Elektronisk)9781450355834, 9781450355834
DOI
StatusUdgivet - 2018
BegivenhedAnnual ACM/IEEE Symposium on Logic in Computer Science - University of Oxford, Oxford, Storbritannien
Varighed: 9 jul. 201812 jul. 2018
Konferencens nummer: 33
http://lics.siglog.org/lics18/

Konference

KonferenceAnnual ACM/IEEE Symposium on Logic in Computer Science
Nummer33
LokationUniversity of Oxford
LandStorbritannien
ByOxford
Periode09/07/201812/07/2018
Internetadresse
SerietitelAnnual Symposium on Logic in Computer Science
Nummer33
ISSN1043-6871

    Forskningsområder

  • Iris, Separation logic, atomicity, fine-grained concurrency, logical relations

Se relationer på Aarhus Universitet Citationsformater

ID: 138166894