Please use this identifier to cite or link to this item:
Title: Verifying opacity of a transactional Mutex lock
Authors: Derrick, J
Dongol, B
Schellhorn, G
Travkin, O
Wehrheim, H
Issue Date: 2015
Citation: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2015, vol. 9109 pp. 161 - 177
Abstract: Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as an atomic block. This atomicity property is captured by a correctness criterion called opacity. Opacity relates histories of a sequential atomic specification with that of STM implementations. In this paper we prove opacity of a recently proposed STM implementation (a Transactional Mutex Lock) by Dalessandro et al.. The proof is carried out within the interactive verifier KIV and proceeds via the construction of an intermediate level in between sequential specification and implementation, leveraging existing proof techniques for linearizability.
Description: © Springer International Publishing Switzerland 2015.
ISBN: 9783319192482
ISSN: 0302-9743
Appears in Collections:Publications

Files in This Item:
File Description SizeFormat 
FullText.pdf236.48 kBUnknownView/Open

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