Verifying opacity of a transactional mutex lock

DOI10.1007/978-3-319-19249-9_11MaRDI QIDQ5206950zbMATH OpenOpenAlexFDO

Authors John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim

Publication date 19 December 2019

Published in FM 2015: Formal Methods (Search for Journal in Brave)

Full work available at URL http://bura.brunel.ac.uk/handle/2438/11265

Mathematics Subject Classification ID

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

• Mechanized proofs of opacity: a comparison of two techniques
• Proving opacity via linearizability: a sound and complete method
• Modularising opacity verification for hybrid transactional memory
• Proving opacity of a pessimistic STM
• Value-based or conflict-based? Opacity definitions for STMs

Cites work

• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• A programming language perspective on transactional memory consistency
• A sound and complete proof technique for linearizability of concurrent data structures
• Model checking transactional memories
• Modular Safety Checking for Fine-Grained Concurrency
• Software transactional memory
• The serializability of concurrent database updates
• Towards formally specifying and verifying transactional memory
• Transactional Memory: Glimmer of a Theory
• Transactional mutex locks
• Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)

Cited in

(10)

• Proving opacity via linearizability: a sound and complete method
• Checking opacity and durable opacity with FDR
• Modularising opacity verification for hybrid transactional memory
• Defining and verifying durable opacity: correctness for persistent software transactional memory
• Proving opacity of transactional memory with early release
• Mechanized proofs of opacity: a comparison of two techniques
• Value-based or conflict-based? Opacity definitions for STMs
• Proving opacity of a pessimistic STM
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• scientific article; zbMATH DE number 7577571 (Why is no real title available?)

Describes a project that uses

Uses Software

• KIV

This page was built for publication: Verifying opacity of a transactional mutex lock

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