Verifying Linearizability on TSO Architectures | Springer Nature Link

Verifying Linearizability on TSO Architectures | Springer Nature Link
Advertisement
Verifying Linearizability on TSO Architectures
Conference paper
pp 341–356
Cite this conference paper
Integrated Formal Methods
(IFM 2014)
Abstract
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.
This is a preview of subscription content,
log in via an institution
to check access.
Access this chapter
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Chapter
EUR 29.95
Price includes VAT (France)
eBook
EUR 42.79
Price includes VAT (France)
Softcover Book
EUR 52.74
Price includes VAT (France)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Institutional subscriptions
Preview
Unable to display preview.
Download preview
PDF.
Unable to display preview.
Download preview
PDF.
Similar content being viewed by others
A Proof Method for Linearizability on TSO Architectures
Chapter
An Observational Approach to Defining Linearizability on Weak Memory Models
Chapter
Proving Opacity via Linearizability: A Sound and Complete Method
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Algorithms
Computability and Recursion Theory
Data Structures
Linear Logic
Register-Transfer-Level Implementation
Theory of Computation
Memory Consistency Models in Concurrent Programming Systems
References
Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The Semantics of Power and ARM Multiprocessor Machine Code. In: Petersen, L., Chakravarty, M.M.T. (eds.) DAMP 2009, pp. 13–24. ACM (2008)
Google Scholar
Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 477–490. Springer, Heidelberg (2007)
Chapter
Google Scholar
Bovet, D., Cesati, M.: Understanding the Linux Kernel, 3rd edn. O’Reilly (2005)
Google Scholar
Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 87–107. Springer, Heidelberg (2012)
Chapter
Google Scholar
Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233–248. Springer, Heidelberg (2007)
Chapter
Google Scholar
Derrick, J., Schellhorn, G., Wehrheim, H.: Proving linearizability via non-atomic refinement. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 195–214. Springer, Heidelberg (2007)
Chapter
Google Scholar
Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 4 (2011)
Google Scholar
Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 323–337. Springer, Heidelberg (2011)
Chapter
Google Scholar
Derrick, J., Wehrheim, H.: Non-atomic refinement in Z and CSP. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 24–44. Springer, Heidelberg (2005)
Google Scholar
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004)
Chapter
Google Scholar
Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: Sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31–45. Springer, Heidelberg (2012)
Chapter
Google Scholar
Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Article
Google Scholar
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690–691 (1979)
Article
MATH
Google Scholar
Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 243–259. Springer, Heidelberg (2012)
Chapter
Google Scholar
Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)
Article
Google Scholar
Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture. Morgan & Claypool Publishers (2011)
Google Scholar
Travkin, O., Mütze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311–326. Springer, Heidelberg (2013)
Chapter
Google Scholar
Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2007)
Google Scholar
Download references
Author information
Authors and Affiliations
Department of Computing, University of Sheffield, Sheffield, UK
John Derrick & Brijesh Dongol
School of Information Technology and Electrical Engineering, The University of Queensland, St Lucia, Australia
Graeme Smith
Authors
John Derrick
View author publications
Search author on:
PubMed
Google Scholar
Graeme Smith
View author publications
Search author on:
PubMed
Google Scholar
Brijesh Dongol
View author publications
Search author on:
PubMed
Google Scholar
Editor information
Editors and Affiliations
Complutense University of Madrid, Madrid, Spain
Elvira Albert
McMaster University, Hamilton, Ontario, Canada
Emil Sekerinski
Rights and permissions
Reprints and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Derrick, J., Smith, G., Dongol, B. (2014). Verifying Linearizability on TSO Architectures.

In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_21
Download citation
.RIS
.ENW
.BIB
DOI
Publisher Name
Springer, Cham
Print ISBN
978-3-319-10180-4
Online ISBN
978-3-319-10181-1
eBook Packages
Computer Science
Computer Science (R0)
Springer Nature Proceedings Computer Science
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Memory Model
Global Memory
Abstract Operation
Proof Method
Return Event
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Publish with us
Policies and ethics
Profiles
Brijesh Dongol
View author profile
Access this chapter
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Chapter
EUR 29.95
Price includes VAT (France)
eBook
EUR 42.79
Price includes VAT (France)
Softcover Book
EUR 52.74
Price includes VAT (France)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Institutional subscriptions