Separation-based reasoning for deterministic message-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, e.g., [O'H07, PM06, VP07, DFPV09, FRS11]. 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 reuse patterns traditionally used in this setting. We demonstrate the feasibility of our logical framework through the analysis of a resource-efficient implementation of Sorting Networks (SNs) [Bat68, Knu98]. A set of deterministic algorithms for sorting list of values concurrently, which are also used to give deeper insights into problems such as loop parallelisation.