A Constructive Approach for Proving Data Structures’ Linearizability
- Submitting institution
-
The University of Surrey
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9027032_1
- Type
- D - Journal article
- DOI
-
10.1007/978-3-662-48653-5_24
- Title of journal
- Lecture Notes in Computer Science;Distributed Computing
- Article number
- -
- First page
- 356
- Volume
- 9363
- Issue
- 0
- ISSN
- 0302-9743
- Open access status
- Out of scope for open access requirements
- Month of publication
- -
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Linearizability (aka atomicity) is a key correctness requirement for concurrent data structures, which is known to be notoriously hard to verify for practical implementations. We develop a new constructive framework that enables deriving linearizability entirely by analysing sequential behaviours, thus making its verification both simpler and more accessible to software engineers. We demonstrate the effectiveness of our framework by applying it to several popular concurrent data structures taken from widely used open-source Java concurrency packages. Recent work building on our approach has appeared at top programming languages and concurrency control venues including ACM OOPSLA'20 and IEEE TPDC'17.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -