ISSE

Search

Local Rely-Guarantee Conditions for Linearizability and Lock-Freedom

B.Tofan, G. Schellhorn, and W. Reif

Local Rely-Guarantee Conditions for Linearizability and Lock-Freedom

Rely-guarantee reasoning specifications typically consider all components of a concurrent system. For the important case where components operate on a shared data object, we derive a local instance of rely-guarantee reasoning, which permits specifications to examine a single pair of representative components only. Based on this instance, we define local proof obligations for linearizability and lock-freedom, which we then apply to a non-blocking concurrent stack with explicit memory reuse. Both the derivation of this local instance and its application are mechanized in the KIV interactive theorem prover.
published 2011 In Pre-Proceedings of Conference on Formal Verification of Object Oriented Software (FoVeOOS)

Publisher: Karlsruhe Reports in Informatics, vol. 26, pp. 342 - 359


Downloads: