A Session Logic for Relaxed Communication Protocols

Abstract:

This thesis addresses the formalization of concurrent programs, where the synchronization among processes is mainly achieved via message passing. Since message passing is a preferred avenue for achieving high performance in distributed applications, ensuring its safe and correct design and implementation is crucial, yet challenging. The challenge mostly comes from the complex interaction schemes commonly used in a distributed system. Specifically,
a bogus behavior may arise either due to the incorrect implementation of the system's core components (the implementation does not conform to the expected communication protocol) or due to the incorrect composition of standalone systems (incompatible protocol composition).

To this purpose, we propose a multiparty session logic to assist in the design and specification of communication-centered programs. This logic is incorporated into a verification framework which helps to (i) uncover communication-related bugs or (ii) prove that the communication protocol has correctly emerged into a bug-free implementation.

This thesis highlights how to (1) design communication protocols which go beyond the current state of the art in terms of expressivity, (2) achieve protocol conformance in a modular fashion, and (3) safely compose "plug and play" protocols.