Stay safe under panic: affine rust programming with multiparty session types
File(s)LIPIcs-ECOOP-2022-4.pdf (1.82 MB)
Published version
Author(s)
Lagaillardie, Nicolas
Neykova, Rumyana
Yoshida, Nobuko
Type
Conference Paper
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 synchronize 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 autodetects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism
for communication, synchronization 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).
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 synchronize 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 autodetects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism
for communication, synchronization 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).
Date Issued
2022-06-23
Date Acceptance
2022-03-01
Citation
Leibniz International Proceedings in Informatics, 2022, 222, pp.4:1-4:29
ISBN
978-3-95977-225-9
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
4:1
End Page
4:29
Journal / Book Title
Leibniz International Proceedings in Informatics
Volume
222
Copyright Statement
© Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida;
licensed under Creative Commons License CC-BY 4.0 (https://creativecommons.org/licenses/by/4.0/)
licensed under Creative Commons License CC-BY 4.0 (https://creativecommons.org/licenses/by/4.0/)
License URL
Source
European Conference on Object-Oriented Programming (ECOOP)'22)
Publication Status
Published
Start Date
2022-06-06
Finish Date
2022-06-10
Coverage Spatial
Berlin, Germany