Towards formally specifying and verifying transactional memory
DOI10.1007/S00165-012-0225-8zbMATH Open1298.68168OpenAlexW2035134754MaRDI QIDQ470040FDOQ470040
Authors: Simon Doherty, Lindsay Groves, Victor Luchangco, 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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Forward and backward simulations. I. Untimed Systems
- Title not available (Why is that?)
- The serializability of concurrent database updates
- An axiomatic proof technique for parallel programs
- Towards formally specifying and verifying transactional memory
- Nested transactional memory: Model and architecture sketches
- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
- Completeness and Nondeterminism in Model Checking Transactional Memories
- Software Transactional Memory on Relaxed Memory Models
- Verifying concurrent data structures by simulation
- High-level small-step operational semantics for transactions
- Transactional Memory: Glimmer of a Theory
- Nonblocking Algorithms and Backward Simulation
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
Cited In (30)
- Correctness of concurrent executions of closed nested transactions in transactional memory systems
- Towards formally specifying and verifying transactional memory
- Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
- Completeness and Nondeterminism in Model Checking Transactional Memories
- Software Transactional Memory on Relaxed Memory Models
- Proving Isolation Properties for Software Transactional Memory
- A framework for formally verifying software transactional memory algorithms
- Title not available (Why is that?)
- Formal verification of a C-like memory model and its uses for verifying program transformations
- A Model of Dynamic Separation for Transactional Memory
- On the correctness problem for serializability
- Checking opacity and durable opacity with FDR
- Formal stystems specification. The RPC-memory specification case study
- On the liveness of transactional memory
- Verification of STM on relaxed memory models
- The semantics of progress in lock-based transactional memory
- Non-interference and local correctness in transactional memory
- A programming language perspective on transactional memory consistency
- Characterizing Transactional Memory Consistency Conditions Using Observational Refinement
- Proving opacity of transactional memory with early release
- Title not available (Why is that?)
- Mechanized proofs of opacity: a comparison of two techniques
- Correctness of an STM Haskell implementation
- A verified durable transactional mutex lock for persistent x86-TSO
- Model checking transactional memories
- Verifying opacity of a transactional mutex lock
- Defining and verifying durable opacity: correctness for persistent software transactional memory
- Last-use opacity: a strong safety property for transactional memory with prerelease support
- An Abort-Aware Model of Transactional Programming
Uses Software
This page was built for publication: Towards formally specifying and verifying transactional memory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q470040)
