Verifying opacity of a transactional mutex lock
DOI10.1007/978-3-319-19249-9_11zbMATH Open1427.68190OpenAlexW1560394043MaRDI QIDQ5206950FDOQ5206950
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
Recommendations
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- The serializability of concurrent database updates
- Software transactional memory
- Towards formally specifying and verifying transactional memory
- Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)
- Modular Safety Checking for Fine-Grained Concurrency
- Transactional Memory: Glimmer of a Theory
- A programming language perspective on transactional memory consistency
- Model checking transactional memories
- A sound and complete proof technique for linearizability of concurrent data structures
- Transactional mutex locks
Cited In (10)
- Proving opacity via linearizability: a sound and complete method
- Title not available (Why is that?)
- Checking opacity and durable opacity with FDR
- Title not available (Why is that?)
- 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
- Modularising opacity verification for hybrid transactional memory
- Defining and verifying durable opacity: correctness for persistent software transactional memory
- Proving opacity of a pessimistic STM
Uses Software
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)
