Towards formally specifying and verifying transactional memory
From MaRDI portal
(Redirected from Publication:470040)
Recommendations
Cites work
- scientific article; zbMATH DE number 4110131 (Why is no real title available?)
- An axiomatic proof technique for parallel programs
- Completeness and Nondeterminism in Model Checking Transactional Memories
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- 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
- Nested transactional memory: Model and architecture sketches
- Nonblocking Algorithms and Backward Simulation
- Software Transactional Memory on Relaxed Memory Models
- The serializability of concurrent database updates
- Towards formally specifying and verifying transactional memory
- Transactional Memory: Glimmer of a Theory
- Verifying concurrent data structures by simulation
Cited in
(30)- Non-interference and local correctness in transactional memory
- Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
- Formal stystems specification. The RPC-memory specification case study
- Correctness of concurrent executions of closed nested transactions in transactional memory systems
- Correctness of an STM Haskell implementation
- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
- Checking opacity and durable opacity with FDR
- On the correctness problem for serializability
- A Model of Dynamic Separation for Transactional Memory
- Characterizing Transactional Memory Consistency Conditions Using Observational Refinement
- Defining and verifying durable opacity: correctness for persistent software transactional memory
- Completeness and Nondeterminism in Model Checking Transactional Memories
- Proving opacity of transactional memory with early release
- An Abort-Aware Model of Transactional Programming
- Model checking transactional memories
- scientific article; zbMATH DE number 1693446 (Why is no real title available?)
- A programming language perspective on transactional memory consistency
- On the liveness of transactional memory
- Mechanized proofs of opacity: a comparison of two techniques
- A framework for formally verifying software transactional memory algorithms
- Towards formally specifying and verifying transactional memory
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Last-use opacity: a strong safety property for transactional memory with prerelease support
- Verification of STM on relaxed memory models
- Software Transactional Memory on Relaxed Memory Models
- The semantics of progress in lock-based transactional memory
- Proving Isolation Properties for Software Transactional Memory
- A verified durable transactional mutex lock for persistent x86-TSO
- Verifying opacity of a transactional mutex lock
- scientific article; zbMATH DE number 7577571 (Why is no real title available?)
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)
