ISSE

Search

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset

B. Tofan, G. Schellhorn, W. Reif

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset

We introduce a compositional 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 sequences of 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.
published 2014 In Proc. of Integrated Formal Methods (iFM), vol. 8739 LNCS, pp.357-372

Publisher: Springer