Proving opacity via linearizability: a sound and complete method

DOI10.1007/978-3-319-60225-7_4MaRDI QIDQ5082190zbMATH OpenOpenAlexFDO

Authors Alasdair Armstrong, Brijesh Dongol, Simon Doherty

Publication date 15 June 2022

Published in Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01658425/file/446833_1_En_4_Chapter.pdf

Mathematics Subject Classification ID

Distributed systems (68M14) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Mechanized proofs of opacity: a comparison of two techniques
• Modularising opacity verification for hybrid transactional memory
• Verifying opacity of a transactional mutex lock
• Proving opacity of a pessimistic STM
• Proving opacity of transactional memory with early release

Cited in

(9)

• Mechanized proofs of opacity: a comparison of two techniques
• Value-based or conflict-based? Opacity definitions for STMs
• Proving opacity of a pessimistic STM
• Defining and verifying durable opacity: correctness for persistent software transactional memory
• Modularising opacity verification for hybrid transactional memory
• Modularising verification of durable opacity
• Verifying opacity of a transactional mutex lock
• Checking opacity and durable opacity with FDR
• A verified durable transactional mutex lock for persistent x86-TSO

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Proving opacity via linearizability: a sound and complete method

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