Laura Voinea

Laura Voinea

Research Associate with an interest in programming languages, static analysis, and logics

Publications

Resource Sharing via Capability-Based Multiparty Session Types

Published in IFM 2019, 2019

Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is stan- dard for multiparty session type systems to use access control based on linear or affine types. While useful in offering strong guarantees of communication safety and session fidelity, linearity and affinity run into the well-known problem of inflexible programming, excluding scenarios that make use of shared channels or need to store channels in shared data structures. In this paper, we develop capability-based resource sharing for multiparty session types. In this setting, channels are split into two entities, the channel itself and the capability of using it. This gives rise to a more flexible session type system, which allows channel references to be shared and stored in persistent data structures. We illustrate our type system through a producer-consumer case study. Finally, we prove that the resulting language satisfies type safety.

Download here

A Session Type System For Asynchronous Unreliable Broadcast Communication

Published in , 2019

Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disci- plines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such systems have structured communication patterns that should be amenable to analysis by means of session types, but the necessary theory has not previously been developed. We introduce the Unreliable Broadcast Session Calculus, a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound. We capture two common operations, broadcast and gather, inhabiting dual session types. Message loss may lead to non-synchronised session endpoints. To further account for unreliability we provide with an autonomous recovery mechanism that does not require acknowledgements from session participants Our type system ensures soundness, safety, and progress between the synchro- nised endpoints within a session. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.

Download here

Mungo and StMungo: Tools for Typechecking Protocols in Java

Published in In: Gay, S. and Ravara, A. (eds.) Behavioural Types: from Theory to Tools. Series: River Publishers Series in Automation, Control and Robotics. River Publishers, pp. 309-328, 2017

We present two tools that support static typechecking of communication protocols in Java. Mungo associates Java classes with typestate specifica- tions, which are state machines defining permitted sequences of method calls. StMungo translates a communication protocol specified in the Scribble protocol description language into a typestate specification for each role in the protocol by following the message sequence. Role implementations can be typechecked by Mungo to ensure that they satisfy their protocols, and then compiled as usual with javac. We demonstrate the Scribble, StMungo and Mungo toolchain via a typechecked POP3 client that can communicate with a real-world POP3 server.

Download here

Benefits of Session Types for Software Development

Published in PLACES16, 2016

Session types are a formalism used to specify and check the correctness of communication based systems. Within their scope, they can guarantee the absence of communication errors such as deadlock, sending an unexpected message or failing to handle an incoming message. Introduced over two decades ago, they have developed into a significant theme in programming languages. In this paper we examine the beliefs that drive research into this area and make it popular. We look at the claims and motivation behind session types throughout the literature. We identify the hypotheses upon which session types have been designed and implemented, and attempt to clarify and formulate them in a more suitable manner for testing.

Download here