Please use this identifier to cite or link to this item:
Title: Proving opacity of a pessimistic STM
Authors: Doherty, S
Dongol, B
Derrick, J
Schellhorn, G
Wehrheim, H
Keywords: Pessimistic STMs;Opacity;Verification;Isabelle;Simulation;TMS2
Issue Date: 2016
Citation: OPODIS (2016)
Abstract: Transactional Memory (TM) is a high-level programming abstraction for concurrency control that provides programmers with the illusion of atomically executing blocks of code, called transactions. TMs come in two categories, optimistic and pessimistic, where in the latter transactions never abort. While this simplifies the programming model, high-performing pessimistic TMs can complex. In this paper, we present the first formal verification of a pessimistic software TM algorithm, namely, an algorithm proposed by Matveev and Shavit. The correctness criterion used is opacity, formalising the transactional atomicity guarantees. We prove that this pessimistic TM is a refinement of an intermediate opaque I/O-automaton, known as TMS2. To this end, we develop a rely-guarantee approach for reducing the complexity of the proof. Proofs are mechanised in the interactive prover Isabelle.
Appears in Collections:Dept of Clinical Sciences Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf329.13 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.