Conversation-Based Governance for Distributed Systems by Multiparty Session Types
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
Software is increasingly organised centring on distributed communicating processes. This is especially true in large-scale distributed computing platforms such as the backend of popular Web-based services and public sector platforms for e-healthcare and e-science, which often provide lifelines of society. An application is organised as a dynamic collection of distributed components. The framework is based on interacting processes, which extends the traditional paradigm of functions and objects and which allows far more versatile and scalable organisation of software components.
Assuring safety in such distributed systems is a vital societal concern: many platforms are long-lived, offer socially critical services, and collect security-sensitive data; safety violations, including security breaches, can have wide-ranging consequences, from temporary service outage to information leakage to exploitation of security vulnerability by criminal organisations. However, existing assurance methodologies are based on objects and functions: no well-established formal assurance methodologies are known for distributed systems. Large-scale distributed computing infrastructures are like skyscrapers used by hundreds of thousands of people, for building which the well-established structural engineering principles are used as a foundation of safe engineering. Can we establish the corresponding engineering principles for building software skyscrapers vital to modern society?
Against this background, the central aim of this project is to establish a general, formally based safety assurance methodology for distributed systems, which we call conversation-based governance. The conversation-based governance starts from advanced types for capturing conversations, called multiparty session types (MPSTs), recently introduced by the PIs and extensively studied by researchers. Building on the latest theoretical results and on the PIs' ongoing collaborations with the project partners, we introduce the new development and assurance framework based on MPSTs. At the centre of our approach is a high-level, programming-language-agnostic MPST-based declarative protocol description language.
The safety assurance in this framework is realised through verifications of distributed components against formal specifications in this protocol language, performed either statically (at the development time) or dynamically (at runtime), of which we place an emphasis on the latter: large-scale distributed systems are rarely amenable to static verification as a whole due to, for example, heterogeneous components, so that only the dynamic verification and enforcement can offer a comprehensive safety assurance. It is due to this emphasis on runtime policing of conversations that we call the proposed assurance framework, conversation-based governance. The project will establish this new methodology through the following tasks:
(1) The development of a programing-language-agnostic protocol description language, called Scribble, and its open source tool chain, programming interfaces (APIs) and runtimes, backed up by a uniform type theory of MPSTs.
(2) The development of an assertion language for specifying and verifying refined safety properties as elaboration of protocols, together with a policy language linked to the assertion language. Decentralised monitors backed up by a theory of the pi-calculus offer efficient, scalable runtime verification and enforcement.
(3) Large-scale experiments through collaboration with project partners, realising formal safety assurance for real-world applications, including global cyberinfrastructure, enterprise software, and messaging middleware.
Throughout the project, an extensive dialogue between theories and practice will be conducted, leading to truly effective principles and tools for general safety assurance methodologies of distributed systems vital for future IT infrastructures and society.
Assuring safety in such distributed systems is a vital societal concern: many platforms are long-lived, offer socially critical services, and collect security-sensitive data; safety violations, including security breaches, can have wide-ranging consequences, from temporary service outage to information leakage to exploitation of security vulnerability by criminal organisations. However, existing assurance methodologies are based on objects and functions: no well-established formal assurance methodologies are known for distributed systems. Large-scale distributed computing infrastructures are like skyscrapers used by hundreds of thousands of people, for building which the well-established structural engineering principles are used as a foundation of safe engineering. Can we establish the corresponding engineering principles for building software skyscrapers vital to modern society?
Against this background, the central aim of this project is to establish a general, formally based safety assurance methodology for distributed systems, which we call conversation-based governance. The conversation-based governance starts from advanced types for capturing conversations, called multiparty session types (MPSTs), recently introduced by the PIs and extensively studied by researchers. Building on the latest theoretical results and on the PIs' ongoing collaborations with the project partners, we introduce the new development and assurance framework based on MPSTs. At the centre of our approach is a high-level, programming-language-agnostic MPST-based declarative protocol description language.
The safety assurance in this framework is realised through verifications of distributed components against formal specifications in this protocol language, performed either statically (at the development time) or dynamically (at runtime), of which we place an emphasis on the latter: large-scale distributed systems are rarely amenable to static verification as a whole due to, for example, heterogeneous components, so that only the dynamic verification and enforcement can offer a comprehensive safety assurance. It is due to this emphasis on runtime policing of conversations that we call the proposed assurance framework, conversation-based governance. The project will establish this new methodology through the following tasks:
(1) The development of a programing-language-agnostic protocol description language, called Scribble, and its open source tool chain, programming interfaces (APIs) and runtimes, backed up by a uniform type theory of MPSTs.
(2) The development of an assertion language for specifying and verifying refined safety properties as elaboration of protocols, together with a policy language linked to the assertion language. Decentralised monitors backed up by a theory of the pi-calculus offer efficient, scalable runtime verification and enforcement.
(3) Large-scale experiments through collaboration with project partners, realising formal safety assurance for real-world applications, including global cyberinfrastructure, enterprise software, and messaging middleware.
Throughout the project, an extensive dialogue between theories and practice will be conducted, leading to truly effective principles and tools for general safety assurance methodologies of distributed systems vital for future IT infrastructures and society.
Planned Impact
The project aims to establish a general and effective development, execution and safety assurance framework for distributed systems building on new structuring methods (conversations and protocols), backed up by formal theories. Embodied as concrete software tools, the proposed methodology will be tested extensively in actual distributed computing environments, giving continuous feedback to the theoretical and design-level development. If successful, the impact of the research will permeate many areas of computing and society in long years to come, as well as meeting some of their urgent needs.
(1) Who might benefit from this research?
The immediate beneficiaries are the development partners of this proposal and those in the related application domains, i.e. e-Science and oceanography (WP3-1), distributed enterprise applications (WP3-2), and scalable messaging middleware (WP3-3). Further once the tools and environments become usable, they also become usable by others, accompanied by open source tools and concrete use scenarios: there is an accelerating demand for developing large-scale applications centring on distributed communicating processes, especially in clouds. For these reasons we expect that those working on distributed systems including global enterprises, systems integration, public infrastructure (e.g. e-healthcare and e-Science) and cloud computing are among the likely beneficiaries in near future.
Finally the end-users and society as a whole will benefit from high-level software quality assurance provided by the proposed methodologies, especially users of infrastructural IT services providing lifeline support, quality of life and social welfare. For example, Ocean Observatories Initiative, a partner of this project (WP3-1), is building distributed observatories providing information from oceans, which is vital for climate change research.
(2) How might they benefit from this research?
First, with the development partners of this project, we carry out extensive experiment of the methodologies and tools from WP1/2, offering constant feedback to our development, leading to robust methodologies and tools truly usable by their developers in their environments. Since all partners are considering the usage of the methodologies in long terms much beyond the duration of this project (for example, the OOI CI has an operational time span of more than 30 years), and because the general principles developed in this project are not restricted to specific application domains but intended for all kinds of software based on distributed communicating processes, they can continue to leverage the fruits from the present collaboration and exploit their potential, leading to rapid accumulation of knowledge.
For the adoption of the proposed methodology beyond these partners, it is important that the methodology is built on a few general principles, distilled as theories, so that it is amenable to systematic teaching, training and extensions. Once their value is clear, any enterprise working on distributed computing environments (e.g. IBM, Microsoft, VMware, Red Hat, Google, and SAP) would be able to adopt them, and may even start to contribute to the enhancement of our open source tools or to provide their own counterparts, leading to the creation of a market for new generation of software tools and methodologies.
In the long term, we expect that the impact will reach the general public who use distributed infrastructures, through a wide adoption of the proposed methodology and its ramifications. Pronounced societal benefits will arise from a public standard for comprehensive certification framework on distributed applications based on the proposed methodologies, contributing to the safety guarantee for infrastructures such as financial networks and cyberinfrastructure for E-science (WP3-1), all of which offer critical services and knowledge to our society.
(1) Who might benefit from this research?
The immediate beneficiaries are the development partners of this proposal and those in the related application domains, i.e. e-Science and oceanography (WP3-1), distributed enterprise applications (WP3-2), and scalable messaging middleware (WP3-3). Further once the tools and environments become usable, they also become usable by others, accompanied by open source tools and concrete use scenarios: there is an accelerating demand for developing large-scale applications centring on distributed communicating processes, especially in clouds. For these reasons we expect that those working on distributed systems including global enterprises, systems integration, public infrastructure (e.g. e-healthcare and e-Science) and cloud computing are among the likely beneficiaries in near future.
Finally the end-users and society as a whole will benefit from high-level software quality assurance provided by the proposed methodologies, especially users of infrastructural IT services providing lifeline support, quality of life and social welfare. For example, Ocean Observatories Initiative, a partner of this project (WP3-1), is building distributed observatories providing information from oceans, which is vital for climate change research.
(2) How might they benefit from this research?
First, with the development partners of this project, we carry out extensive experiment of the methodologies and tools from WP1/2, offering constant feedback to our development, leading to robust methodologies and tools truly usable by their developers in their environments. Since all partners are considering the usage of the methodologies in long terms much beyond the duration of this project (for example, the OOI CI has an operational time span of more than 30 years), and because the general principles developed in this project are not restricted to specific application domains but intended for all kinds of software based on distributed communicating processes, they can continue to leverage the fruits from the present collaboration and exploit their potential, leading to rapid accumulation of knowledge.
For the adoption of the proposed methodology beyond these partners, it is important that the methodology is built on a few general principles, distilled as theories, so that it is amenable to systematic teaching, training and extensions. Once their value is clear, any enterprise working on distributed computing environments (e.g. IBM, Microsoft, VMware, Red Hat, Google, and SAP) would be able to adopt them, and may even start to contribute to the enhancement of our open source tools or to provide their own counterparts, leading to the creation of a market for new generation of software tools and methodologies.
In the long term, we expect that the impact will reach the general public who use distributed infrastructures, through a wide adoption of the proposed methodology and its ramifications. Pronounced societal benefits will arise from a public standard for comprehensive certification framework on distributed applications based on the proposed methodologies, contributing to the safety guarantee for infrastructures such as financial networks and cyberinfrastructure for E-science (WP3-1), all of which offer critical services and knowledge to our society.
Organisations
- Imperial College London (Lead Research Organisation)
- Pivotal Software, Inc (Collaboration)
- National Science Foundation (NSF) (Collaboration)
- VMware, Inc. (Collaboration)
- Cognizant Technology Solutions (Collaboration)
- Red Hat UK (Collaboration)
- November Group, LLC (Collaboration)
- University of California, San Diego (UCSD) (Collaboration)
- Estafet Ltd (Collaboration)
- Weaveworks Ltd (Collaboration)
- DELL (United States) (Project Partner)
- University of California, San Diego (Project Partner)
- Red Hat (United Kingdom) (Project Partner)
- Cognizant (United Kingdom) (Project Partner)
People |
ORCID iD |
Nobuko Yoshida (Principal Investigator) |
Publications
Imai K.
(2020)
Multiparty session programming with global protocol combinators
in Leibniz International Proceedings in Informatics, LIPIcs
Jones A V
(2013)
Imperial College Computing Student Workshop
King J
(2019)
Multiparty Session Type-safe Web Development with Static Linearity
in Electronic Proceedings in Theoretical Computer Science
Kouzapas D
(2017)
Characteristic bisimulation for higher-order session processes.
in Acta informatica
Kouzapas D
(2014)
Globally Governed Session Semantics
in Logical Methods in Computer Science
Kouzapas D
(2019)
On the relative expressiveness of higher-order session processes
in Information and Computation
Description | Some developers are interested in our research as they are potentially useful to software development. Session types are the analogue of data types for communication. A session type will again act as a fundamental unit of compositionality: the first thing a developer writes or reads about each process will be the session types of its communications, and session type discipline will guarantee that communications from different processes are in accord with the session type. This project has carried forward the above research programme with deep insights into the logical structure of session types, with a series of implementations in widely-used languages (including C, MPI, Erlang, Go, Haskell, Java, Python and F#) and in specialist languages for session types (such as Session C), and with collaborations with industry. Industrial applications of session types include the Scribble specification language maintained by Red Hat, the design of monitoring software used by the Ocean Observatories Initiative, and analysis of microservices carried out by ThoughtWorks and Estafet. We have disseminated our results through academic publication, by participating in summer schools, and by organising workshops. May 2014 - CoCo, Loch Lomond May 2014 - Shonan Workshop on Software Contracts for Communication, Monitoring, Security June 2014 - Graduate Course on Session Types, L'Aquila (Italy) June-July 2014 - BETTY Summer School, Lovan January 2014 - POPL 2014 Tutorial June 2015 - 15th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Multicore Programming, Bertinoro, Italy January 2016 - Lecture at 'Journées Francophones des Langages Applicatifs', JFLA 2016, Saint-Malo, France June-July 2016 BETTY Summer School, Limassol August 2016 - International Summer School on Metaprogramming, Cambridge August 2016, 2017 - University of Keio, Graduate School, Yokohama (Japan) January-February 2017 - Dagstuhl Workshop on Theory and Application of Behavioural Types November 2017 - FM Tutorial February 2018 - CGO Tutorial August 2018 - CONFESTA Conference |
Exploitation Route | Several prototype tools were published and used by both academia and industry. Including Scribble (FASE 2016, FASE 2017), Lchannels (ECOOP 2016), CoreSym (POPL 2015), GodelChecker (POPL 2017, ICSE 2018) and Session Type Providers (CC 2018). The joint-development of Scribble continues with RedHat, and they will eventually consider to integrate their existing projects. For more details of other tools please see http://mrg.doc.ic.ac.uk/tools/. |
Sectors | Communities and Social Services/Policy Digital/Communication/Information Technologies (including Software) Education Environment Financial Services and Management Consultancy Security and Diplomacy |
URL | http://mrg.doc.ic.ac.uk/publications/ |
Description | Applications to OpenTelemetry tracing tool, and Scribble tools. |
First Year Of Impact | 2022 |
Sector | Digital/Communication/Information Technologies (including Software),Education,Financial Services, and Management Consultancy |
Impact Types | Policy & public services |
Description | Cognizant |
Organisation | Cognizant Technology Solutions |
Country | United States |
Sector | Private |
PI Contribution | Collaboration with Cognizant and Estafet applied Scribble developed by Imperial in a microservice environment. |
Collaborator Contribution | Our partners proposes to use Scribble in their product. |
Impact | There is an ongoing dialogue on using Scribble in the partner's products, including ZDLC https://www.cognizant.com/ZDLC. |
Start Year | 2013 |
Description | Development of the Scribble language and framework |
Organisation | Cognizant Technology Solutions |
Country | United States |
Sector | Private |
PI Contribution | Developing an open source product. |
Collaborator Contribution | Providing use cases, technical meetings, and hosting KTS. |
Impact | TBD |
Start Year | 2013 |
Description | Development of the Scribble language and framework |
Organisation | Red Hat UK |
Country | United Kingdom |
Sector | Private |
PI Contribution | Developing an open source product. |
Collaborator Contribution | Providing use cases, technical meetings, and hosting KTS. |
Impact | TBD |
Start Year | 2013 |
Description | Development of the Scribble language and framework |
Organisation | University of California, San Diego (UCSD) |
Country | United States |
Sector | Academic/University |
PI Contribution | Developing an open source product. |
Collaborator Contribution | Providing use cases, technical meetings, and hosting KTS. |
Impact | TBD |
Start Year | 2013 |
Description | Development of the Scribble language and framework |
Organisation | VMware, Inc. |
Country | United States |
Sector | Private |
PI Contribution | Developing an open source product. |
Collaborator Contribution | Providing use cases, technical meetings, and hosting KTS. |
Impact | TBD |
Start Year | 2013 |
Description | Estafet |
Organisation | Estafet Ltd |
Country | United Kingdom |
Sector | Private |
PI Contribution | Implementation of microservices monitoring based on Scribble. |
Collaborator Contribution | Technical discussions and collaboration on partner's product. |
Impact | A product based on monitor generation for microservices based on the Scribble framework was proposed. See http://estafet.com/scribble-3/. |
Start Year | 2016 |
Description | November Group, LLC |
Organisation | November Group, LLC |
Country | United States |
Sector | Private |
PI Contribution | Ongoing discussions with the partners on applications of Scribble developed at Imperial with logical assertions, and applying the technology to specify and verify smart contract on a block-chain. |
Collaborator Contribution | Use cases for session types and Scribble. |
Impact | . |
Start Year | 2013 |
Description | Ocean Observatories Intiative Cyber Infrastructure project |
Organisation | National Science Foundation (NSF) |
Department | Ocean Observatories Initiative |
Country | United States |
Sector | Charity/Non Profit |
PI Contribution | The collaboration explored using Scribble developed at Imperial to formally specify OOI Cyber Infrastructure (OOI CI). |
Collaborator Contribution | A number of use cases for Scribble were contributed by the partners for Scribble development. |
Impact | A runtime monitoring framework based on Scribble was developed, leading to publications in PLACES'13, RV 2013, FMSD, and the monitoring prototype integrated in the OOI CI framework (https://github.com/ooici/pyon/tree/pyon-conversations) |
Start Year | 2011 |
Description | Pivotal |
Organisation | Pivotal Software, Inc |
Country | United States |
Sector | Private |
PI Contribution | Research on dynamic verification based on session types. |
Collaborator Contribution | Technical meetings and use cases of session types. |
Impact | Erlang and python (celery) message passing middleware were the resulting tools implemented following the discussions. The implementations led to a number of publications in RV 2013, COORDINATION 2014 and LMCS in 2017. |
Start Year | 2013 |
Description | RedHat |
Organisation | Red Hat UK |
Country | United Kingdom |
Sector | Private |
PI Contribution | Development of open source software Scribble |
Collaborator Contribution | Collaborations, software development, technical discussion and meetings |
Impact | The open source tool Scribble is available online at https://github.com/scribble/scribble-java. The software led to a number of publications in international conference such as FASE 2016, FASE 2017, ECOOP 2016 and ECOOP 2017. |
Start Year | 2013 |
Description | Weaveworks |
Organisation | Weaveworks Ltd |
Country | United States |
Sector | Private |
PI Contribution | There is an ongoing discussions on the topics of distributed containers and Kubernetes development and configurations, as well as recent applications of session types in Go. |
Collaborator Contribution | Use cases of session types. |
Impact | . |
Start Year | 2013 |
Title | A sound algorithm for asynchronous session subtyping |
Description | This is an implementation of the algorithm given in the paper A Sound Algorithm for Asynchronous Session Subtyping (CONCUR'19) by Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. |
Type Of Technology | Software |
Year Produced | 2019 |
Impact | Led to a publication at CONCUR 19 |
URL | https://github.com/julien-lange/asynchronous-subtyping |
Title | Armus |
Description | Armus is a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs. |
Type Of Technology | Software |
Year Produced | 2015 |
Impact | Led to a publication at PPoPP 2015 and one at TOPLAS 2019 |
URL | https://bitbucket.org/cogumbreiro/armus/wiki/Home |
Title | Armus |
Description | Armus is a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs. |
Type Of Technology | Software |
Year Produced | 2015 |
Impact | Led to a publication in PPoPP'15. |
URL | https://bitbucket.org/cogumbreiro/armus/wiki/PPoPP15 |
Title | Artifact: Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types |
Description | Artifact of the paper: "Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types", PPoPP 2022. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | The Rumpsteak framework is a framework for MPST in Rust. This software is an artifact that shows its capabilities. |
URL | https://zenodo.org/record/5786034 |
Title | Artifact: Design-By-Contract for Flexible Multiparty Session Protocols |
Description | Artifact for the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.21 |
Title | Artifact: Dynamically Updatable Multiparty Session Protocols |
Description | Artifact for the paper: Dynamically Updatable Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Dynamically Updatable Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.10 |
Title | Artifact: Generalised Multiparty Session Types with Crash-Stop Failures |
Description | Artifact supporting the paper : Generalised Multiparty Session Types with Crash-Stop Failures |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for the paper : https://github.com/alcestes/mpstk-crash-stop |
URL | https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35 |
Title | Artifact: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Description | Artifact for paper: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for paper : Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
URL | https://dl.acm.org/doi/10.1145/3563331 |
Title | Artifact: Rollback Recovery in Session-Based Programming |
Description | Artifact for paper: Rollback Recovery in Session-Based Programming |
Type Of Technology | Software |
Year Produced | 2023 |
Impact | Artifact for paper: Rollback Recovery in Session-Based Programming |
URL | https://link.springer.com/chapter/10.1007/978-3-031-35361-1_11#chapter-info |
Title | Artifact: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types |
Description | Artifact for the paper: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (https://doi.org/10.4230/DARTS.8.2.9) This introduces the `multicrusty` library. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper. |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9 |
Title | BitML |
Description | A domain-specific language for smart contracts with a computationally sound embedding into Bitcoin |
Type Of Technology | Software |
Year Produced | 2019 |
Impact | Led to a publication at ESEC/FSE 2019 |
URL | https://github.com/bitml-lang |
Title | CAMP: Cost-Aware Multiparty Session Protocols (artifact) |
Description | This is the artifact for the paper *CAMP: Cost-Aware Multiparty Session Protocols*.
The artifact comprises: - A library for specifying cost-aware multiparty protocols. - The raw data used for comparing the cost models with real execution costs. - The cost-aware protocol specifications of the benchmarks that we studied. The library for specifying cost-aware protocols also provides functions for extracting cost equations from them, and for estimating recursive protocol latencies (i.e. average cost per protocol iteration). We provide a script for extracting cost equations, and instantiating them using the parameters used in the paper. |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
URL | https://zenodo.org/record/4046892 |
Title | CAMP: Cost-Aware Multiparty Session Protocols (artifact) |
Description | This is the artifact for the paper *CAMP: Cost-Aware Multiparty Session Protocols*.
The artifact comprises: - A library for specifying cost-aware multiparty protocols. - The raw data used for comparing the cost models with real execution costs. - The cost-aware protocol specifications of the benchmarks that we studied. The library for specifying cost-aware protocols also provides functions for extracting cost equations from them, and for estimating recursive protocol latencies (i.e. average cost per protocol iteration). We provide a script for extracting cost equations, and instantiating them using the parameters used in the paper. |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
Impact | Led to a publication to OOPSLA 2020. |
URL | https://zenodo.org/record/4046893 |
Title | Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact) |
Description | We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop fail- ures 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 execut- able 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. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Designing Asynchronous Multiparty Protocols with Crash-Stop Failures |
URL | https://zenodo.org/record/7974824 |
Title | DinGoHunter |
Description | This is a static analyser to model concurrency and find deadlocks in Go code. The main purpose of this tool is to infer from Go source code its concurrency model in either of the two formats: Communicating Finite State Machines (CFSMs) and MiGo types. The inferred models are then passed to separate tools for formal analysis. In both approaches, we apply a system known in the literature as Session Types to look for potential communication mismatches to preempt potential deadlocks. |
Type Of Technology | Software |
Year Produced | 2015 |
Open Source License? | Yes |
Impact | Led to publications in CC2016, and POPL 2017, as well as a book chapter in "Behavioural Types: from Theory to Tools" |
URL | https://github.com/nickng/dingo-hunter |
Title | EMTST |
Description | A Coq library to implement and reason about Session types. Together with a subject reduction for binary session types. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at TACAS 2020 |
URL | https://doi.org/10.5281/zenodo.3516299 |
Title | Effect-Sessions |
Description | This tool implements the embedding of session types into Haskell, via an effect system encoding. |
Type Of Technology | Software |
Year Produced | 2016 |
Open Source License? | Yes |
Impact | Led to a publication at POPL'2016 |
URL | https://www.doc.ic.ac.uk/~dorchard/popl16/ |
Title | Effpi |
Description | Effpi is an experimental toolkit for strongly-typed message-passing programs in Dotty (a.k.a. the future Scala 3 programming language), with verification capabilities based on type-level model checking. |
Type Of Technology | Software |
Year Produced | 2019 |
Impact | Led to publications at Scala Symposium 2019 (tool paper) and PLDI 2019 |
URL | https://alcestes.github.io/effpi/ |
Title | Featherweight Go (Artifact) |
Description | This paper presents Featherweight Go (FG) and Featherweight Generic Go (FGG), a core calculus of Go and a proposal for extending it with F-bounded polymorphism. The calculi are in the same vein as Featherweight Java (FJ), but where Featherweight Generic Java (FGJ) was translated into FJ via erasure, FGG translates into FG via monomorphization (which is also formalized). The two calculi are proven sound using the normal progress and preservation arguments. Additionally a bisimulation is shown to exist between a FGG program and its monomorphization (if it exists); in other words that monomorphization preserves the semantics of the program. The artifact consists of an implementation of type checkers and interpreters for FG and FGG, as well as a monomorphization procedure (including the check if it is possible). It includes the examples from the paper, and a comparison using the Go compiler as reference. Type preservation and bisimulation for these programs are tested dynamically. Additionally, the same is tested for all well-typed programs up to a certain size (which are generated in a manner similar to property-based testing). |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
Impact | Led to a publication at OOPSLA 2020 |
URL | https://zenodo.org/record/4048297 |
Title | GMC Syn |
Description | The tool allows to - Check that a set of CFSM is Generalised Multiparty Compatible (GMC) - Synthesise a choreography (global graph) which is equivalent to the input CFSMs. |
Type Of Technology | Software |
Year Produced | 2017 |
Impact | Led to publications at POPL 2015 and CC 2016, as well as a book chapter in "Behavioural Types: from Theory to Tools". |
URL | https://bitbucket.org/julien-lange/gmc-synthesis/wiki/Home |
Title | Godel Checker |
Description | godel-checker is a model checker for MiGo types, and uses the output of the MiGo type extractor gospal. This tool is part of the Go static verification framework described in this work. |
Type Of Technology | Software |
Year Produced | 2018 |
Impact | Led to a publication at ICSE 2018 |
URL | https://bitbucket.org/MobilityReadingGroup/godel-checker |
Title | Godel2 |
Description | Godel2 is a model checker for MiGo types that returns results of liveness and safety checks for channels and mutex locks, as well as the presence of data races on shared pointers. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at ECOOP 2020 |
Title | Gong |
Description | Gong is a liveness and safety checker for MiGo types. |
Type Of Technology | Software |
Year Produced | 2016 |
Impact | Led to a publication at POPL 2017 |
URL | https://github.com/nickng/gong |
Title | KMC |
Description | A tool for checking k-multiparty compatibility in communicating session automata |
Type Of Technology | Software |
Year Produced | 2019 |
Impact | Led to a publication at CAV 2019 |
URL | https://bitbucket.org/julien-lange/k-checking |
Title | Lchannels |
Description | lchannels is a Scala library for type-safe session programming. It provides linear I/O channels, which allow to transfer data locally, or over a network. Its API allows to - define protocols, represented as a set of continuation-passing style classes, and - easily write programs that interact according to such protocols The Scala type checker can examine the resulting code and spot many protocol violations at compile time. |
Type Of Technology | Software |
Year Produced | 2017 |
Impact | Led to publications at ECOOP'16 and ECOOP'17 |
URL | http://alcestes.github.io/lchannels/ |
Title | Multiparty Motion Coordination: From Choreographies to Robotics Programs (Artifact) |
Description | Software artifact for the paper "Multiparty Motion Coordination: From Choreographies to Robotics Programs" submitted to OOPSLA 2020 The artifact has been packaged into a virtual machine (Ubuntu 20.04). The username and password for the virtual machine is "pgcd". |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
Impact | Led to a publication at OOPSLA 2020 |
URL | https://zenodo.org/record/4051783 |
Title | NuScr - An implementation of MPST toolchain in OCaml |
Description | Multiparty session types (MPST) provide a typing discipline for message-passing concurrency, ensuring deadlock freedom for distributed processes. We present NuScr (Nu-Scribble), an extensible toolchain, implemented in OCaml, for MPST-based protocols. The toolchain can convert multiparty protocols in the Scribble protocol description language into global types in the MPST theory; global types are projected into local types, and local types are converted to their corresponding communicating finite state machine (CFSM). The toolchain also generates OCaml APIs from CFSMs, which implement endpoints in the protocol. Our design allows for language-independent code generation, and opens possibilities to generate APIs for other programming languages. We design our toolchain with modularity and extensibility in mind, so that extensions of core MPST can be easily integrated within our framework. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | The NuScr toolchain has a modular and extensible design, so that extensions of core MPST can be easily integrated within our framework. |
URL | https://nuscr.github.io/nuscr/ |
Title | Pabble |
Description | Pabble is a parametric extension of Scribble primarily designed for describing communication protocols in parallel computing. |
Type Of Technology | Software |
Year Produced | 2015 |
Impact | Led to publications at CC'2015, SOCA, PDP'2014 and a chapter in the book "Behavioural Types: from Theory to Tools" |
URL | http://www.doc.ic.ac.uk/~cn06/parameterised-scribble/ |
Title | Parallel Algebraic Language |
Description | A Haskell EDSL for building session-typed parallel code. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at CC 2020. |
Title | STScript |
Description | STScript is a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets using routed MPST (RouST). STScript uses TypeScript, ReactJS, and NodeJS as an implementation language, client framework and server framework respectively. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at CC 2021. |
Title | Savara |
Description | Testable Architecture developed with Cognizant |
Type Of Technology | Software |
Year Produced | 2014 |
Open Source License? | Yes |
Impact | Industry product |
URL | http://savara.jboss.org/ |
Title | Scribble |
Description | Scribble is a language to describe application-level protocols among communicating systems. A protocol represents an agreement on how participating systems interact with each other. Without a protocol, it is hard to do meaningful interaction: participants simply cannot communicate effectively, since they do not know when to expect the other parties to send data, or whether the other party is ready to receive data. However, having a description of a protocol has further benefits. It enables verification to ensure that the protocol can be implemented without resulting in unintended consequences, such as deadlocks. |
Type Of Technology | Software |
Year Produced | 2018 |
Open Source License? | Yes |
Impact | Used by several industry partners. |
URL | http://www.scribble.org/ |
Title | Scribble-Go |
Description | Scribble-Go is a toolchain for safe distributed programming using role-parametric session types in Go. It extends Scribble, a toolchain for safe distributed programming using basic (non-role-parametric) session types in Java, with support for role-parametricity and support for Go. |
Type Of Technology | Software |
Year Produced | 2019 |
Impact | Led to a publication at POPL 2019 |
URL | http://mrg.doc.ic.ac.uk/tools/scribble-go/ |
Title | Session Actor |
Description | Session Actor is an actor framework in Python with support for session types. An actor can implement multiple session types (roles) in a similar way as an object can implement multiple interfaces. The framework supports automatic discovery of roles and runtime checks for protocol compliance. |
Type Of Technology | Software |
Year Produced | 2017 |
Impact | Led to a publication at COORDINATION 2014 and LMCS'17. |
URL | https://github.com/rumineykova/sessionactors |
Title | Session Erlang |
Description | We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. A recovered communication system is free from deadlocks, orphan messages and reception er- rors. Here we present an erlang API for programming with gen_server. |
Type Of Technology | Software |
Year Produced | 2017 |
Impact | Led to a publication in CC'17. |
URL | https://gitlab.doc.ic.ac.uk/rn710/codeINspire |
Title | Session Type Provider |
Description | STP is a type provider for F# that generates APIs from protocol specifications |
Type Of Technology | Software |
Year Produced | 2018 |
Impact | Led to a publication at CC 2018 |
URL | https://session-type-provider.github.io/ |
Title | Session* |
Description | Session* is a toolchain for specifying message passing protocols using Refined Multiparty Session Types and safely implementing the distributed endpoint programs in F*. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at OOPSLA 2020. |
Title | ZDLC |
Description | ZDLC IT Knowledge Automation reverse-engineers process flows, data lineage and business rules from the running systems, automatically captures the business's operational user interface activity and aligns these together. The power of ZDLC automation makes accurate, up-to-date and unambiguous IT knowledge affordable, enabling organizations to deliver with more agility, precision and cost-effectiveness. |
Type Of Technology | Software |
Year Produced | 2018 |
Impact | Used in the industry |
URL | https://www.cognizant.com/ZDLC |
Title | Zooid: a DSL for Certified Multiparty Computation |
Description | Artifact for the Zooid language and Coq mechanisation of the metathory of multiparty session types. This artifact contains the implementation for "Zooid: a DSL for Certified Multiparty Computation" from PLDI'21 This code is maintained at: https://github.com/emtst/zooid-cmpst |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | See: http://mrg.doc.ic.ac.uk/publications/zooid-paper/ |
URL | https://zenodo.org/record/4581294 |
Title | codeINspire - Let it recover: Multiparty Protocol Induced Recovery |
Description | This is an Erlang API for programming with gen_server. We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. A recovered communication system is free from deadlocks, orphan messages and reception errors. |
Type Of Technology | Software |
Year Produced | 2017 |
Impact | Led to a publication at CC 2017. |
Title | dot-parser |
Description | A parser for DOT files in Rust |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | No such parser previously existed in Rust. This is used for the developement of the Rumpsteak framework. |
URL | https://crates.io/crates/dot-parser |
Title | mpstk - the Multiparty Session Types toolKit |
Description | mpstk is a toolkit for specifying multiparty protocols and verifying their properties (e.g., deadlock-freedom and liveness). |
Type Of Technology | Software |
Year Produced | 2019 |
Impact | Led to a publication at POPL 2019 |
URL | https://alcestes.github.io/mpstk/ |
Title | mpstpp |
Description | Multiparty Session Types Plus + |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at ESOP 2020 |
Title | ocaml-mpst |
Description | ocaml-mpst is a communication library powered by Multiparty Session Types (abbreviated as MPST) in OCaml. Thus it ensures: * Deadlock-freedom, * Protocol fidelity (communication will take place according to a prescribed protocol) and * Communication safety (you do not get any type-mismatch errors) --- under the assumption that all communication channels are used linearly. |
Type Of Technology | Software |
Year Produced | 2020 |
Impact | Led to a publication at ECOOP 2020 |
Title | session-ocaml |
Description | Session-ocaml is a novel library for concurrent / distributed programming in OCaml featuring session types. The characteristics of it includes: - Statically checked, multiple simultaneous sessions. - The novel protocol types which provide a clear describtion of concurrent services. -- Type inference. -- Labelled branching and recursion, effectively represented using polymorphic variants in OCaml. -- Delegation enables a ongoing session to be passed around threads. |
Type Of Technology | Software |
Year Produced | 2017 |
Impact | Led to a publication in Science of Computer Programming. |
URL | https://keigoimai.info/session-ocaml/ |