6 Search Results for "Zhou, Fangyi"

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.1
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

Authors: Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou

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

Abstract
Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types (MPST) with crash-stop semantics to support failure handling protocols. We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock-freedom, protocol conformance, and liveness of typed processes in the presence of crashes. Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scribble multiparty protocol language to generate protocol-conforming Scala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.
Cite as

Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barwell_et_al:LIPIcs.ECOOP.2023.1,
  author =	{Barwell, Adam D. and Hou, Ping and Yoshida, Nobuko and Zhou, Fangyi},
  title =	{{Designing Asynchronous Multiparty Protocols with Crash-Stop Failures}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{1:1--1: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.1},
  URN =		{urn:nbn:de:0030-drops-181944},
  doi =		{10.4230/LIPIcs.ECOOP.2023.1},
  annote =	{Keywords: Session Types, Concurrency, Failure Handling, Code Generation, Scala}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.9
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)

Authors: Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou

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

Abstract
We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop failures and crash-handling behaviours. Teatrino accompanies the novel MPST theory in the related article, and enables users to generate fault-tolerant protocol-conforming Scala code from Scribble protocols. Local types are projected from the global protocol, enabling correctness-by-construction, and are expressed directly as Scala types via the Effpi concurrency library. Teatrino extends both Scribble and Effpi with support for crash-stop behaviour. The generated Scala code is executable and can be further integrated with existing systems. The accompanying theory in the related article guarantees deadlock-freedom and liveness properties for failure handling protocols and their implementation. This artifact includes examples, extended from both session type and distributed systems literature, featured in the related article.
Cite as

Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 9:1-9:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{barwell_et_al:DARTS.9.2.9,
  author =	{Barwell, Adam D. and Hou, Ping and Yoshida, Nobuko and Zhou, Fangyi},
  title =	{{Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)}},
  pages =	{9:1--9:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Barwell, Adam D. and Hou, Ping and Yoshida, Nobuko and Zhou, Fangyi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.9.2.9},
  URN =		{urn:nbn:de:0030-drops-182492},
  doi =		{10.4230/DARTS.9.2.9},
  annote =	{Keywords: Session Types, Concurrency, Failure Handling, Code Generation, Scala}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.35
Generalised Multiparty Session Types with Crash-Stop Failures

Authors: Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature.
Cite as

Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 35:1-35:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{barwell_et_al:LIPIcs.CONCUR.2022.35,
  author =	{Barwell, Adam D. and Scalas, Alceste and Yoshida, Nobuko and Zhou, Fangyi},
  title =	{{Generalised Multiparty Session Types with Crash-Stop Failures}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{35:1--35:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35},
  URN =		{urn:nbn:de:0030-drops-170982},
  doi =		{10.4230/LIPIcs.CONCUR.2022.35},
  annote =	{Keywords: Session Types, Concurrency, Failure Handling, Model Checking}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.21
Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)

Authors: Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We introduce CAScr, the first implementation of Scribble (http://www.scribble.org, https://nuscr.dev/) that relies on choreography automata, for deadlock-free distributed programming. CAScr supports the main theoretical results and constructions in the related article. CAScr takes the popular top-down approach to system development, based on choreographic models, following the original methodology of Scribble and multiparty session types. The top-down approach enables correctness-by-construction: a developer provides a global description for the whole communication protocol; by projecting the global protocol, APIs are generated from local CFSMs, which ensure the safe implementation of each participant. The theory of choreography automata in the related article guarantees deadlock freedom for the distributed implementation of flexible global protocols. We target web development, supporting in particular the TypeScript programming language.
Cite as

Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-Contract for Flexible Multiparty Session Protocols (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{gheri_et_al:DARTS.8.2.21,
  author =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  title =	{{Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)}},
  pages =	{21:1--21:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.21},
  URN =		{urn:nbn:de:0030-drops-162196},
  doi =		{10.4230/DARTS.8.2.21},
  annote =	{Keywords: Choreography automata, design by contract, deadlock freedom, Communicating Finite State Machines, TypeScript programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.8
Design-By-Contract for Flexible Multiparty Session Protocols

Authors: Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.
Cite as

Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-By-Contract for Flexible Multiparty Session Protocols. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 8:1-8:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gheri_et_al:LIPIcs.ECOOP.2022.8,
  author =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  title =	{{Design-By-Contract for Flexible Multiparty Session Protocols}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{8:1--8:28},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.8},
  URN =		{urn:nbn:de:0030-drops-162367},
  doi =		{10.4230/LIPIcs.ECOOP.2022.8},
  annote =	{Keywords: Choreography automata, design by contract, deadlock freedom, Communicating Finite State Machines, TypeScript programming}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.12
Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)

Authors: Julia Gabet and Nobuko Yoshida

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
This artifact contains a version of the Godel tool that checks MiGo+ types - an extension of MiGo from [Lange et al., 2018] including GoL. Given the extracted MiGo+ types, the tool can analyse them using the mCRL2 model checker to check several properties including liveness, safety and data race freedom as defined in our paper. The artifact also includes examples, shipped with both the source of the Godel tool and the benchmark repository. The latter also contains the Go source for the benchmark examples. We provide compiled binaries of the artifact in a Docker image, with instructions on how to use them. Finally, for convenience, the Docker image also contains a binary version of the migoinfer+ tool, developed as a fork from the original migoinfer by Nicholas Ng in [Lange et al., 2018]. This new version adds the ability to extract shared memory pointers as well as Mutex and RWMutex locks.
Cite as

Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{gabet_et_al:DARTS.6.2.12,
  author =	{Gabet, Julia and Yoshida, Nobuko},
  title =	{{Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)}},
  pages =	{12:1--12:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Gabet, Julia and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.6.2.12},
  URN =		{urn:nbn:de:0030-drops-132096},
  doi =		{10.4230/DARTS.6.2.12},
  annote =	{Keywords: Go language, behavioural types, race detection, happens-before relation, safety, liveness}
}
  • Refine by Author
  • 6 Yoshida, Nobuko
  • 3 Barwell, Adam D.
  • 3 Zhou, Fangyi
  • 2 Gheri, Lorenzo
  • 2 Hou, Ping
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Distributed computing models
  • 4 Theory of computation → Process calculi
  • 3 Software and its engineering → Concurrent programming languages
  • 2 Software and its engineering → Formal software verification
  • 2 Software and its engineering → Model checking
  • Show More...

  • Refine by Keyword
  • 3 Concurrency
  • 3 Failure Handling
  • 3 Session Types
  • 2 Choreography automata
  • 2 Code Generation
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2022
  • 2 2023
  • 1 2020

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact