Modularising opacity verification for hybrid transactional memory

DOI10.1007/978-3-319-60225-7_3MaRDI QIDQ5082189zbMATH OpenOpenAlexFDO

Authors Alasdair Armstrong, Brijesh Dongol

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-01658416/file/446833_1_En_3_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

• Proving opacity via linearizability: a sound and complete method
• Verifying opacity of a transactional mutex lock
• Proving opacity of a pessimistic STM
• Mechanized proofs of opacity: a comparison of two techniques
• Proving opacity of transactional memory with early release

Cited in

(8)

• Mechanized proofs of opacity: a comparison of two techniques
• Proving opacity of a pessimistic STM
• Defining and verifying durable opacity: correctness for persistent software transactional memory
• Proving opacity via linearizability: a sound and complete method
• Modularising verification of durable opacity
• Verifying opacity of a transactional mutex lock
• Checking opacity and durable opacity with FDR
• Proving opacity of transactional memory with early release

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Modularising opacity verification for hybrid transactional memory

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