Software Transactional Memory on Relaxed Memory Models

DOI10.1007/978-3-642-02658-4_26MaRDI QIDQ3636871zbMATH OpenOpenAlexFDO

Authors Vasu Singh, Rachid Guerraoui, Thomas A. Henzinger

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_26

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of STM on relaxed memory models
• Software transactional memory
• Checking opacity and durable opacity with FDR
• Towards formally specifying and verifying transactional memory
• Effective abstractions for verification under relaxed memory models

Cited in

(14)

• A model of dynamic separation for transactional memory
• Model checking transactional memories
• A framework for formally verifying software transactional memory algorithms
• Remote Transaction Commit: Centralizing Software Transactional Memory Commits
• Mending fences with self-invalidation and self-downgrade
• Verification of STM on relaxed memory models
• Weak atomicity for the x86 memory consistency model
• Towards formally specifying and verifying transactional memory
• The Cost of Privatization in Software Transactional Memory
• Privatization techniques for software transactional memory
• Operational semantics of a weak memory model with channel synchronization
• Operational semantics of a weak memory model with channel synchronization
• Extensible transactional memory testbed
• Versioned boxes as the basis for memory transactions

Describes a project that uses

Uses Software

• Checkfence

This page was built for publication: Software Transactional Memory on Relaxed Memory Models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3636871)