Verifying linearizability on TSO architectures

Derrick, John, Smith, Graeme and Dongol, Brijesh (2014). Verifying linearizability on TSO architectures. In: Elvira Albert and Emil Sekerinski, Integrated Formal Methods - 11th International Conference, IFM 2014, Proceedings. 11th International Conference on Integrated Formal Methods, IFM 2014, Bertinoro, Italy, (341-356). 9 - 11 September 2014. doi:10.1007/978-3-319-10181-1_21


Author Derrick, John
Smith, Graeme
Dongol, Brijesh
Title of paper Verifying linearizability on TSO architectures
Conference name 11th International Conference on Integrated Formal Methods, IFM 2014
Conference location Bertinoro, Italy
Conference dates 9 - 11 September 2014
Proceedings title Integrated Formal Methods - 11th International Conference, IFM 2014, Proceedings   Check publisher's open access policy
Journal name Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   Check publisher's open access policy
Series Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2014
Year available 2014
Sub-type Fully published paper
DOI 10.1007/978-3-319-10181-1_21
ISBN 9783319101804
9783319101811
ISSN 0302-9743
1611-3349
Editor Elvira Albert
Emil Sekerinski
Volume 8739 LNCS
Start page 341
End page 356
Total pages 16
Chapter number 21
Total chapters 23
Collection year 2015
Language eng
Abstract/Summary Linearizability is the standard correctness criterion for fine-grained, non-atomic concurrent algorithms, and a variety of methods for verifying linearizability have been developed. However, most approaches assume a sequentially consistent memory model, which is not always realised in practice. In this paper we define linearizability on a weak memory model: the TSO (Total Store Order) memory model, which is implemented in the x86 multicore architecture. We also show how a simulation-based proof method can be adapted to verify linearizability for algorithms running on TSO architectures. We demonstrate our approach on a typical concurrent algorithm, spinlock, and prove it linearizable using our simulation-based approach. Previous approaches to proving linearizabilty on TSO architectures have required a modification to the algorithm's natural abstract specification. Our proof method is the first, to our knowledge, for proving correctness without the need for such modification.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 3 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Mon, 02 Mar 2015, 19:47:59 EST by Graeme Smith on behalf of School of Information Technol and Elec Engineering