Search Results

Documents authored by Castro-Perez, David


Document
Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols

Authors: David Castro-Perez and Nobuko Yoshida

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)


Abstract
Multiparty Session Types (MPST) are a typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang. This paper proposes Dynamically Updatable Multiparty Session Protocols, a new MPST theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable. We prove that DMst guarantees deadlock-freedom and liveness. We implement a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

Cite as

David Castro-Perez and Nobuko Yoshida. Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{castroperez_et_al:LIPIcs.ECOOP.2023.6,
  author =	{Castro-Perez, David and Yoshida, Nobuko},
  title =	{{Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{6:1--6:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.6},
  URN =		{urn:nbn:de:0030-drops-181995},
  doi =		{10.4230/LIPIcs.ECOOP.2023.6},
  annote =	{Keywords: Multiparty Session Types, Correctness-by-construction, Concurrency, Golang}
}
Document
Artifact
Dynamically Updatable Multiparty Session Protocols (Artifact)

Authors: David Castro-Perez and Nobuko Yoshida

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)


Abstract
Multiparty Session Types (MPST) are typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang. This artifact contains an implementation of Dynamically Updatable Multiparty Session Protocols, a new MPST theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable. DMst guarantees deadlock-freedom and liveness. The artifact comprises a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate GoScr by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

Cite as

David Castro-Perez and Nobuko Yoshida. Dynamically Updatable Multiparty Session Protocols (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Article{castroperez_et_al:DARTS.9.2.10,
  author =	{Castro-Perez, David and Yoshida, Nobuko},
  title =	{{Dynamically Updatable Multiparty Session Protocols (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Castro-Perez, David and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.10},
  URN =		{urn:nbn:de:0030-drops-182505},
  doi =		{10.4230/DARTS.9.2.10},
  annote =	{Keywords: Multiparty Session Types, Correctness-by-construction, Concurrency, Golang}
}
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