Shared Contract-Obedient Endpoints

TL;DR

This paper introduces a novel verification approach for message-passing programs that balances linear and arbitrary endpoint usage by extending separation logic with fractional shares and reflexive ownership transfer.

Contribution

It presents a new proof system enabling shared endpoint usage in message-passing programs, bridging the gap between existing linear and arbitrary sharing techniques.

Findings

Supports sharing of endpoints with fractional shares

Introduces reflexive ownership transfer mechanism

Demonstrates linear sharing in various examples

Abstract

Most of the existing verification techniques for message-passing programs suppose either that channel endpoints are used in a linear fashion, where at most one thread may send or receive from an endpoint at any given time, or that endpoints may be used arbitrarily by any number of threads. The former approach usually forbids the sharing of channels while the latter limits what is provable about programs. In this paper we propose a midpoint between these techniques by extending a proof system based on separation logic to allow sharing of endpoints. We identify two independent mechanisms for supporting sharing: an extension of fractional shares to endpoints, and a new technique based on what we call reflexive ownership transfer. We demonstrate on a number of examples that a linear treatment of sharing is possible.