Turtles: Protocol-Based Foundations for Distributed Multiagent Systems
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
There is growing interest in distributed systems and architectures whose components are autonomous social parties such as humans and organisations. The parties in such systems interact with each other via their software agents for the purposes of exchanging information and services. The interactions normally take the form of conversations (as opposed to invocations) realised over asynchronous messaging. Naturally, a crucial area of study for computer science and software engineering is the specification and enactment of interaction protocols, that is, the rules of encounter by which parties in the system would interact. Considered as such, the notion of protocol represents a generalisation of the notion of "contract" advocated in Design by Contract approaches.
A key question concerns the nature of contracts. Work in areas such as concurrency and Web services, has predominantly conceptualised protocols in terms of message ordering and occurrence constraints that must be respected by the parties' agents. We refer to such protocols as messaging protocols. Although messaging protocols serve the important purpose of distributed coordination, considered as contracts, they are too low-level for multiagent settings of autonomous parties. Specifically, they do not capture social constraints such as the commitments that are binding on the parties in the interaction.
This gap represents a substantial opportunity. In real life, commitments in fact represent the atoms of what people normally understand as contracts. Commitments accommodate the balance between, on the one hand, autonomy and flexibility, and, on the other hand, correct behaviour. Commitment specifications capture stakeholder requirements in multiparty domains. Further, the states of commitments underlie most key performance indicators (KPIs) that stakeholders are interested in any multiagent domain. Work in commitment protocols in multiagent systems has made progress in developing computational abstractions for commitments. However, important challenges related to expressiveness and distributed enactment of commitment protocols have not even been adequately formulated, let alone tackled. Ensuring correct distributed enactment for expressive commitment protocols is crucial to realising the full value of commitments as a human-level architectural abstraction.
The broad objective of Turtles is to bring commitment-based contracts to distributed computing. This project develops foundational theory, software, and methodology for building commitment-based distributed systems. To encourage wider adoption, the project will embed the algorithms in prototypes, and develop a tool-supported methodology for specifying and implementing social protocols. Further, Turtles will develop real systems based on use cases and practices from a number of industrial partners and evaluate these systems based on their feedback.
The success of Turtles will enable capturing important subtleties of real-life social and business interactions and transform how we design software systems for crucial multiparty domains such as healthcare, disaster response, smart cities, banking, education, and e-commerce and e-business, where commitments are crucial.
A key question concerns the nature of contracts. Work in areas such as concurrency and Web services, has predominantly conceptualised protocols in terms of message ordering and occurrence constraints that must be respected by the parties' agents. We refer to such protocols as messaging protocols. Although messaging protocols serve the important purpose of distributed coordination, considered as contracts, they are too low-level for multiagent settings of autonomous parties. Specifically, they do not capture social constraints such as the commitments that are binding on the parties in the interaction.
This gap represents a substantial opportunity. In real life, commitments in fact represent the atoms of what people normally understand as contracts. Commitments accommodate the balance between, on the one hand, autonomy and flexibility, and, on the other hand, correct behaviour. Commitment specifications capture stakeholder requirements in multiparty domains. Further, the states of commitments underlie most key performance indicators (KPIs) that stakeholders are interested in any multiagent domain. Work in commitment protocols in multiagent systems has made progress in developing computational abstractions for commitments. However, important challenges related to expressiveness and distributed enactment of commitment protocols have not even been adequately formulated, let alone tackled. Ensuring correct distributed enactment for expressive commitment protocols is crucial to realising the full value of commitments as a human-level architectural abstraction.
The broad objective of Turtles is to bring commitment-based contracts to distributed computing. This project develops foundational theory, software, and methodology for building commitment-based distributed systems. To encourage wider adoption, the project will embed the algorithms in prototypes, and develop a tool-supported methodology for specifying and implementing social protocols. Further, Turtles will develop real systems based on use cases and practices from a number of industrial partners and evaluate these systems based on their feedback.
The success of Turtles will enable capturing important subtleties of real-life social and business interactions and transform how we design software systems for crucial multiparty domains such as healthcare, disaster response, smart cities, banking, education, and e-commerce and e-business, where commitments are crucial.
Planned Impact
We list the potential beneficiaries and summarise the potential impact on each of them. (Please also see Pathways to Impact.)
KNOWLEDGE:
Researchers: Turtles will contribute foundational scientific knowledge crucial to building distributed systems of multiple parties. This will enable bringing together the currently distinct communities of programming languages and multiagent systems and lead to the formation of joint new communities and agendas based on computational social abstractions. The impact on service-oriented computing and business process management will also be profound.
Software developers: Turtles will contribute knowledge toward the development of systems that support business interactions within and across organisations. This knowledge will improve communication with stakeholders, and simplify the development and maintenance of such systems.
Stakeholders: Turtles will contribute knowledge that enables stakeholders to understand requirements and key performance indicators in terms of commitments, and to relate these artifacts to software.
PEOPLE:
Researchers and students: Turtles will train PDRAs and PhD students working on related projects. The project's results will also inform undergraduate and graduate students via courses and tutorials.
Software developers and stakeholders: Turtles will train software developers and stakeholders via the substantial engagement with our partners.
Protocol analysts: In the medium-to-long run, we envisage the emergence of a new class of professionals called protocol analysts, who will be experts in specifying, analysing, and implementing social protocols.
SOCIETAL:
Standards bodies: Standardisation is key to better interoperability and therefore better services in important societal domains such as healthcare, smart cities, energy, and so on. Standardisation efforts are enormously complex and standards are often not adopted. Sometimes, the reason for this is due to unclear and complex specifications. Turtles will simplify the creation of protocol-based standards via a formal, tool-supported language that enables expressing both the messaging and high-level concerns.
ECONOMIC:
Business ecosystems: Via easier standardisation, Turtles will support the proliferation of business ecosystems consisting of stakeholders, including government, and developers in many multiparty domains. This will lead to reduced implementation costs and increased business engagements via better interoperability. To give a concrete example, RosettaNet is used by Intel and other companies to conduct billions of dollars worth of business. A study showed that adopting the RosettaNet protocols reduced transaction costs and increased throughput (http://tinyurl.com/p38nc7r). A healthcare study postulated billions of dollars worth of savings for the United States both during protocol implementation and post-implementation periods (http://tinyurl.com/o7sv8y6).
KNOWLEDGE:
Researchers: Turtles will contribute foundational scientific knowledge crucial to building distributed systems of multiple parties. This will enable bringing together the currently distinct communities of programming languages and multiagent systems and lead to the formation of joint new communities and agendas based on computational social abstractions. The impact on service-oriented computing and business process management will also be profound.
Software developers: Turtles will contribute knowledge toward the development of systems that support business interactions within and across organisations. This knowledge will improve communication with stakeholders, and simplify the development and maintenance of such systems.
Stakeholders: Turtles will contribute knowledge that enables stakeholders to understand requirements and key performance indicators in terms of commitments, and to relate these artifacts to software.
PEOPLE:
Researchers and students: Turtles will train PDRAs and PhD students working on related projects. The project's results will also inform undergraduate and graduate students via courses and tutorials.
Software developers and stakeholders: Turtles will train software developers and stakeholders via the substantial engagement with our partners.
Protocol analysts: In the medium-to-long run, we envisage the emergence of a new class of professionals called protocol analysts, who will be experts in specifying, analysing, and implementing social protocols.
SOCIETAL:
Standards bodies: Standardisation is key to better interoperability and therefore better services in important societal domains such as healthcare, smart cities, energy, and so on. Standardisation efforts are enormously complex and standards are often not adopted. Sometimes, the reason for this is due to unclear and complex specifications. Turtles will simplify the creation of protocol-based standards via a formal, tool-supported language that enables expressing both the messaging and high-level concerns.
ECONOMIC:
Business ecosystems: Via easier standardisation, Turtles will support the proliferation of business ecosystems consisting of stakeholders, including government, and developers in many multiparty domains. This will lead to reduced implementation costs and increased business engagements via better interoperability. To give a concrete example, RosettaNet is used by Intel and other companies to conduct billions of dollars worth of business. A study showed that adopting the RosettaNet protocols reduced transaction costs and increased throughput (http://tinyurl.com/p38nc7r). A healthcare study postulated billions of dollars worth of savings for the United States both during protocol implementation and post-implementation periods (http://tinyurl.com/o7sv8y6).
Organisations
- Imperial College London (Lead Research Organisation)
- Pivotal Software, Inc (Collaboration)
- VMware, Inc. (Collaboration)
- Cognizant Technology Solutions (Collaboration)
- November Group, LLC (Collaboration)
- Red Hat UK (Collaboration)
- University of California, San Diego (UCSD) (Collaboration)
- Estafet Ltd (Collaboration)
- Weaveworks Ltd (Collaboration)
- November Group LLC (Project Partner)
- North Carolina State University (Project Partner)
- Shadowcat Systems Limited (Project Partner)
- Weaveworks (Project Partner)
- Red Hat (United Kingdom) (Project Partner)
People |
ORCID iD |
Nobuko Yoshida (Principal Investigator) |
Publications
Gheri L.
(2022)
Design-By-Contract for Flexible Multiparty Session Protocols
in Leibniz International Proceedings in Informatics, LIPIcs
Ghilezan S
(2023)
Precise Subtyping for Asynchronous Multiparty Sessions
in ACM Transactions on Computational Logic
Ghilezan S
(2021)
Precise subtyping for asynchronous multiparty sessions
in Proceedings of the ACM on Programming Languages
Ghilezan S
(2019)
Precise subtyping for synchronous multiparty sessions
in Journal of Logical and Algebraic Methods in Programming
Graversen E
(2021)
Event structure semantics of (controlled) reversible CCS
in Journal of Logical and Algebraic Methods in Programming
Graversen E
(2022)
Event structures for the reversible early internal p-calculus
in Journal of Logical and Algebraic Methods in Programming
Graversen E
(2019)
Towards a categorical representation of reversible event structures
in Journal of Logical and Algebraic Methods in Programming
Graversen E
(2017)
Towards a Categorical Representation of Reversible Event Structures
in Electronic Proceedings in Theoretical Computer Science
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, F#, PureScript, Scala, OCaml, Haskell, TypeScripts, Rust and Python) 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. Many keynote talks at the international conferences and workshops such as FCT'21 and ST'30 (Oct 23) January-February 2022 - Dagstuhl Workshop on Theory and Application of Behavioural Types January-February 2017 - Dagstuhl Workshop on Theory and Application of Behavioural Types November 2017 - FM Tutorial February 2018 - CGO 2018 Tutorial August 2018 Invited talk at CONFESTA (China) April 2019 F# Exchange July 2019 Scala Worlds January 2020 Invited talk at ICDICT |
Exploitation Route | Several prototype tools were published and used by both academia and industry. Including Scribble (FASE 2017), (POPL 2017, ICSE 2018) 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 | Digital/Communication/Information Technologies (including Software) Education Financial Services and Management Consultancy |
URL | http://mrg.doc.ic.ac.uk/publications/ |
Description | We presented our key finding in many conferences and workshops. For example, in 2017, Nicholas Ng spoke at the Golang UK conference. Following up on the work on static analysis for Go, a paper entitled "A Static Verification Framework for Message Passing in Go using Behavioural Types" was published at ICSE 2018, a developer/software eng conference. |
First Year Of Impact | 2019 |
Sector | Digital/Communication/Information Technologies (including Software) |
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 | 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 in PPoPP'15. |
URL | https://bitbucket.org/cogumbreiro/armus/wiki/PPoPP15 |
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 | 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 | 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 | 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/ |