Towards Concurrent Quantitative Separation Logic

TL;DR

This paper introduces a new separation logic that combines quantitative and concurrent separation logic to reason about programs with concurrency, pointers, and randomization, focusing on probabilistic lower bounds.

Contribution

It develops a novel verification technique that integrates two types of separation logic to handle the complex combination of concurrency, pointers, and randomization.

Findings

Enables reasoning about lower bounds of probabilities for postconditions.

Bridges the gap in existing logic frameworks for combined paradigms.

Provides a foundation for probabilistic program verification in concurrent settings.

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.