Verifying Opacity of a Transactional Mutex Lock

DOI10.1007/978-3-319-19249-9_11zbMath1427.68190OpenAlexW1560394043MaRDI QIDQ5206950

John Derrick, Gerhard Schellhorn, Oleg Travkin, Brijesh Dongol, 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)

Related Items (5)

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ Checking opacity and durable opacity with FDR ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• KIV

Cites Work

• Unnamed Item
• Unnamed Item
• Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)
• Towards formally specifying and verifying transactional memory
• Model checking transactional memories
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
• Transactional Mutex Locks
• Modular Safety Checking for Fine-Grained Concurrency
• Transactional Memory: Glimmer of a Theory
• The serializability of concurrent database updates
• Software transactional memory
• A programming language perspective on transactional memory consistency

This page was built for publication: Verifying Opacity of a Transactional Mutex Lock