Shared Contract-Obedient Endpoints
\'Etienne Lozes (Universit\"at Kassel, Germany), Jules Villard, (University College London, UK)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Security and Verification in Computing · Distributed systems and fault tolerance
