Towards Concurrent Quantitative Separation Logic
Ira Fesefeldt, Joost-Pieter Katoen, Thomas Noll
TL;DR
The paper develops concurrent, heap-manipulating probabilistic reasoning by merging Quantitative Separation Logic (QSL) with Concurrent Separation Logic (CSL) into a new framework. It introduces chpGCL, a concurrent heap-manipulating probabilistic language with Markov Decision Process semantics, and defines weakest resource-safe liberal preexpectations (wrlp) to obtain lower bounds on postconditions via resource invariants. A formal proof system accompanies the semantics, enabling backward reasoning about lower-bounded probabilistic properties in concurrent settings, and is demonstrated on a producer-consumer–lossy channel example. The approach advances scalable, sound verification of randomized, pointer-based concurrent algorithms, while highlighting limitations and directions for future work, including upper-bound reasoning and environmental probabilistic models.
Abstract
In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic -- Quantitative Separation Logic and Concurrent Separation Logic -- into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program.