Abstract
Linearizability is one of the main correctness criteria for implementations of concurrent data structures. A data structure is linearizable if its operations appear to execute atomically. Verifying linearizability of concurrent unbounded linked data structures is a challenging problem because it requires correlating executions that manipulate (unbounded-size) memory states. We present a static analysis for verifying linearizability of concurrent unbounded linked data structures. The novel aspect of our approach is the ability to prove that two (unboundedsize) memory layouts of two programs are isomorphic in the presence of abstraction. A prototype implementation of the analysis verified the linearizability of several published concurrent data structures implemented by singly-linked lists. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Amit, D., Rinetzky, N., Reps, T., Sagiv, M., & Yahav, E. (2007). Comparison under abstraction for verifying linearizability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4590 LNCS, pp. 477–490). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_49
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
