Thumbnail
Access Restriction
Subscribed

Author Dongol, Brijesh ♦ Derrick, John
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2015
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Linearisability ♦ Abstraction ♦ Compositional proofs ♦ Concurrent objects ♦ Interval-based methods ♦ Mechanisation ♦ Reduction ♦ Refinement ♦ Shape analysis
Abstract Linearisability is a key correctness criterion for concurrent data structures, ensuring that each history of the concurrent object under consideration is consistent with respect to a history of the corresponding abstract data structure. Linearisability allows concurrent (i.e., overlapping) operation calls to take effect in any order, but requires the real-time order of nonoverlapping to be preserved. The sophisticated nature of concurrent objects means that linearisability is difficult to judge, and hence, over the years, numerous techniques for verifying lineasizability have been developed using a variety of formal foundations such as data refinement, shape analysis, reduction, etc. However, because the underlying framework, nomenclature, and terminology for each method is different, it has become difficult for practitioners to evaluate the differences between each approach, and hence, evaluate the methodology most appropriate for verifying the data structure at hand. In this article, we compare the major of methods for verifying linearisability, describe the main contribution of each method, and compare their advantages and limitations.
ISSN 03600300
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2015-09-01
Publisher Place New York
e-ISSN 15577341
Journal ACM Computing Surveys (CSUR)
Volume Number 48
Issue Number 2
Page Count 43
Starting Page 1
Ending Page 43


Open content in new tab

   Open content in new tab
Source: ACM Digital Library