Modular termination verification with a higher-order concurrent separation logic (Intermediate report)

TL;DR

This paper presents a modular approach to verify termination in concurrent programs using an extension of Iris, enabling reasoning about non-blocking algorithms with higher-order store and call permissions.

Contribution

It introduces call permissions and atomic blocks into a higher-order concurrent separation logic to modularly verify termination of concurrent, non-blocking algorithms without modifying Iris.

Findings

Successfully reasoned about termination of a lock-free concurrent stack

Extended Iris with call permissions and atomic blocks

Preserved Iris's ability to reason about helping and prophecies

Abstract

We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming language with a higher-order store. At present, we focus on one particular liveness property, namely termination. By guaranteeing termination we can strengthen statements of partial correctness to total correctness. This is achieved by the classic approach of turning termination into a safety property. In particular we extend the programming language under consideration with call permissions, which have been shown to enable modular reasoning about termination. Atomic blocks are added to increase the expressiveness of our call-permission-based approach. Our work builds on top of Iris -- a foundational, machine-checked, higher-order concurrent separation logic framework -- without modifying it. With these additions we are able to modularly reason about the termination of concurrent, but non-blocking algorithms. Our additions to the programming language under consideration preserve Iris' ability to reason about helping and prophecies. As an example, we apply the current system to an existing case study for a lock-free concurrent stack with helping that has been proven in Iris. Finally, we sketch the next steps to scale our approach to blocking concurrency.