Dan Frumin ; Robbert Krebbers ; Lars Birkedal - ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

lmcs:6598 - Logical Methods in Computer Science, July 21, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:9)2021
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

Authors: Dan Frumin ; Robbert Krebbers ; Lars Birkedal

    We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines a program $e'$ at type $\tau$. ReLoC provides type-directed structural rules and symbolic execution rules in separation-logic style for manipulating the judgment, whereas in prior work on refinements for languages with higher-order state and concurrency, such proofs were carried out by unfolding the judgment into its definition in the model. ReLoC's abstract proof rules make it simpler to carry out refinement proofs, and enable us to generalize the notion of logically atomic specifications to the relational case, which we call logically atomic relational specifications. We build ReLoC on top of the Iris framework for separation logic in Coq, allowing us to leverage features of Iris to prove soundness of ReLoC, and to carry out refinement proofs in ReLoC. We implement tactics for interactive proofs in ReLoC, allowing us to mechanize several case studies in Coq, and thereby demonstrate the practicality of ReLoC. ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a new Coq mechanization, and support for Iris's prophecy variables. The latter allows us to carry out refinement proofs that involve reasoning about the program's future. We also expand ReLoC's notion of logically atomic relational specifications with a new flavor based on the HOCAP pattern by Svendsen et al.

    Volume: Volume 17, Issue 3
    Published on: July 21, 2021
    Accepted on: June 5, 2021
    Submitted on: June 25, 2020
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.1,D.2.4
    Fundings :
      Source : OpenAIRE Graph
    • Sovereign: A Framework for Modular Formal Verification of Safety Critical Software; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 13563

    3 Documents citing this article

    Consultation statistics

    This page has been seen 686 times.
    This article's PDF has been downloaded 168 times.