Building correct communicating systems (i.e. concurrent and distributed systems) is a hard task. Such systems often present non-deterministic behaviours that are hard to reproduce. This means that, whenever there is a bug in one of such systems, fixing it is a time consuming and costly task. Furthermore, distributed systems are nowadays widespread in our society, including key sectors such as banking or E-healthcare. Thus, bugs in communicating systems can be very damaging, threatening large economic costs, and the safety and security of the industries that rely on them.
To guarantee the correctness of communicating systems, many tools and theories have been developed. Session types are among the most influential theories for verifying the absence of concurrency bugs in communicating systems. Session types can guarantee that process implementations only follow the specified structured sequence of actions (send/receive). These specifications effectively represent communication protocols, and session type theories provide techniques to verify that they are absent of concurrency bugs. Among the most influential extensions of session types is the theory of Multiparty Session Types (MPST), which enables the modelling of protocols among an arbitrary number of participants, and has been integrated with many mainstream languages.
However, most of the tools based on session types are not following the exact theories that are presented in the scientific publications, since they also need to take into account engineering issues. Furthermore, most of the session type theories are proven correct using complex pen-and-paper soundness proofs. Such proofs can contain errors, and the literature shows examples of these cases. This is a big threat to the validity of large bodies of work. Proof assistants are tools that can guarantee the correctness of these soundness arguments. Encoding languages, tools, and theories in a proof assistant is called mechanisation, and it has led to large influential developments in computer science, such as CompCert, a certified C compiler that has proven to present significantly less bugs than other comparable compilers, and that is currently being used in the context of critical systems.
But proof mechanisation is significantly hard, and not much work exists on mechanising MPST. One of the main hurdles in mechanising MPST is the notion of process equivalence, or bisimilarity. Informally, two processes are bisimilar if they match each others actions, according to their Labelled-state Transition System (LTS) semantics. One main techniques for proving bisimilarity is known as the bisimulation proof method, which relies on finding a relation between two processes that guarantees that they will match each other's moves according to their LTS. These proofs are widespread in concurrency theory, and are key to successful mechanisations of MPST. We need a way to simplify the mechanisation of LTS semantics, and bisimilarity proofs.
We will study common bisimulation proof techniques and algorithms, and find and implement a suitable candidate for mechanisation. Our main goal is to automate as much as possible of the mechanisation of the LTS semantics. One of the key challenges is to find the suitable definitions: pen-and-paper proofs can often overlook details that are important in a mechanisation. For example, termination is often informally justified in pen-and-paper proofs, but the specific details are key to a successful mechanisation. We will mechanise a generic framework for LTS semantics and bisimilarity in the Coq proof assistant, and use it in two case studies from the project partners. These case studies will serve both as a way to evaluate success, and as main driving elements of this project. Finally, we will study the extraction of certified implementations within our framework, thus contributing to increase the safety and reliability of distributed systems.
|