Skip to main content
SpringerLink
Log in

An Observational Approach to Defining Linearizability on Weak Memory Models

  • Conference paper
  • First Online:
Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10321))

Abstract

In this paper we present a framework for defining linearizability on weak memory models. The purpose of the framework is to be able to define the correctness of concurrent algorithms in a uniform way across a variety of memory models. To do so linearizability is defined within the framework in terms of memory order as opposed to program order. Such a generalisation of the original definition of linearizability enables it to be applied to non-sequentially consistent architectures. It also allows the definition to be given in terms of observable effects rather than being dependent on an understanding of the weak memory model architecture. We illustrate the framework on the TSO (Total Store Order) weak memory model, and show that it respects existing definitions of linearizability on TSO.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The related work of Burckhardt [3] and Gotsman [11] avoid this issue by modifiying the abstract specification. We are motivated, however, to allow implementations on TSO to be proved correct with respect to standard specifications of concurrent objects.

  2. 2.

    We use the term behaviour to informally refer to a sequence of operations an object may undergo. Later we formalise this as histories used in the standard definition of linearizability, and as executions used in our observational definition of linearizability.

  3. 3.

    This principle is also used in other work on linearizability in TSO [19].

  4. 4.

    To distinguish identical commands such as the two stores to c in the write operation of seqlock we would add other identifying information such as program counters, but we elide that detail here.

  5. 5.

    Since commands are deterministic there is exactly one such value.

References

  1. 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 

  2. Amit, D., Rinetzky, N., Reps, T., 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). doi:10.1007/978-3-540-73368-3_49

    Chapter  Google Scholar 

  3. Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 87–107. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28869-2_5

    Chapter  Google Scholar 

  4. Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233–248. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74061-2_15

    Chapter  Google Scholar 

  5. Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 4:1–4:43 (2011)

    Article  Google Scholar 

  6. 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). doi:10.1007/978-3-642-21437-0_25

    Chapter  Google Scholar 

  7. Derrick, J., Smith, G.: A framework for correctness criteria on weak memory models. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 178–194. Springer, Cham (2015). doi:10.1007/978-3-319-19249-9_12

    Chapter  Google Scholar 

  8. Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 341–356. Springer, Cham (2014). doi:10.1007/978-3-319-10181-1_21

    Google Scholar 

  9. Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30232-2_7

    Chapter  Google Scholar 

  10. Fitzpatrick, J.: An interview with Steve Furber. Commun. ACM 54(5), 34–39 (2011)

    Article  Google Scholar 

  11. 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). doi:10.1007/978-3-642-33651-5_3

    Chapter  Google Scholar 

  12. 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 

  13. Maranget, L., Sarkar, S., Sewell, P.: A tutorial introduction to the ARM and POWER relaxed memory models (2012). Draft available from http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf

  14. Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Automated Deduction, pp. 13–39. Kluwer (1998)

    Google Scholar 

  15. Schellhorn, G., Wehrheim, H., Derrick, J.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Log. 15(4), 31:1–31:37 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  16. 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 

  17. Smith, G., Derrick, J., Dongol, B.: Admit your weakness: verifying correctness on TSO architectures. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 364–383. Springer, Cham (2015). doi:10.1007/978-3-319-15317-9_22

    Google Scholar 

  18. 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, San Rafael (2011)

    Google Scholar 

  19. 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, Cham (2013). doi:10.1007/978-3-319-03077-7_21

    Chapter  Google Scholar 

  20. Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132–147. Springer, Cham (2014). doi:10.1007/978-3-319-13338-6_11

    Google Scholar 

  21. Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, University of Sheffield, Sheffield, UK

    John Derrick

  2. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, Australia

    Graeme Smith

Authors
  1. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Graeme Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John Derrick .

Editor information

Editors and Affiliations

  1. University Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. University College London, London, United Kingdom

    Alexandra Silva

Rights and permissions

Reprints and permissions

Copyright information

© 2017 IFIP International Federation for Information Processing

About this paper

Cite this paper

Derrick, J., Smith, G. (2017). An Observational Approach to Defining Linearizability on Weak Memory Models. In: Bouajjani, A., Silva, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2017. Lecture Notes in Computer Science(), vol 10321. Springer, Cham. https://doi.org/10.1007/978-3-319-60225-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-60225-7_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-60224-0

  • Online ISBN: 978-3-319-60225-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation