Eleni Bila ; John Derrick ; Simon Doherty ; Brijesh Dongol ; Gerhard Schellhorn et al. - Modularising Verification Of Durable Opacity

lmcs:6941 - Logical Methods in Computer Science, July 28, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:7)2022
Modularising Verification Of Durable OpacityArticle

Authors: Eleni Bila ; John Derrick ; Simon Doherty ; Brijesh Dongol ORCID; Gerhard Schellhorn ; Heike Wehrheim

    Non-volatile memory (NVM), also known as persistent memory, is an emerging paradigm for memory that preserves its contents even after power loss. NVM is widely expected to become ubiquitous, and hardware architectures are already providing support for NVM programming. This has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency and in the development of associated verification approaches. Software transactional memory (STM) is a key programming abstraction that supports concurrent access to shared state. In a fashion similar to linearizability as the correctness condition for concurrent data structures, there is an established notion of correctness for STMs known as opacity. We have recently proposed durable opacity as the natural extension of opacity to a setting with non-volatile memory. Together with this novel correctness condition, we designed a verification technique based on refinement. In this paper, we extend this work in two directions. First, we develop a durably opaque version of NOrec (no ownership records), an existing STM algorithm proven to be opaque. Second, we modularise our existing verification approach by separating the proof of durability of memory accesses from the proof of opacity. For NOrec, this allows us to re-use an existing opacity proof and complement it with a proof of the durability of accesses to shared state.


    Volume: Volume 18, Issue 3
    Published on: July 28, 2022
    Accepted on: May 17, 2022
    Submitted on: December 1, 2020
    Keywords: Computer Science - Distributed, Parallel, and Cluster Computing
    Funding:
      Source : OpenAIRE Graph
    • Verifiably Correct Transactional Memory.; Funder: UK Research and Innovation; Code: EP/R032351/1
    • Verifiably Correct Transactional Memory; Funder: UK Research and Innovation; Code: EP/R032556/1
    • Verifiably Correct Swarm Attestation; Funder: UK Research and Innovation; Code: EP/V038915/1
    • RoboTest: Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots; Funder: UK Research and Innovation; Code: EP/R025134/2

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1983 times.
    This article's PDF has been downloaded 611 times.