Abstract
We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.
Cite
CITATION STYLE
Lev-Ari, K., Chockler, G., & Keidar, I. (2015). A constructive approach for proving data structures’ linearizability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9363, pp. 356–370). Springer Verlag. https://doi.org/10.1007/978-3-662-48653-5_24
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
