Model checking transactional memories

DOI10.1007/s00446-009-0092-6zbMath1267.68143OpenAlexW2077571050MaRDI QIDQ2377134

Thomas A. Henzinger, Rachid Guerraoui, Vasu Singh

Publication date: 28 June 2013

Published in: Distributed Computing (Search for Journal in Brave)

Full work available at URL: https://infoscience.epfl.ch/record/117513/files/PLDI_paper.pdf

zbMATH Keywords

model checkingtransactional memories

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (7)

On the correctness problem for serializability ⋮ Formal verification of mobile robot protocols ⋮ Perspectives on Transactional Memory ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ Checking opacity and durable opacity with FDR ⋮ Completeness and Nondeterminism in Model Checking Transactional Memories ⋮ Verifying Opacity of a Transactional Mutex Lock

Uses Software

• Checkfence
• Antichains

Cites Work

• Unnamed Item
• Reasoning about networks with many identical finite state processes
• Maximal serializability of iterated transactions
• Model-checking of correctness conditions for concurrent objects
• 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
• Propositional dynamic logic of looping and converse is elementarily decidable
• The serializability of concurrent database updates
• Toward a theory of transactional contention managers
• Randomized wait-free concurrent objects (extended abstract)
• Computer Aided Verification
• Software transactional memory
• Antichains: A New Algorithm for Checking Universality of Finite Automata

This page was built for publication: Model checking transactional memories