Communicating automata and quasi-synchronous communications
Automates communicants et communications quasi-synchrones
Résumé
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 and receiving messages asynchronously. 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, of a limited portability of the code, and of the difficulty of running representative tests, etc, it is error prone and therefore often reserved to experts. Model-checking of communicating automata aims at analysing formal models of distributed systems and discovering bugs like message loss or deadlocks. Due to the asynchronous nature of the communications, this problem is undecidable in general, even with two machines only, and several restrictions have been considered to restore decidability. We define a new one in this thesis: systems that are realisable with synchronous communications (RSC for short), that is the systems whose behaviours are equivalent to synchronous ones. We propose the class of RSC systems as a generalisation of half-duplex systems, which are system of two machines, where a machines does not send any message if it still has some pending messages to be received in its queue. We study another formalism as well: choreographies, which provide a way to reason globally on a system. Choreographies describe synchronous executions, and one of the problems associated with it is checking whether the combination of all participants of the described communication will behave accordingly to the global description. We propose to rely on the properties of RSC systems to study this problem.
Les systèmes distribués sont le plus souvent basés sur l'échange asynchrone de messages entre des agents. La programmation par échanges de messages est largement utilisée en calcul haute performance, en programmation événementielle, dans les architectures orientées service, etc. Malheureusement du fait de la variété des modèles de communication, des ambiguïtés dans les spécifications, de la portabilité limitée du code, ou encore de la difficulté à exécuter des tests, il est très difficile de vérifier les systèmes communicants. Le model-checking de systèmes communicants vise à analyser des modèles formels de systèmes distribués et à détecter automatiquement des erreurs comme des pertes de messages ou des inter-blocages. Ces problèmes sont indécidables pour des systèmes à partir de deux machines, et plusieurs hypothèses restrictives ont été étudiées pour rendre les problèmes décidables. Nous définissons dans cette thèse une nouvelle classe de systèmes : les systèmes réalisables avec des communications synchrones (RSC pour faire court). Les comportements de ces systèmes approximent des comportement synchrones, où les messages sont envoyés et reçus simultanément. Nous nous basons sur cette définition pour étudier la généralisation d'une autre classe de systèmes : les systèmes half- duplex. Un système à deux machines est half-duplex si lorsqu'une machine envoie des messages, l'autre ne peut pas lui en envoyer. Nous étudions également un autre formalisme, permettant de raisonner sur les systèmes de manière globale : les chorégraphies. Ce formalisme décrit les exécutions de manière synchrone, et un des problèmes qui y est associé est de vérifier si la combinaison des comportements de chaque acteur qui y est décrit est conforme à la description globale. Nous proposons d'utiliser les propriétés des systèmes RSC pour traiter ce problème.
Origine : Version validée par le jury (STAR)