Branching Out: Existential External Choice in Effpi
This work addresses a specific problem for developers using the Effpi framework by incrementally improving its expressiveness for protocol verification in concurrent programming.
The authors tackled the limited expressiveness of the Effpi framework for strongly-typed message-passing programs by extending it with external choice, branching operations over multiple channels, and a timeout mechanism, resulting in enhanced expressiveness demonstrated through examples like implementing the Raft consensus algorithm.
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.