Shared Contract-Obedient Endpoints

Étienne Lozes
(Universität Kassel, Germany)
Jules Villard
(University College London, UK)

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.

In Marco Carbone, Ivan Lanese, Alexandra Silva and Ana Sokolova: Proceedings Fifth Interaction and Concurrency Experience (ICE 2012), Stockholm, Sweden, 16th June 2012, Electronic Proceedings in Theoretical Computer Science 104, pp. 17–31.
Published: 14th December 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.104.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org