Permission-Based Separation Logic for Message-Passing Concurrency

TL;DR

This paper introduces a permission-based separation logic framework for message-passing concurrency, enabling local reasoning and compositional verification of concurrent programs.

Contribution

It extends processes with permission-resources and develops a sound proof system for separation-based reasoning in message-passing concurrency.

Findings

Provides a reduction semantics for permission-extended processes

Defines a sound proof system for local, separation-based reasoning

Lays a foundation for compositional verification of message-passing programs

Abstract

We develop local reasoning techniques for message passing concurrent programs based on ideas from separation logics and resource usage analysis. We extend processes with permission- resources and define a reduction semantics for this extended language. This provides a foundation for interpreting separation formulas for message-passing concurrency. We also define a sound proof system permitting us to infer satisfaction compositionally using local, separation-based reasoning.