Towards formally specifying and verifying transactional memory

DOI10.1007/s00165-012-0225-8zbMath1298.68168OpenAlexW2035134754MaRDI QIDQ470040

Victor Luchangco, Simon Doherty, Lindsay Groves, Mark Moir

Publication date: 11 November 2014

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-012-0225-8

zbMATH Keywords

verificationformal specificationrefinementtransactional memoryI/O automationsimulation proof

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

On the correctness problem for serializability, Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory, Last-use opacity: a strong safety property for transactional memory with prerelease support, Mechanized proofs of opacity: a comparison of two techniques, Correctness of concurrent executions of closed nested transactions in transactional memory systems, Checking opacity and durable opacity with FDR, Proving opacity of transactional memory with early release, Towards formally specifying and verifying transactional memory, Unnamed Item, Verifying Opacity of a Transactional Mutex Lock

Uses Software

• NOrec

Cites Work

• Unnamed Item
• Unnamed Item
• Towards formally specifying and verifying transactional memory
• Nested transactional memory: Model and architecture sketches
• An axiomatic proof technique for parallel programs
• Forward and backward simulations. I. Untimed Systems
• High-level small-step operational semantics for transactions
• Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
• Completeness and Nondeterminism in Model Checking Transactional Memories
• Transactional Memory: Glimmer of a Theory
• Software Transactional Memory on Relaxed Memory Models
• Nonblocking Algorithms and Backward Simulation
• The serializability of concurrent database updates
• Formal Techniques for Networked and Distributed Systems – FORTE 2004