Using coarse-grained abstractions to verify linearizability on TSO architectures

Derrick, John, Smith, Graeme, Groves, Lindsay and Dongol, Brijesh (2014). Using coarse-grained abstractions to verify linearizability on TSO architectures. In: Eran Yahav, Hardware and Software: Verification and Testing. 10th International Haifa Verification Conference (HVC), Haifa, Israel, (1-16). 18 - 20 November 2014. doi:10.1007/978-3-319-13338-6_1


Author Derrick, John
Smith, Graeme
Groves, Lindsay
Dongol, Brijesh
Title of paper Using coarse-grained abstractions to verify linearizability on TSO architectures
Conference name 10th International Haifa Verification Conference (HVC)
Conference location Haifa, Israel
Conference dates 18 - 20 November 2014
Proceedings title Hardware and Software: Verification and Testing   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2014
Year available 2014
Sub-type Fully published paper
DOI 10.1007/978-3-319-13338-6_1
ISBN 9783319133379
9783319133386
ISSN 0302-9743
1611-3349
Editor Eran Yahav
Volume 8855
Start page 1
End page 16
Total pages 16
Chapter number 1
Total chapters 21
Collection year 2015
Language eng
Formatted Abstract/Summary
Most approaches to verifying linearizability assume a sequentially consistent memory model, which is not always realised in practice. In this paper we study correctness on a weak memory model: the TSO (Total Store Order) memory model, which is implemented in x86 multicore architectures.

Our central result is a proof method that simplifies proofs of linearizability on TSO. This is necessary since the use of local buffers in TSO adds considerably to the verification overhead on top of the already subtle linearizability proofs. The proof method involves constructing a coarse-grained abstraction as an intermediate layer between an abstract description and the concurrent algorithm. This allows the linearizability proof to be split into two smaller components, where the effect of the local buffers in TSO is dealt with at a higher level of abstraction than it would have been otherwise.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 03 Feb 2015, 16:41:42 EST by System User on behalf of School of Information Technol and Elec Engineering