Verifying correctness of persistent concurrent data structures

DOI10.1007/978-3-030-30942-8_12MaRDI QIDQ6535948zbMATH OpenFDO

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

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_12

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)

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

Cites work

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

Cited in

(2)

• Modularising verification of durable opacity
• Vorpal

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)