Compositional Verification in Concurrent Separation Logic with Permissions Regions

TL;DR

This paper introduces a new compositional verification system for concurrent programs using separation logic with permissions, enhancing automation and reasoning about shared memory regions.

Contribution

It presents novel logical principles and an entailment procedure for compositional reasoning in CSLPerm, with an implementation in the CoSl tool.

Findings

Successfully verified 10 challenging concurrent programs

Demonstrated improved automation and compositionality

Outperformed existing methods on complex benchmarks

Abstract

Concurrent separation logic with fractional permissions (CSLPerm) provides a promising reasoning system to verify most complex sequential and concurrent fine-grained programs. The logic with strong and weak separating conjunctions offers a solid foundation for producing concise and precise proofs. However, it lacks automation and compositionality support. This paper addresses this limitation by introducing a compositional verification system for concurrent programs that manipulate regions of shared memory. The centre of our system is novel logical principles and an entailment procedure that can infer the residual heaps in the frame rule for a fragment of CSL-Perm with explicit arithmetical constraints for memory heaps' disjointness. This procedure enables the compositional reasoning for concurrent threads and function calls. We have implemented the proposal in a prototype tool called CoSl, tested it with 10 challenging concurrent programs, including those beyond the state-of-the-art, and confirmed the advantage of our approach.