SpringerLink
Log in

Relating trace refinement and linearizability

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

In the late 1980’s, Back extended the notion of stepwise refinement of sequential systems to concurrent systems. By doing so he provided a definition of what it means for a concurrent system to be correct with respect to an abstract (potentially sequential) specification. This notion of refinement, referred to as trace refinement, was also independently proposed by Abadi and Lamport and has found widespread acceptance and application within the refinement community. Around the same time as Back’s work, Herlihy and Wing proposed linearizability as the correctness notion for concurrent objects. Linearizability has also found widespread acceptance being regarded as the standard notion of correctness for concurrent objects in the concurrent-algorithms community. In this paper, we provide a formal link between trace refinement and linearizability. This allows us to compare the two correctness conditions. Our comparisons show that trace refinement implies linearizability, but that linearizability does not imply trace refinement in general. However, linearizability does imply trace refinement under certain conditions. These conditions relate to (i) the fact that trace refinement can be used to prove both safety and liveness properties, whereas linearizability can only be used to prove safety properties, and (ii) the fact that trace refinement depends on the identification of when operations in the implementation are observed to occur. We discuss the consequences of these differences in the context of verifying concurrent objects.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge

    Book  MATH  Google Scholar 

  2. Abadi M, Lamport L (1991) The existence of refinement map**s. Theor Comput Sci 82(2): 253–284

    Article  MATH  MathSciNet  Google Scholar 

  3. Back R-JR (1990) Refinement calculus, part II: parallel and reactive programs. In: Stepwise refinement of distributed systems models, formalisms, correctness. Springer, pp 67–93

  4. Bovet D, Cesati M (2005) Understanding the Linux kernel. O’Reilly & Associates, Sebastopol

    Google Scholar 

  5. Bouajjani A, Emmi M, Enea C, Hamza J (2015) Tractable refinement checking for concurrent objects. In ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2015). ACM, pp 651–662

  6. Back R-JR, von Wright J (1994) Trace refinement of action systems. In: Concurrency theory (CONCUR ’94), volume 836 of LNCS. Springer, pp 367–384

  7. Derrick J, Smith G (2015) A framework for correctness criteria on weak memory models. In: International symposium on formal methods (FM 2015). volume 9109 of LNCS. Springer, pp 178–194

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

  9. Filipović I, O’Hearn P, Rinetzky N, Yang H (2010) Abstraction for concurrent objects. Theor Comput Sci 411(51): 4379–4398

    Article  MATH  MathSciNet  Google Scholar 

  10. Gorrieri R, Rensink A (2001) Action refinement. In: (eds) In: Handbook of process algebra, chapter 16. Elsevier, Amsterdam, pp 1047–1147

    Chapter  Google Scholar 

  11. Guerraoui R, Ruppert E (2014) Linearizability is not always a safety property. In: Networked systems. volume 8593 of LNCS. Springer, pp 57–69

  12. Gotsman A, Yang H (2011) Liveness-preserving atomicity abstraction. In: International colloquium on automata, languages and programming (ICALP 2011), volume 6756 of LNCS. Springer, pp 453–465

  13. Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Burlington

    Google Scholar 

  14. Hendler D, Shavit N, Yerushalmi L (2004) A scalable lock-free stack algorithm. In: ACM symposium on parallelism in algorithms and architectures (SPAA ’04). ACM Press, pp 206–215

  15. Herlihy M, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3): 463–492

    Article  Google Scholar 

  16. König D (1990) Theory of finite and infinite graphs. Springer, Berlin

  17. Spivey JM (1992) The Z notation: a reference manual. Prentice Hall, Upper Saddle River

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

  19. Treiber RK (1986) Systems programming: co** with parallelism. Technical Report RJ 5118, IBM Almaden Res. Ctr.

Download references

Author information

Authors and Affiliations

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

    Graeme Smith & Kirsten Winter

Authors
  1. Graeme Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kirsten Winter
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Graeme Smith.

Additional information

Communicated by Michael Butler

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Smith, G., Winter, K. Relating trace refinement and linearizability. Form Asp Comp 29, 935–950 (2017). https://doi.org/10.1007/s00165-017-0418-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-017-0418-2

Keywords

Search

Navigation