Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last (Technical Report)

TL;DR

The paper tackles runtime verification of concurrent Clojure programs against multiparty session types (MPST), addressing both safety and liveness with Discourje. It extends Discourje to detect liveness violations by introducing mock channels that simulate real channels and allow deadlock reasoning at runtime while preserving dynamic MPST semantics with a specification $S$ and implementation $I$. The paper details a deadlock-detection algorithm that uses a critical section and synchronization via mock actions to ensure atomicity and to avoid data races, applicable to both buffered and unbuffered channels and to actions $\text{send}$, $\text{receive}$, and $\text{select}$. Demonstrations with the Two-Buyer and Load Balancing protocols illustrate that the extension yields exceptions on liveness violations that the original Discourje missed, and the work outlines future enhancements and performance considerations.

Abstract

Multiparty session typing (MPST) is a formal method to make concurrent programming simpler. The idea is to use type checking to automatically prove safety (protocol compliance) and liveness (communication deadlock freedom) of implementations relative to specifications. Discourje is an existing run-time verification library for communication protocols in Clojure, based on dynamic MPST. The original version of Discourje can detect only safety violations. In this paper, we present an extension of Discourje to detect also liveness violations.

Figures (3)

• Figure 1: Discourje and Clojure in a nutshell
• Figure 2: Specification in Discourje
• Figure 3: Implementation in Clojure