Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/13508
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. |
URI: | http://bura.brunel.ac.uk/handle/2438/13508 |
Appears in Collections: | Dept of Health Sciences Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 329.13 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.