Loïc Germerie Guizouarn

About

PhD Subject

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. 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 machines aims at analysing formal models of distributed systems and discovering bugs like message loss or deadlocks. This problem is undecidable in general, even with two machines only, and several restrictions have been considered to restore decidability. One of them is the half-duplex hypothesis: in a system of two machines, it is always the case that a machines does not send any message if it still has some pending messages to be received in its queue.

The goal of this phD thesis is to define new classes of communicating machines for which model-checking is decidable, among other by extending the notion of half-duplex systems to systems of arbitrary number of machines. Possibly, this would involve to introduce a separation logic for communicating machines that captures these generalised half-duplex properties.

Publications

• Multiparty Half-duplex Systems and Synchronous Communications
  Cinzia Di Giusto, Loïc Germerie Guizouarn, and Étienne Lozes
  Journal of Logical and Algebraic Methods in Programming, February 2023
• Formalising Futures and Promises in Viper
  Cinzia Di Giusto, Loïc Germerie Guizouarn, Ludovic Henrio, and Étienne Lozes
  33èmes Journées Francophones des Langages Applicatifs, June 2022
• Towards Generalised Half-duplex Systems
  Cinzia Di Giusto, Loïc Germerie Guizouarn, and Etienne Lozes
  ICE Online, June 2021, volume 347 of EPTCS, pages 22–37, 2021

Teaching

I taught in the second year of the computer science degree. I taught Mechanisms of Operating Systems and C language programming and datastructures.

Contact information