Fearless Asynchronous Communications with Timed Session Types in Rust (Artifact)

Authors Nicolas Lagaillardie , Ping Hou , Nobuko Yoshida



PDF
Thumbnail PDF

Artifact Description

DARTS.10.2.10.pdf
  • Filesize: 0.65 MB
  • 3 pages

Document Identifiers

Author Details

Nicolas Lagaillardie
  • Imperial College London, UK
Ping Hou
  • University of Oxford, UK
Nobuko Yoshida
  • University of Oxford, UK

Acknowledgements

We thank the anonymous reviewers for their useful comments and suggestions.

Cite AsGet BibTex

Nicolas Lagaillardie, Ping Hou, and Nobuko Yoshida. Fearless Asynchronous Communications with Timed Session Types in Rust (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.10

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Abstract

We introduce MultiCrusty^T, a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. MultiCrusty^T leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. This artifact allows to evaluate our approach by running examples from the literature, real-world use cases and protocols from real-time systems, featured in the related article, showcasing the correctness by construction of our approach. We allow to see the performance of our solution by running benchmarks and generating graphs, highlighting a less than 10% compile-time and runtime overhead compared with an untimed implementation. We also demonstrate how to implement, step by step, your own timed protocols, from a very basic one with only two parties and simple interactions, to complex ones with more than three parties, choices and recursion.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software usability
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Process calculi
Keywords
  • session types
  • affine types
  • π-calculus
  • asynchrony
  • timeouts
  • failures
  • Rust

Metrics

References

  1. Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida. Fearless asynchronous communications with timed multiparty session protocols, 2024. URL: https://arxiv.org/abs/2406.19541.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail