Relating trace refinement and linearizability

Smith, Graeme and Winter, Kirsten (2017) Relating trace refinement and linearizability. Formal Aspects of Computing, 1-16. doi:10.1007/s00165-017-0418-2


Author Smith, Graeme
Winter, Kirsten
Title Relating trace refinement and linearizability
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 1433-299X
0934-5043
Publication date 2017-02-14
Sub-type Article (original research)
DOI 10.1007/s00165-017-0418-2
Open Access Status Not yet assessed
Start page 1
End page 16
Total pages 16
Place of publication London, United Kingdom
Publisher Springer U K
Collection year 2018
Language eng
Formatted 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.
Keyword Concurrency
Correctness
Linearizability
Trace refinement
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: HERDC Pre-Audit
School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 28 Feb 2017, 00:20:24 EST by Web Cron on behalf of Learning and Research Services (UQ Library)