{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:09Z","timestamp":1740109089009,"version":"3.37.3"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160102457","DP130102901"],"award-info":[{"award-number":["DP160102457","DP130102901"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            In the late 1980\u2019s, 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\n            <jats:italic>trace refinement<\/jats:italic>\n            , 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\u2019s work, Herlihy and Wing proposed\n            <jats:italic>linearizability<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0418-2","type":"journal-article","created":{"date-parts":[[2017,2,14]],"date-time":"2017-02-14T12:58:22Z","timestamp":1487077102000},"page":"935-950","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Relating trace refinement and linearizability"],"prefix":"10.1145","volume":"29","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kirsten","family":"Winter","sequence":"additional","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Back R-JR (1990) Refinement calculus part II: parallel and reactive programs. In: Stepwise refinement of distributed systems models formalisms correctness. Springer pp 67\u201393","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/1077084"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"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\u2013662","DOI":"10.1145\/2775051.2677002"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Back R-JR von Wright J (1994) Trace refinement of action systems. In: Concurrency theory (CONCUR \u201994) volume 836 of LNCS. Springer pp 367\u2013384","DOI":"10.1007\/978-3-540-48654-1_28"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"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\u2013194","DOI":"10.1007\/978-3-319-19249-9_12"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Derrick J Schellhorn G Wehrheim H (2011) Mechanically verified proof obligations for linearizability. ACM Trans Program Lang Syst 33(1):4:1\u20134:43","DOI":"10.1145\/1889997.1890001"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50034-5"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Ruppert E (2014) Linearizability is not always a safety property. In: Networked systems. volume 8593 of LNCS. Springer pp 57\u201369","DOI":"10.1007\/978-3-319-09581-3_5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"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\u2013465","DOI":"10.1007\/978-3-642-22012-8_36"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/1734069"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Hendler D Shavit N Yerushalmi L (2004) A scalable lock-free stack algorithm. In: ACM symposium on parallelism in algorithms and architectures (SPAA \u201904). ACM Press pp 206\u2013215","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"K\u00f6nig D (1990) Theory of finite and infinite graphs. Springer Berlin","DOI":"10.1007\/978-1-4684-8971-2"},{"key":"e_1_2_1_2_17_2","unstructured":"Spivey JM (1992) The Z notation: a reference manual. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"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\u201331:37","DOI":"10.1145\/2629496"},{"key":"e_1_2_1_2_19_2","unstructured":"Treiber RK (1986) Systems programming: coping with parallelism. Technical Report RJ 5118 IBM Almaden Res. Ctr."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0418-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0418-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0418-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0418-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:13:40Z","timestamp":1641485620000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0418-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.1007\/s00165-017-0418-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0418-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,11]]},"assertion":[{"value":"25 February 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 December 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}