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
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (3)
Uses Software
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