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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge
Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82(2): 253–284
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
Bovet D, Cesati M (2005) Understanding the Linux kernel. O’Reilly & Associates, Sebastopol
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
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
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
Derrick J, Schellhorn G, Wehrheim H (2011) Mechanically verified proof obligations for linearizability. ACM Trans Program Lang Syst 33(1):4:1–4:43
Filipović I, O’Hearn P, Rinetzky N, Yang H (2010) Abstraction for concurrent objects. Theor Comput Sci 411(51): 4379–4398
Gorrieri R, Rensink A (2001) Action refinement. In: (eds) In: Handbook of process algebra, chapter 16. Elsevier, Amsterdam, pp 1047–1147
Guerraoui R, Ruppert E (2014) Linearizability is not always a safety property. In: Networked systems. volume 8593 of LNCS. Springer, pp 57–69
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
Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Burlington
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
Herlihy M, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3): 463–492
König D (1990) Theory of finite and infinite graphs. Springer, Berlin
Spivey JM (1992) The Z notation: a reference manual. Prentice Hall, Upper Saddle River
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
Treiber RK (1986) Systems programming: coping with parallelism. Technical Report RJ 5118, IBM Almaden Res. Ctr.
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by Michael Butler
Rights and permissions
About this article
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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0418-2