Value-based or conflict-based? Opacity definitions for STMs

DOI10.1007/978-3-319-67729-3_8MaRDI QIDQ1675797zbMATH OpenOpenAlexFDO

Authors Jürgen König, Heike Wehrheim

Publication date 3 November 2017

Full work available at URL https://doi.org/10.1007/978-3-319-67729-3_8

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

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

Cited in

(5)

• Mechanized proofs of opacity: a comparison of two techniques
• Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)
• Defining and verifying durable opacity: correctness for persistent software transactional memory
• Verifying opacity of a transactional mutex lock
• Checking opacity and durable opacity with FDR

This page was built for publication: Value-based or conflict-based? Opacity definitions for STMs

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