Branching Out: Existential External Choice in Effpi

Effpi 21,22 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 14.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 16.