Skip to Main content Skip to Navigation
Conference papers

Proving Opacity via Linearizability: A Sound and Complete Method

Abstract : Transactional memory (TM) is a mechanism that manages thread synchronisation on behalf of a programmer so that blocks of code execute with the illusion of atomicity. The main safety criterion for transactional memory is opacity, which defines conditions for serialising concurrent transactions.Verifying opacity is complex because one must not only consider the orderings between fine-grained (and hence concurrent) transactional operations, but also between the transactions themselves. This paper presents a sound and complete method for proving opacity by decomposing the proof into two parts, so that each form of concurrency can be dealt with separately. Thus, in our method, verification involves a simple proof of opacity of a coarse-grained abstraction, and a proof of linearizability, a better-understood correctness condition. The most difficult part of these verifications is dealing with the fine-grained synchronization mechanisms of a given implementation; in our method these aspects are isolated to the linearizability proof. Our result makes it possible to leverage the many sophisticated techniques for proving linearizability that have been developed in recent years. We use our method to prove opacity of two algorithms from the literature. Furthermore, we show that our method extends naturally to weak memory models by showing that both these algorithms are opaque under the TSO memory model, which is the memory model of the (widely deployed) x86 family of processors. All our proofs have been mechanised, either in the Isabelle theorem prover or the PAT model checker.
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01658425
Contributor : Hal Ifip <>
Submitted on : Thursday, December 7, 2017 - 3:49:16 PM
Last modification on : Thursday, December 26, 2019 - 10:48:02 AM

File

446833_1_En_4_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Alasdair Armstrong, Brijesh Dongol, Simon Doherty. Proving Opacity via Linearizability: A Sound and Complete Method. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. pp.50-66, ⟨10.1007/978-3-319-60225-7_4⟩. ⟨hal-01658425⟩

Share

Metrics

Record views

156

Files downloads

87