Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

DOI10.1007/978-3-030-50086-3_3OpenAlexW3037775571MaRDI QIDQ5041273

Gerhard Schellhorn, Simon Doherty, Eleni Bila, John Derrick, Brijesh Dongol, 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)

Related Items (3)

Checking opacity and durable opacity with FDR ⋮ Verifying correctness of persistent concurrent data structures: a sound and complete method ⋮ Unnamed Item

Uses Software

• NOrec

Cites Work

• Unnamed Item
• Unnamed Item
• Towards formally specifying and verifying transactional memory
• Mechanized proofs of opacity: a comparison of two techniques
• Forward and backward simulations. I. Untimed Systems
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Transactional Mutex Locks
• Proving Opacity of a Pessimistic {STM}
• Transactional Memory: Glimmer of a Theory
• Modularising Opacity Verification for Hybrid Transactional Memory
• Proving Opacity via Linearizability: A Sound and Complete Method
• Verifying Opacity of a Transactional Mutex Lock

This page was built for publication: Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory