Verification of STM on relaxed memory models

DOI10.1007/s10703-011-0131-3zbMath1247.68165OpenAlexW2067647017MaRDI QIDQ453508

Vasu Singh, Thomas A. Henzinger, Rachid Guerraoui

Publication date: 27 September 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: http://infoscience.epfl.ch/record/178042

zbMATH Keywords

model checkingrelaxed memory modelstransactional memories

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Unnamed Item

Uses Software

• Zing
• SPIN
• Atomizer
• Velodrome
• Checkfence
• Goldilocks
• Antichains
• FastTrack

Cites Work

• Atomizer: A dynamic atomicity checker for multithreaded programs
• Effective Program Verification for Relaxed Memory Models
• 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
• The serializability of concurrent database updates
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Relaxed memory models
• The Java memory model
• Computer Aided Verification
• Computer Aided Verification
• Software transactional memory
• Tools and Algorithms for the Construction and Analysis of Systems
• Antichains: A New Algorithm for Checking Universality of Finite Automata