Compositional Verification of a Lock-Free Stack with RGITL

Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfahler, Wolfgang Reif


This paper describes a compositional verification approach for concurrent
algorithms based on the logic Rely-Guarantee Interval Temporal Logic (RGITL),
which is implemented in the interactive theorem prover KIV. The logic makes it
possible to mechanically derive and apply decomposition theorems for safety and
liveness properties. Decomposition theorems for rely-guarantee reasoning, linearizability and lock-freedom are described and applied on a non-trivial running example,
a lock-free data stack implementation that uses an explicit allocator stack for memory reuse. To deal with the heap, a lightweight approach that combines ownership
annotations and separation logic is taken.

Full Text:




Hosted By Universitätsbibliothek TU Berlin.