Turtles: Protocol-Based Foundations for Distributed Multiagent Systems

Lead Research Organisation: Imperial College London
Department Name: Dept of 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.

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).

Publications

10 25 50
publication icon
Altayeva A (2019) Service Equivalence via Multiparty Session Type Isomorphisms in Electronic Proceedings in Theoretical Computer Science

publication icon
Bocchi L (2017) Monitoring networks through multiparty session types in Theoretical Computer Science

publication icon
Carbone M (2016) Multiparty session types as coherence proofs in Acta Informatica

publication icon
Castellan S (2019) Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side in Proceedings of the ACM on Programming Languages

publication icon
Cogumbreiro T (2018) Dynamic Deadlock Verification for General Barrier Synchronisation in ACM Transactions on Programming Languages and Systems

publication icon
Ghilezan S (2019) Precise subtyping for synchronous multiparty sessions in Journal of Logical and Algebraic Methods in Programming

publication icon
Graversen E (2017) Towards a Categorical Representation of Reversible Event Structures in Electronic Proceedings in Theoretical Computer Science

publication icon
Graversen E (2019) Towards a categorical representation of reversible event structures in Journal of Logical and Algebraic Methods in Programming

 
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.

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 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 2017
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 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 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 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 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 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 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 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 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 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 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/