Proving linearizability with temporal logic |
| |
Authors: | Simon B?umler Gerhard Schellhorn Bogdan Tofan Wolfgang Reif |
| |
Affiliation: | (2) Department of Computer Science, Brown University, Providence, RI, USA |
| |
Abstract: | Linearizability is a global correctness criterion for concurrent systems. One technique to prove linearizability is applying a composition theorem which reduces the proof of a property of the overall system to sufficient rely-guarantee conditions for single processes. In this paper, we describe how the temporal logic framework implemented in the KIV interactive theorem prover can be used to model concurrent systems and to prove such a composition theorem. Finally, we show how this generic theorem can be instantiated to prove linearizability of two classic lock-free implementations: a Treiber-like stack and a slightly improved version of Michael and Scott’s queue. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|