Non-Blocking Concurrent Imperative Programming with Session Types

Miguel Silva
Mário Florido
Frank Pfenning

Concurrent C0 is an imperative programming language in the C family with session-typed message-passing concurrency. The previously proposed semantics implements asynchronous (non-blocking) output; we extend it here with non-blocking input. A key idea is to postpone message reception as much as possible by interpreting receive commands as a request for a message. We implemented our ideas as a translation from a blocking intermediate language to a non-blocking language. Finally, we evaluated our techniques with several benchmark programs and show the results obtained. While the abstract measure of span always decreases (or remains unchanged), only a few of the examples reap a practical benefit.

In Iliano Cervesato and Maribel Fernández: Proceedings Fourth International Workshop on Linearity (LINEARITY 2016), Porto, Portugal, 25 June 2016, Electronic Proceedings in Theoretical Computer Science 238, pp. 64–72.
Published: 17th January 2017.

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