CMU-CS-21-141.pdf (4.21 MB)
Download file

Communication-Based Semantics for Recursive Session-Typed Processes

Download (4.21 MB)
posted on 07.12.2021, 19:18 by Ryan KavanaghRyan Kavanagh
Communicating systems are ubiquitous, and they bring human lives inestimable value.
Despite this, they often go wrong, sometimes with severe consequences. They are hard to get
right or reason about because of their inherent complexity. To tame this complexity, we can use
various formalisms and semantic techniques to model, implement, and reason about communicating
systems. Notable among these are session-typed programming languages and process calculi.
Session types [Hon93; HVK98] are a typing discipline for communicating systems. They encode
communication protocols to specify communications, analogously to how data types specify values
in functional programs. Importantly, session-typed programming languages guarantee various
desirable properties of communicating systems.
Many techniques exist for reasoning about session-typed programming languages and their
programs.These include linear logical relations [Pér+14; Ton15], game semantics [CY19], denotational
semantics [Atk17; KMP19], bisimulations [KPY17], and run-time monitoring [GJP18]. Few
prior approaches have treated inductive and co-inductive session types [Ton15; LM16; DP19] or
general recursive types [KPY17], or considered higher-order languages that integrate functional
features and code transmission. Moreover, many prior techniques are not compositional.
In this dissertation, we present novel semantics and reasoning techniques for Polarized
SILL [TCP13; PG15], a higher-order session-typed programming language. Polarized SILL coherently
integrates functional programming with asynchronous session-typed message-passing concurrency.
It supports recursive communication protocols, value transmission (including code transmission),
choices (a form of branching), and synchronization. Our contributions are unified by their commitment
to the process abstraction: communication is the only phenomenon of processes. As a result,
our semantics define the meaning of processes in terms of their communications. Together, they
support the following thesis:
Communication-based semantics elucidate the structure of session-typed languages and
allow us to reason about programs written in these languages.
Concretely, we give Polarized SILL three communication-based semantics: an observed communications
semantics, a communication-based framework for testing equivalences, and a denotational
Our observed communication semantics defines the meaning of processes to be the communications
we observe during their executions. Ours is the first to support rich protocols like recursion,
code transmission, and synchronization.
We use our observed communication semantics to define extensional notions of program
equivalence. They are given by a testing equivalences framework. Testing equivalence is a technique
for defining process equivalence. It deems processes to be equivalent whenever they are indistinguishable
through experimentation. Classical approaches to testing equivalences [DH84; Hen83; De
85] define experiment outcomes in terms of states. In contrast, we define experiment outcomes in
terms of observed communications. We show that one of the testing equivalences captured by our
framework coincides with barbed congruence, the canonical notion of process equivalence.
Our denotational semantics defines the meaning of communicating processes to be stable
continuous functions between dI-domains of session-typed communications. Importantly, our denotational
semantics is compositional, and we can reason modularly about programs. Our semantics
is an instance of CYO semantics, a novel kind of semantics that adapts ideas from Kahn semantics for
dataflow networks [Kah74] to handle bidirectional communications. Our denotational semantics is
sound relative to barbed congruence.
To support our work, we make two contributions to the mathematical foundations of programming
languages semantics. First, we introduce the first notions of fairness for substructural
operational semantics and multiset rewriting systems, and we study their properties.These fairness
results are essential to ensuring that our observed communications semantics is well-defined in
the presence of non-terminating processes. Second, we introduce techniques for reasoning about
parametrized fixed points of functors, and we study their 2-categorical properties. These results
underlie our denotational interpretation of recursive session types.




Usage metrics