Verifying Opacity of a Transactional Mutex Lock

J. Derrick and B. Dongol and G. Schellhorn and O. Travkin and H. Wehrheim

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.
published 22.06.2015 Proceeding of FM 2015, LNCS 9109, pp. 161-177

Publisher: Springer

DOI: (Springer Link)


For questions regarding the publication, please contact!