Compositional Verification of a Lock-Free Stack with RGITL

2015/11/03 by Bogdan Tofan, Tofan, Bogdan, Gerhard Schellhorn +7
Computer Science · #Distributed systems and fault tolerance #Formal Methods in Verification #Logic, programming, and type systems

paper · pdf · doi:10.14279/tuj.eceasst.66.885

Abstract

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.

Related

• Compositional Verification in Concurrent Separation Logic with Permissions Regions
• Compositional Reasoning for Shared-variable Concurrent Programs
• Structural Temporal Logic for Mechanized Program Verification
• Compositional Verification in Rewriting Logic
• Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)