Towards Resilient Communication Protocols

At a high level, the objective of this research is to automate the addition of crash handling behaviour to protocols that describe the agenda of communication between participants in a distributed or concurrent program.

What is meant by a protocol, is a high-level description of a program considering only messages sent between participants. For example, a program between an ATM machine and a bank will have much code running on both ends, but such code is omitted, in our protocol we are only interested what messages are sent between participants and in what order.

In any given communication protocol, there may be a number of unreliable participants, for example while a bank can usually be trusted, an ATM machine is subject to crash. A protocol involving such unreliable participants cannot be guaranteed to behave as it appears because

there is the possibility that a message outlined in the protocol will fail to send. It is not desirable for an ATM to behave unexpectedly in such situtaions, and it is the case in many distributed systems that there will exist unreliable participants that can lead to unexpected behaviour. This can be accounted for by extending the protocol to be more descriptive, specifically, this means to detail what the protocol should do in the case of failure to send a message.

However, depending on the original protocol, the way a crash (i.e. failure) would be handled will differ. In some protocols it is necessary that the protocol continues to operate with the remaining functional participants, and in others, a crashed participant will mean the protocol cannot continue to operate and must come to a stop.

This is to be achieved through the introduction of failures. In particular, as described in the literature, there are currently four specific failure patterns. These patterns are graceful failure, local graceful failure, failover and successor failover. Graceful failure aims to end the protocol as

quickly as possible. Local graceful failure does as graceful failure except that it attempts to limit the effect of the crash to the subset of the participants affected, Failover allows one of the existing participants to take over the role of the crashed participant to continue operation.

Successor failover introduces an new previously not present participant to take over the role of the crashed participant.

Rather than manually inspecting and modifying protocols to deal with each case of failure which can be very time consuming, we would like the programmer to be able to specify how the protocol should continue in the case of a crash, and then have that behaviour automatically introduced for them using one of the aforementioned patterns.

On the theoretical side, this project will explore Multiparty Session Types (MPST) as a foundational framework. MPST provides a formal structure for defining communication protocols between multiple participants. Additionally, we will investigate algorithms for the automated

generation of crash-handling branching, allowing protocols to adapt dynamically to failures. This approach will ensure that the system remains robust and flexible in real-world scenarios where communication failures are inevitable.

In terms of implementation, the protocols mentioned are expressed in a domain specific language called Scribble, and the automatic extension of these is to be implemented in a functional programming language such as OCaml or Haskell. These protocols not only need to be implemented in code but also proved for correctness with the use of Pi-calculus.

This project falls within the EPSRC information and communication technologies (ICT) research area where ICT is one of the themes or research areas listed on this website.