Title: Separation-Based Reasoning for Deterministic Channel-Passing Concurrent Programs

Abstract:
The correctness of concurrent programs is hard to reason about because of the multiple interleaving and interactions between the independently executing program entities (e.g., threads, processes etc.) that need to be considered. Yet, for a substantial subset of concurrent programs that are required to be deterministic, more scalable and modular proof systems have been proposed. In these proof systems, only a subset of interleaving/interactions are considered and the analysis is decomposed so that the correctness of the global program is derived from the analysis of its sub-programs, i.e., local reasoning.

In this work we study the development of a local reasoning technique, based on resource separation, to reason about the correctness of message-passing concurrent programs. In particular we focus on resource reuse patterns that can be used in this setting.
We demonstrate the feasibility of our logical framework through the analysis of a resource-efficient implementation of Sorting Networks (SNs).