Please use this identifier to cite or link to this item:
|Title:||Verifying opacity of a transactional Mutex lock|
|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.|
|Appears in Collections:||Publications|
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.