Laetitia Laversa

Most of the distributed systems we use nowadays are based on the message-passing paradigm where systems are structured into parties that interact only by sending/receiving messages. Message-passing programming is largely employed in high performance computing (MPI, OpenMP, etc), event-driven applications built on top of actor-based languages (Scala, Erlang,etc), service-oriented architectures, peer-to-peer applications, etc. Unfortunately, because of the variety of communication models (peer to peer, mailbox, etc.), of the ambiguities of the specifications of the communication primitives, and of the difficulty of running representative tests, etc., it is error prone and therefore often reserved to experts. The majority of the issues above stem from the asynchronous nature of messages exchange. Indeed, the conception and the analysis of message-passing programs is greatly simplified if one can assume that all communications occur synchronously, i.e., that each message is received exactly at the same time it has been sent. As a matter of fact, some properties (e.g., reachability) becomes decidable if the underlying communication model is synchronous. We are thus interested in understanding under which conditions we could avoid using asynchronous models and being able to design and prove correct simpler but equally powerful systems. This is a property that goes under the name of synchronizability. Synchronizability of a distributed system is the property that the observable behaviour of the system is the same whether or not the communications are synchronous. The main topic of my PhD is to develop methods and tools that help designing safe distributed systems based on the notion of synchronizability.