Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compositional Verification in Concurrent Separation Logic with Permissions Regions

Quang Loc Le

TL;DR

This work advances automated, compositional verification for concurrent programs that manipulate shared memory by extending CSL-Perm with labels, permissions, and arithmetic ($\mathsf{SL}_{\mathsf{aLP}}$). It introduces distribution principles that preserve disjointness between strong and weak separating conjunctions, and a frame inference procedure FrInfer that automatically derives residual frames to support thread- and procedure-modular reasoning. The authors integrate FrInfer into a full compositional verifier, CoSl, and demonstrate its effectiveness on 10 challenging fine-grained programs, including cases beyond prior state-of-the-art. The approach enables robust automation for frame-based reasoning and compositional verification in CSL-Perm, with practical impact for scalable analysis of concurrent heap-manipulating code. The work also outlines directions for extending the framework with bi-abduction, cyclic proofs, and real-world applications such as smart contracts.

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.

Compositional Verification in Concurrent Separation Logic with Permissions Regions

TL;DR

This work advances automated, compositional verification for concurrent programs that manipulate shared memory by extending CSL-Perm with labels, permissions, and arithmetic (). It introduces distribution principles that preserve disjointness between strong and weak separating conjunctions, and a frame inference procedure FrInfer that automatically derives residual frames to support thread- and procedure-modular reasoning. The authors integrate FrInfer into a full compositional verifier, CoSl, and demonstrate its effectiveness on 10 challenging fine-grained programs, including cases beyond prior state-of-the-art. The approach enables robust automation for frame-based reasoning and compositional verification in CSL-Perm, with practical impact for scalable analysis of concurrent heap-manipulating code. The work also outlines directions for extending the framework with bi-abduction, cyclic proofs, and real-world applications such as smart contracts.

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.

Paper Structure

This paper contains 35 sections, 4 theorems, 48 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Compositional verification for inter-procedures.
  3. Compositional verification for concurrent threads.
  4. Overview and Illustrative Examples
  5. Distribution principles.
  6. Frame inference.
  7. Compositional verification.
  8. $\mathsf{SL}_{\mathsf{aLP}}$: CSL with Labels, Permissions, and Arithmetic
  9. Logical Principles of $\mathsf{SL}_{\mathsf{aLP}}$
  10. $*$ and $\circledast$ Distribution.
  11. Permission Distribution.
  12. Procedure $\textsf{ws{-}norm}({A})$.
  13. Procedures inward and inward*.
  14. Frame Inference Procedure
  15. FrInfer Entailment Algorithm
  16. ...and 20 more sections

Key Result

lemma thmcounterlemma

For all $A$, $B$, $C$ and $D$, and nominals $\alpha$, $\beta$, $\gamma$ and $\xi$

Figures (4)

  • Figure 1: Concurrent tree traversal with derived program states $\color{blue}{s_1}$, $\color{blue}{s_2}$, $\color{blue}{s_3}$ and $\color{blue}{s_4}$
  • Figure 2: Entailment proof rules for frame inference ($\square$ is $*$ or $\circledast$).
  • Figure 3: The programming language.
  • Figure 4: Predicate transformers for program statements ($x', y', \beta$ are fresh variables).

Theorems & Definitions (12)

  • lemma thmcounterlemma: $*$ and $\circledast$ Distribution
  • lemma thmcounterlemma: Permission Split and Join
  • theorem thmcountertheorem: Soundness
  • theorem thmcountertheorem: Soundness
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 2 more