A compositional proof method for linearizability applied to a wait-free multiset

4Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We introduce a compositional, complete proof method for linearizability that combines temporal logic, rely-guarantee reasoning and possibilities. The basic idea of our proof method is that each process must preserve possibility steps as an additional guarantee condition for linearizability. To illustrate the expressiveness of our method, we apply it to a wait-free multiset implementation with intricate linearization points. Both the soundness of our method as well as its application to our multiset have been mechanized in the interactive verifier KIV. © 2014 Springer International Publishing.

Cite

CITATION STYLE

APA

Tofan, B., Schellhorn, G., & Reif, W. (2014). A compositional proof method for linearizability applied to a wait-free multiset. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8739 LNCS, pp. 357–372). Springer Verlag. https://doi.org/10.1007/978-3-319-10181-1_22

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free