Conversation-Based Governance for Distributed Systems by Multiparty Session Types

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

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.

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
Bartoletti M (2015) Choreographies in the wild in Science of Computer Programming

publication icon
Bartoletti M (2017) Honesty by typing in Logical Methods in Computer Science

publication icon
Bocchi L (2013) Virtual Models for Archaeology in Archeologia e Calcolatori

publication icon
Bocchi L (2014) On the behaviour of general purpose applications on cloud storages in Service Oriented Computing and Applications

 
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
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 Development of an open source projects, Scribble at Red Hat and Savara at Cognizant; also applications to Ocean Observatories Initiative; a commercial product, ZCDL at Cognizant, IBM and ThoughtWorks; In particular, Scribble was used for implementing a microservice use case in ThoughtWorks, and as a design tool at Estafet. Scribble development is partly shared with RedHat but is not used in their end product yet. The tools were used also by academia, for example, Scribble (FASE 2016, FASE 2017), Lchannels (ECOOP 2016) and CoreSym (POPL 2015). Further details of the findings are documented at http://mrg.doc.ic.ac.uk/ . More details: Gary Brown of Red Hat maintains Scribble, a tool for specifying communication protocols using session types that was designed by the team and integrates with several research projects. This is ongoing. Matthew Arrott of November Group LLC has applied work from Imperial on dynamic monitoring of session types in Python in monitoring software deployed by the Ocean Observatories initiative (2015). He regularly interact with Imperial College team by e-mail and meetings, and most recently discussed about applications of Scribble with logical assertions, in particular, we discussed how to apply the technology to specify and verify smart contract on a blockchain. Alexis Richardson of Weaveworks was in contact, and discussed with our research team some recent applications of session types in Go. Steve Ross-Talbot of Estafet has employed session types in the analysis of Microservices (from January 2017). Imperial is working on extensions of Scala for multiparty session types (a part of collaborations with Glasgow's post-doc, Ornela) based on our ECOOP'16, and '17 (implementation can be found https://alcestes.github.io/lchannels/) , which is highlighted by Roland Kuhn, CTO of Actyx, and one of our industry collaborators, gave a talk titled Distributed Systems vs. Compositionality at Scala World, talked about some of our works. His slides can be found https://www.slideshare.net/rolandkuhn/distributed-systems-vs-compositionality Session types have been applied to deadlock detection in the Go programming language, which was designed by Google and is in widespread use there and elsewhere. This series of work has been written up in the morning paper, a high-traffic blog which selects and summarises computer science research papers (https://blog.acolyer.org/2017/02/02/fencing-off-go-liveness-and-safety-for-channel-based-programming/ and https://blog.acolyer.org/2018/01/25/a-static-verification-framework-for-message-passing-in-go-using-behavioural-types/) and highlighted by the ACM (https://www.linkedin.com/hp/update/6234050296415297536), the main organisation of computing researchers and practitioners (February 2017, Janurary 2018). Several researchers and students including Fahd Abdeljallal, Nicholas Ng, and Nobuko Yoshida have spoken on session types and related subjects to developer conferences including F#unctional Londoners (2016); Golang UK (2016 & 2017); Strange Loop (2016) at St Louis.
Sector Digital/Communication/Information Technologies (including Software),Education
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.
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
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
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
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
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
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 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 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 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 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 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 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 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 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