Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper extends the Effpi framework, a tool for writing strongly-typed message-passing programs in Scala, with external choice via a branching operation that enforces continuations based on the label of the received message. The extension allows branching over multiple channels and introduces a "catch timeout" operation for handling missing messages. This enhancement is validated through examples, including an implementation of the Raft consensus algorithm, demonstrating increased expressiveness.
Effpi, a Scala framework for message-passing programs, gets a serious upgrade, making it easier to implement complex protocols like Raft with new branching and timeout features.
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.