License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2022.4
URN: urn:nbn:de:0030-drops-162324
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16232/
Go to the corresponding LIPIcs Volume Portal

Lagaillardie, Nicolas ; Neykova, Rumyana ; Yoshida, Nobuko

Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types

pdf-format:
LIPIcs-ECOOP-2022-4.pdf (2 MB)

Abstract

Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new typing discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).

BibTeX - Entry

@InProceedings{lagaillardie_et_al:LIPIcs.ECOOP.2022.4,
  author =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  title =	{{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16232},
  URN =		{urn:nbn:de:0030-drops-162324},
  doi =		{10.4230/LIPIcs.ECOOP.2022.4},
  annote =	{Keywords: Rust language, affine multiparty session types, failures, cancellation}
}

Keywords: Rust language, affine multiparty session types, failures, cancellation
Collection: 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022
Supplementary Material: Software (ECOOP 2022 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.8.2.9

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI