Verifying correctness of persistent concurrent data structures

DOI10.1007/978-3-030-30942-8_12zbMATH Open1539.68084MaRDI QIDQ6535948FDOQ6535948

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

Publication date: 14 March 2024

Recommendations

• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Defining and verifying durable opacity: correctness for persistent software transactional memory
• Modularising verification of durable opacity
• Robust shared objects for non-volatile main memory
• The limits of helping in non-volatile memory data structures

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Forward and backward simulations. I. Untimed Systems
• An integrated specification and verification technique for highly concurrent data structures
• Tentative steps toward a development method for interfering programs
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Making Linearizability Compositional for Partially Ordered Executions
• Library abstraction for C/C++ concurrency
• A sound and complete proof technique for linearizability of concurrent data structures
• Verification of Concurrent Programs on Weak Memory Models
• Proving opacity of a pessimistic STM

This page was built for publication: Verifying correctness of persistent concurrent data structures

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