Mechanized proofs of opacity: a comparison of two techniques

Publication date 12 September 2018

Recommendations

Cites work

scientific article; zbMATH DE number 1301859 (Why is no real title available?)
A framework for formally verifying software transactional memory algorithms
A programming language perspective on transactional memory consistency
A sound and complete proof technique for linearizability of concurrent data structures
Completeness and Nondeterminism in Model Checking Transactional Memories
Formal Techniques for Networked and Distributed Systems – FORTE 2004
Forward and backward simulations. I. Untimed Systems
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
Isabelle/HOL. A proof assistant for higher-order logic
Model checking transactional memories
Modular Safety Checking for Fine-Grained Concurrency
The serializability of concurrent database updates
Towards formally specifying and verifying transactional memory
Transactional Memory: Glimmer of a Theory
Verifying opacity of a transactional mutex lock
Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)

Cited in

(8)

Proving opacity via linearizability: a sound and complete method
Checking opacity and durable opacity with FDR
Modularising opacity verification for hybrid transactional memory
Defining and verifying durable opacity: correctness for persistent software transactional memory
Value-based or conflict-based? Opacity definitions for STMs
Proving opacity of a pessimistic STM
A verified durable transactional mutex lock for persistent x86-TSO
Verifying opacity of a transactional mutex lock

Describes a project that uses

Uses Software

This page was built for publication: Mechanized proofs of opacity: a comparison of two techniques