A framework for formally verifying software transactional memory algorithms

DOI10.1007/978-3-642-32940-1_36MaRDI QIDQ2912700zbMATH OpenOpenAlexFDO

Authors Mohsen Lesani, Victor Luchangco, Mark Moir

Publication date 25 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-32940-1_36

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Towards formally specifying and verifying transactional memory
• Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
• Proving opacity of a pessimistic STM
• Software Transactional Memory on Relaxed Memory Models
• Verification of STM on relaxed memory models

Cited in

(10)

• Towards formally specifying and verifying transactional memory
• Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
• Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
• Proving Isolation Properties for Software Transactional Memory
• scientific article; zbMATH DE number 7577571 (Why is no real title available?)
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Checking opacity and durable opacity with FDR
• An analytic framework for performance modeling of software transactional memory
• Mechanized proofs of opacity: a comparison of two techniques
• Model checking transactional memories

Describes a project that uses

Uses Software

• PVS

This page was built for publication: A framework for formally verifying software transactional memory algorithms

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