Session-Based Concurrency: Between Operational and Declarative Views

The analysis of message-passing programs remains an open challenge for Computer Science.
In particular, certifying a program’s conformance with respect to some intended protocols is an active research problem. These programs can be specified by considering an operational view, in which explicit sequences of actions describe the program’s protocol interactions. These operational specifications have been much investigated, but may miss important requirements. Consider, e.g., a client-server interaction: the client may want to drop the connection if the server does not respond within t seconds, or the server may want to react to a failure by executing certain actions. This kind of requirements fit better in what we call the declarative view of the program, which describes the conditions that govern the program’s behavior, rather than the behavior itself.

This dissertation investigates the relation between the operational and declarative views of message-passing programs, following a rigorous approach that lies at the intersection of Concurrency Theory, Programming Languages, and Software Verification. Concretely, our work rests upon process calculi, small programming languages that rigorously specify interacting programs, and on behavioral type systems that can statically verify the conformance of a program specification against a protocol (abstracted as a behavioral type). We focus on session-based concurrency, an approach to message-passing concurrency in which the messages exchanged by protocol participants are structured using session types. Our approach exploits techniques for assessing the relative expressiveness of a process calculus with respect to another one; we also propose new typed process calculi when necessary.

In our work, we relate operational and declarative languages
using encodings (correct language translations). As operational languages, we consider a pi-calculus with binary session types, called pi, and several variants of it. As declarative languages, we consider linear concurrent constraint programming (lcc), a specification language in which behavior is governed by constraints shared in a centralized store, and ReactiveML (RML), an extension of OCaml to the paradigm of synchronous reactive programming (SRP).

Our contributions are divided in three parts. In the first part, the focus is on process calculi: we develop two encodings of pi into lcc. The first encoding relates the notions of linearity present in both calculi and allow us to analyze how the point-to-point communication of pi can be modeled in lcc. The second encoding shows that lcc can give a low-level declarative view of session establishment mechanisms by using private information and authentication protocols.
In the second part, we connect process calculi and actual programming languages: we develop two encodings of pi into RML to examine the relation between session-based concurrency and timed behavior with event-handling constructs. The first encoding demonstrates that signals (the synchronization unit of SRP) can represent the communication structures in pi. The second encoding considers variants of pi into RML with asynchronous communication: it showcases how synchronous reactive structures can be used to add time and event-handling constructs to session-based programs. In the final part, we consider the interplay of pi and SRP in a slightly different way: we define MRS, a new process calculus with sessions, broadcast communication, event-handling constructs, and timed behavior. We equip MRS with an expressive typing discipline, based on multiparty session types, which allows us to statically check message-passing programs with session protocols, deadlines, and event-handling requirements.

All in all, this dissertation stresses the importance of adopting a unified view to the analysis of message-passing programs in which the interplay of declarative features (time, events, and partial information) influences and informs the operational descriptions of behaviors (session protocols). Our approach is comprehensive and rigorous, and allows us to give correct, declarative specifications of message-passing programs. In our view, our technical contributions shed light on the foundations required to ensure the harmonious integration of operational and declarative views that guarantees program correctness and reliability.