Defining and verifying durable opacity: correctness for persistent software transactional memory

DOI10.1007/978-3-030-50086-3_3MaRDI QIDQ5041273zbMATH OpenOpenAlexFDO

Authors Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Publication date 13 October 2022

Published in Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2004.08200

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Checking opacity and durable opacity with FDR
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Value-based or conflict-based? Opacity definitions for STMs
• Proving opacity of a pessimistic STM
• Verifying opacity of a transactional mutex lock

Cites work

• Forward and backward simulations. I. Untimed Systems
• scientific article; zbMATH DE number 1301859 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• Mechanized proofs of opacity: a comparison of two techniques
• Modularising opacity verification for hybrid transactional memory
• Proving opacity of a pessimistic STM
• Proving opacity via linearizability: a sound and complete method
• Towards formally specifying and verifying transactional memory
• Transactional Memory: Glimmer of a Theory
• Transactional mutex locks
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Verifying opacity of a transactional mutex lock

Cited in

(7)

• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Modularising verification of durable opacity
• Vorpal
• Checking opacity and durable opacity with FDR
• Verifying correctness of persistent concurrent data structures
• A verified durable transactional mutex lock for persistent x86-TSO
• Proving opacity of transactional memory with early release

Describes a project that uses

Uses Software

• NOrec

This page was built for publication: Defining and verifying durable opacity: correctness for persistent software transactional memory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5041273)