Automated Modular Verification for Race-Free Channels with Implicit and Explicit Synchronization

TL;DR

This paper introduces an advanced session logic with explicit synchronization constraints to verify race-freedom and communication safety in multiparty communication protocols, improving over previous implicit-only approaches.

Contribution

It presents a more expressive session logic incorporating 'happens-before' and 'communicates-before' constraints for automated, modular verification of race-free communication channels.

Findings

Ensures race-freedom over common channels.

Allows localized automated verification for each protocol component.

Extensible to deadlock-freedom verification.

Abstract

Ensuring the correctness of software for communication centric programs is important but challenging. Previous approaches, based on session types, have been intensively investigated over the past decade. They provide a concise way to express protocol specifications and a lightweight approach for checking their implementation. Current solutions are based on only implicit synchronization, and are based on the less precise types rather than logical formulae. In this paper, we propose a more expressive session logic to capture multiparty protocols. By using two kinds of ordering constraints, namely "happens-before" <HB and "communicates-before" <CB, we show how to ensure from first principle race-freedom over common channels. Our approach refines each specification with both assumptions and proof obligations to ensure compliance to some global protocol. Each specification is then projected for each party and then each channel, to allow cooperative proving through localized automated verification. Our primary goal in automated verification is to ensure race-freedom and communication-safety, but the approach is extensible for deadlock-freedom as well. We shall also describe how modular protocols can be captured and handled by our approach.