Verification of STM on relaxed memory models
From MaRDI portal
Recommendations
Cites work
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Atomizer: A dynamic atomicity checker for multithreaded programs
- Completeness and Nondeterminism in Model Checking Transactional Memories
- Computer Aided Verification
- Computer Aided Verification
- Effective Program Verification for Relaxed Memory Models
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
- Relaxed memory models
- Software Transactional Memory on Relaxed Memory Models
- Software transactional memory
- The Java memory model
- The serializability of concurrent database updates
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(9)- A Versatile STM Protocol with Invisible Read Operations That Satisfies the Virtual World Consistency Condition
- 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
- A framework for formally verifying software transactional memory algorithms
- Mending fences with self-invalidation and self-downgrade
- Weak atomicity for the x86 memory consistency model
- Automatic verification of RMA programs via abstraction extrapolation
- Effective abstractions for verification under relaxed memory models
Describes a project that uses
Uses Software
This page was built for publication: Verification of STM on relaxed memory models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q453508)
