Branching Out: Existential External Choice in Effpi

TL;DR

Effpi is extended with external choice and timeout operations, enhancing its expressiveness for message-passing protocols, demonstrated through examples like the Raft consensus algorithm.

Contribution

The paper introduces branching and timeout features to Effpi, enabling more expressive protocol specifications and handling of message reception scenarios.

Findings

Effpi now supports external choice with label-dependent continuations.

A catch timeout operation allows processes to handle message delays gracefully.

The extended framework successfully models complex protocols like Raft.

Abstract

Effpi is a framework for writing strongly-typed message-passing programs in Scala, where the compiler enforces the conformance of process implementations to specified protocol types. A compiler plugin is provided to verify properties of protocols, such as deadlock-freedom and liveness, by encoding the behavioural types into a variant of CCS. To address limitations in the expressiveness of the existing toolkit, we extend Effpi with external choice by introducing a branching operation. Upon accepting a message via a branch, protocols enforce a continuation which depends on the label (type) of the received message. We equip the branching operation with the ability to accept messages over more than one channel. Additionally, we introduce a "catch timeout" operation to allow processes to gracefully handle a lack of incoming messages. The enhanced expressiveness of Effpi is demonstrated through a number of examples, including an implementation of the Raft consensus algorithm.