Intrinsically-Typed Mechanized Semantics for Session Types

TL;DR

This paper introduces an executable, intrinsically typed small-step semantics for a functional session type calculus, implemented in Agda, ensuring type soundness and progress through mechanization.

Contribution

It presents the first mechanized, intrinsically typed semantics for a realistic session type calculus including recursion, subtyping, and asynchronous communication.

Findings

Proves type preservation and progress in Agda implementation

Models asynchronous communication with encoding

Ensures soundness through mechanized semantics

Abstract

Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages with session types are tedious and technically involved, it is rare to see mechanized soundness proofs for these systems. We present an executable intrinsically typed small-step semantics for a realistic functional session type calculus. The calculus includes linearity, recursion, and recursive sessions with subtyping. Asynchronous communication is modeled with an encoding. The semantics is implemented in Agda as an intrinsically typed, interruptible CEK machine. This implementation proves type preservation and a particular notion of progress by construction.

Equations

$$\displaystyle\begin{array}[]{l}\mathtt{let}\ x\ \mathtt{=}\ (\mathtt{new}\ \mathsf{end!})\ \mathtt{in}\\ \mathtt{let}\ (c_{1},c_{2})\ \mathtt{=}\ x\ \mathtt{in}\\ \mathtt{let}\ u\ \mathtt{=}\ \mathtt{fork}\ (\mathtt{close}\ c_{1})\ \mathtt{in}\\ \mathtt{wait}\ c_{2}\end{array}$$

Full text

We present an executable intrinsically typed small-step semantics for a realistic functional session type calculus. The calculus includes linearity, recursion, and recursive sessions with subtyping. Asynchronous communication is modeled with an encoding.

The semantics is implemented in Agda as an intrinsically typed, interruptible CEK machine. This implementation proves type preservation and a particular notion of progress by construction.

session types, dependent types, concurrency

††conference: Woodstock ’18: ACM Symposium on Neural Gaze Detection; June 03–05, 2018; Woodstock, NY††booktitle: Woodstock ’18: ACM Symposium on Neural Gaze Detection, June 03–05, 2018, Woodstock, NY††price: 15.00††isbn: 978-1-4503-9999-9/18/06††copyright: none††ccs: Software and its engineering Concurrent programming structures††ccs: Software and its engineering Semantics††ccs: Theory of computation Process calculi

1. Introduction

Session types are an established paradigm for structured communication (Honda1993; HondaVasconcelosKubo1998; DBLP:journals/csur/HuttelLVCCDMPRT16; CastagnaDezaniCiancagliniGiachinoPadovani2009). The original form provides a typing discipline for protocols between two parties on bidirectional, heterogeneously typed communication channels. The operations for session types $S$ are

• •

creating a channel;

• •

$\textup{{send}}:{!T}.S\multimap T\multimap S$, sending a value of type $T$ and continuing the protocol according to $S$;

• •

$\textup{{recv}}:{?T}.S\multimap T\otimes S$, receiving a value of type $T$ and continuing according to $S$;

• •

$\textup{{select}}_{i}:(S_{1}\oplus S_{2})\multimap S_{i}$, internal choice between two continuations;

• •

$\textup{{branch}}:(S_{1}\with S_{2})\multimap(S_{1}\multimap T)\otimes(S_{2}\multimap T)$, accepting an external choice between different continuations;

• •

$\textup{{close}}:\textbf{end!}\to 1$, closing a channel;

• •

$\textup{{wait}}:\textbf{end?}\to 1$, waiting for a channel to be closed.

There are synchronous and asynchronous variants (GayVasconcelos2010-jfp; Wadler2012; DBLP:conf/esop/LindleyM15), or variants with additional typing features (e.g., dependent types (DBLP:conf/fossacs/ToninhoY18), context-free (ThiemannVasconcelos2016; DBLP:conf/esop/Padovani17)), as well as extensions to deal with more than two participants in a protocol (HondaYoshidaCarbone2008). They also found their way into functional and object oriented languages (DBLP:journals/iandc/Dezani-CiancagliniDMY09). Generally, session types are inspired by linear type systems and systems with typestate as channels change their type at each communication operation and must thus be handled linearly. Some variants are directly connected to linear logic via the Curry-Howard correspondence (CairesPfenning2010; DBLP:conf/esop/ToninhoCP13; Wadler2012).

What static guarantees do we expect from session types? First, type preservation — as for any other type system. Second, session fidelity, which means that channels are only used according to their stated protocol/session type. Third, some notion of progress. The strongest notion of progress is, of course, deadlock freedom, which is guaranteed by the designs derived from linear logic (CairesPfenning2010), but many formulations of session types have weaker notions of progress.

How does the literature go about proving these properties? Mostly by careful and tedious manual proofs. To our knowledge, there is only one session-type related paper that comes with a mechanized proof of type soundness (DBLP:journals/mscs/GotoJJPR16), which we discuss in Section LABEL:sec:related.

The main contribution of this paper is the first mechanized proof of the type soundness and session fidelity of a realistic, fully-fledged functional session type calculus.

• •

First fully mechanized type preservation proof for a functional calculus with session-typed communication.

On top of the functional core (call-by-value PCF with products) our formalization covers linear typing, forking processes, creating and closing communication channels, higher-order sending and receiving values, selection from and offering of choice, and recursive session types with subtyping.

• •

First fully mechanized proof of session fidelity.

Session fidelity means that the operations on both ends of a channel always agree on the direction of the next transmission on the channel and on the type of the transmitted value, if any: an operation that sends a value of type $T$ on one end is always matched by a receive operation that expects a value of (a supertype of) type $T$.

• •

The preservation proof on the level of expressions comes essentially for free as the calculus is implemented in terms of an intrinsically typed, multi-threaded CEK machine.

For each serious computation step, the CEK machine relinquishes to the scheduler, which preserves typing along with some global resource invariants.

• •

Relative progress is established by construction. The scheduler contains a step function that attempts to find a thread in which it can perform a computation step. If the step function fails, it has detected a deadlock situation (which is to be expected as the underlying calculus is not deadlock-free).

• •

The focus of the formalization is a sychronous session type calculus, but we give a typed encoding of asychronous session types in typed ones, which is compatible with our results.

Challenges of the formalization

Several aspects of the formalization are standard: intrinsically typed abstract syntax with de Bruijn indexing (DBLP:conf/sbmf/Wadler18; DBLP:journals/pacmpl/PoulsenRTKV18; DBLP:journals/jar/BentonHKM12), type-indexed values, and gas-driven evaluation (siek13:_type_safet_three_easy_lemmas; DBLP:conf/esop/OwensMKT16; DBLP:conf/popl/AminR17). In addition, we address the following key challenges.

1. (1)

Linearity needs to be handled at the syntactic level. The typing of expressions must make sure that linearly typed values are neither duplicated nor discarded. 2. (2)

The multi-threaded CEK machine provides an executable model of reductions at the expression level while keeping a clean interface to thread-level reduction, which is inspired by free monad constructions, and thread scheduling. Our model performs only syntactic rearrangements (aka administrative reductions) at the expression level and leaves serious execution steps to the scheduler at the thread level. This design choice pushes the handling of all effects (nontermination, communication, nondeterminism) entirely to the thread level, thus simplifying the model for the expression level. 3. (3)

Channels need to be managed as a global resource. The problem here is that communication over a channel requires a rendezvous between two different threads (expressions). These threads must have a common means to identify the channel, which cannot be handled locally at the level of an expression. 4. (4)

Resources need to be handled linearly, in particular when they are moved across different semantics entities. We deal with this aspect by introducing the concept of a resource splitting tree, which is a binary tree that maintains linearity. 5. (5)

We make a preliminary investigation of adequacy of the CEK execution with respect to a small-step semantics. Adequacy does not follow from the intrinsic typedness of the interpreter, but requires separate proofs (see Section 5.4).

The framework reported in this paper is implemented in roughly 3000 lines of Agda. The full code is available in a github repository111https://github.com/peterthiemann/definitional-session. For pedagogic reasons, the code fragments shown in Sections 2–4 of this paper are taken from a simplified version with some slight deviations from the repository version, but nonetheless fully type checked. The code fragments in Section 5 are pretty printed excerpts from the repository code. Throughout, we assume familiarity with Agda or other similar proof assistants.

2. A Tiny Language with Session Types

MicroSession is a simplified subset of the session-typed language by GayVasconcelos2010-jfp. Nevertheless, it contains the fundamental operations of a session-typed language. These operations are channel creation, sending and receiving values, and closing a channel. To glue these operations together in a meaningful way, we further require process creation (fork), introduction and elimination of pairs (the operations to create a channel and to receive a value return pairs), and a let construct to sequence operations. This simplicity enables us to concentrate on the key ideas, on which the modeling of all further operations on sessions relies. In Section 5 we explain what it takes to extend the formalization of MicroSession to full Synchronous GV.

In this section, we define the type structure and the syntax of MicroSession. Our syntax definition is intrinsically typed in a way that enforces linear handling of channels. Variable binding is handled with de Bruijn indices.

Figure 1 defines the type structure of MicroSession. Types are unit types, pair types, and channel types. A channel is described by a session type, which either describes a transmission (STrm d t s) of a value of type t and continuing at type s or the closing of a channel (SEnd d). Both types are parameterized by a direction (d : Dir), which indicates the direction of the data transfer, either sending (SND) or receiving (RCV). This parameterization reduces the number of cases to consider when defining duality, subtyping, and context reduction and proving their properties. For convenience, we introduce the abbreviations SSend t s, SRecv t s, SEnd!, and SEnd? using Agda’s pattern feature.

The dual of a session type describes the protocol on the other end of the channel (see Fig. 4). It flips the direction of the communication operations. This operation is involutory as proved in the lemma dual-inv : ∀ s → dual (dual s) ≡ s.222The type x ≡ y denotes Martin-Löf identity of x and y with single element refl (MartinLoef1975). Figure 4 defines the operation dual and proves that it is involutory.

We use lists of types as typing contexts (: TCtx).

Figure 2 contains key notions to formalize linear handling of resources in the type system (walker:subst_type_system; DBLP:conf/lics/CervesatoP96). A ternary context splitting relation333The definition makes use of Agda’s syntactic convention for defining infix operators: the underlines in the identifier ≜∘ indicate the positions of the three arguments. ≜ ₁ ∘ ₂ on typing contexts captures contraction. It splits an incoming context in the conclusion of a rule into two contexts ₁ and ₂ for use in the premises. As values of unrestricted type can be contracted whereas linear ones cannot, there is a predicate Unr that identifies the unrestricted ones: the unit type is unrestricted and pairs are unrestricted if both components are. It extends to typing contexts : TCtx by All Unr , which means that all entries of need to satisfy Unr.444Using the library type Data.List.All.

Context splitting implements contraction by permitting only bindings for unrestricted types to end up in both ₁ and ₂ (constructor unr). Linear types end up either in ₁ (constructor lft) or in ₂ (constructor rgt).

Figure 3 defines the typing of expressions by means of the type Expr t. It is indexed by the typing context and the result type t and ensures that its values have type t in context . While this setup has become standard (DBLP:journals/pacmpl/PoulsenRTKV18; DBLP:conf/sbmf/Wadler18; DBLP:conf/cpp/Allais0MM17), there are a few twists in our particular instance.

The syntax is in A-normal form to restrict evaluation contexts to a sequence of bodies of let expressions. That is, all constructs except let and fork take only variables as subterms. In A-normal form, the let expression is the only place that composes non-trivial computations. This choice simplifies the formalization of the semantics as explained in Sec 4.4.

Variables (var) are represented by de Bruijn indices into the context. Accessing variables is formalized in the type t ∈ , which implements weakening only for unrestricted variables. If the variable is on top of the context (constructor here), then all bindings below must be unrestricted. If the variable is below the top (constructor there), then the top binding must be unrestricted.

The unit constructor introduces a unit value if the context is unrestricted. The pair constructor introduces a pair. It splits the context and looks up the components. The letpair constructor eliminates a pair and binds the components in an expression. It splits the context between the pair and the expression. letbind splits the context between two expressions and binds the result of the first expression in the second. fork takes a unit-typed expression to run in a new thread. new requires that the context is unrestricted; it takes a session type and creates a channel of this type. It returns a pair of dual endpoints for this channel. close and wait close a channel, actively or passively as indicated by the session types SEnd! and SEnd?. send takes two arguments (hence splitting is needed), a channel of type TChan (SSend t s) which is ready to send a $t$ and a value of type $t$. It returns the continuation channel of type $s$. recv takes a channel which is ready to receive a $t$ and returns a pair consisting of the continuation channel and the received value. This pair type is linear because it contains a channel type.

Figure 5 contains a well-formed example term. Fig. 5(a) shows it in some concrete syntax whereas Fig. 5(b) contains its Agda rendition. The code creates a session of type SEnd! which yields a pair of channel ends. Next, it decomposes the pair into the channel ends of type SEnd! and its dual SEnd?, respectively, forks a thread which closes one channel end, and keeps the other end in the main thread to wait on it.

3. Operational Semantics

The semantics has two layers as common in functional calculi with session types. The top layer is a process calculus which operates on a thread pool. Each single thread corresponds to an expression. A scheduler selects the next thread to execute. The bottom layer deals with the reduction of single expressions.

The expression semantics is modeled by an extended CEK machine (FelleisenFriedman1986). The state of a CEK machine comprises an expression $e$ (aka control), an environment $\varrho$, and a continuation $\kappa$. This machine is typed so that the environment contains values according to the type environment for $e$ and the input type of the continuation matches the type of $e$. The machine is extended to implement “stuttering execution”. For any serious activity, it suspends itself to a continuation and renders control to the scheduler that administers computation on the thread level. In particular, execution is suspended for every operation that may not terminate (i.e., function application) or that requires interaction with the scheduler (i.e., thread and channel creation) or with other processes (e.g., sending and receiving values).

Expression level execution is driven by a function decompose that takes a CEK machine state and returns a continuation along with the operation that needs to be performed by the scheduler as well as arguments for this operation. In a first approximation the type of the decompose function is as follows.555Section 4.3 discusses the full type for decompose.

@mkpream

@l@ @addtopreamble@mkpream@l@   @addtopreamble@mkpream@l@ @addtopreamble@mkpream@l@   @addtopreamble@mkpream@l@ @addtopreamble@mkpream@l@ @addtopreamble@mkpream@l@   @addtopreamble@mkpream@l@ @addtopreamble@mkpream@l@   @addtopreamble@mkpream@l@ @addtopreamble@mkpream@l@ @addtopreamble@mkpream@l@@addtopreamble@preamble@preambledecompose : (split : ≜ ₁ ∘ ₂) missing

@mkpream@l@   @addtopreamble@mkpream@l@@addtopreamble@preamble@preamblemissing@mkpream@l@ @addtopreamble@mkpream@l@@addtopreamble@preamble@preamble→ (e : Expr ₁ t) → ( : VEnv ₁) → ( : Cont ₂ t) missing

@mkpream@l@   @addtopreamble@mkpream@l@@addtopreamble@preamble@preamblemissing@mkpream@l@ @addtopreamble@mkpream@l@@addtopreamble@preamble@preamble→ Command missing

The types of the expression e and the value environment are linked via the type environment ₁, where VEnv ₁ contains values as specified by the type environment. The type t serves as the argument type of the continuation as well as the result type of the expression. The continuation is represented by a closure consisting of an evaluation context and a value environment. It is therefore indexed by type environment ₂ which provides the typing of the variables captured in the closures. The two type environments are split off a single parent environment to correctly model linear types as explained in Section 2.

The intention is that the CEK execution “gives up” as soon as some side effect is to be executed. It does so by issuing a Command, which instructs the top-level scheduler to perform the effect on behalf of the thread. Each Command contains a continuation which accepts the value resulting from executing the effect as input.

The function decompose connects the static semantics with the dynamic semantics. While expressions are indexed by objects of the static semantics (i.e., type environments and types), (value) environments and continuations are objects of the dynamic semantics and will be indexed with run-time resources. In our case, resources are the endpoints of communication channels as explained in Section 4.1. An endpoint is a special case of a value, values are contained in environments, and every continuation contains an environment. Hence, resources are expressed as additional indices of the types of these objects as shown in Section 4.3.

The process level consists of expression processes, parallel execution of processes, and restriction to introduce a new session typed channel. We leave omit its description because we keep processes in a normal form where all restrictions are pushed to the top level and the expression processes are collected in a thread pool. The scheduler discards unit processes and enforces commutativity and associativity.

4. Resources

Working towards resources, we start with defining the values stored in the environments of the machine. The main complication arises in devising the representation of channel endpoints.

• •

A channel endpoint is a global resource, so it must be defined outside the currently executing thread / expression.

• •

As two threads communicate through the endpoints of the same channel, there must be a global naming scheme for channels across all currently executing threads.

• •

It must be possible to detect a rendezvous of two threads. For example, if one thread wants to close a particular channel, we need to match it with another thread that waits on the other end of the same channel.

To this end, we define two entities. A global session context $G$ that corresponds to the collection of all restrictions and a thread pool that contains representations of all expression processes.

4.1. Global Session Context

The global session context represents the system-wide view of all channels and their current state. The crucial step is called resource splitting which break this view down to individual threads and all the way to individual values while guaranteeing uniqueness of reference and consistency with the system view. Uniqueness means that each channel end is only referenced in one value in the current state. As values are related to environments, continuations, threads, and the threadpool, splittings naturally form a tree structure, the splitting tree. Moreover, these conditions (and thus the splitting tree) need to be maintained throughout the execution.

Figure 6(a) contains the definition of the global session context by the type SCtx, ranged over by $G$. Working backwards, a global session context is a list. Each entry of the list describes the state of one channel (type Session) in terms of a session type and a polarity of type PosNeg. It contains an entry for every channel that has been created at some earlier point during execution. Figure 6(b) explains the meaning of an entry and defines a graphical representation for it. If a channel is not available at the top level, then it is closed. In general, unavailability of a channel may also mean that the channel is allocated to a different semantic entity. A session context is Inactive if all its entries are unavailable, i.e., equal to nothing.666Is-nothing is a library predicate for the Maybe type.

To manage resources, each semantic entity that may depend on the availability of a resource is indexed by a session context G which makes available exactly the resources used by this entity. These semantic entities are (in order of containment)

(1) the thread pool (i.e., a process in normal form),

(2) expression threads,

(3) value environments,

(4) values.

It is an invariant of our encoding that all these entities refer to a session context of the same length as the global context, so that a channel can be globally identified by its de Bruijn index into the context. The thread pool is indexed by the root context from which all other contexts are split off. Conceptually, the allocation of resources to semantic entities is described by a single binary tree rooted in the global session context. Each inner node of the tree corresponds to a split operation and the leaves correspond to (primitive) values. Each semantic action maintains this tree. The upcoming definition of resource splitting guarantees linear handling of all resources.

For example, Figure 7 shows the splitting tree for a thread pool777Section 4.5 contains the definition of the thread pool type. which has two channels available and a third channel that has been closed already. The channel ends are split among three threads where Thread1 and Thread3 each obtain one end of a channel, and Thread2 obtains two ends of different channels. In the end, at the Empty thread pool, all resources must have been distributed to the threads, and we say the remaining resource context is inactive.

Exactly the same kind of resource splitting occurs in value environments and also in values themselves.

Given this intuition, we define resource splitting in Figure 8. Relation RSplit governs splitting of a single entry. Unavailable resources cannot be split (rs-both); all resources can go exclusively to the left or to the right child context (rs-left, rs-right); a POSNEG resource stands for both channel ends and can be split in two ways: either the POS end goes left and the NEG end goes right (rs-posneg) or vice versa (rs-negpos). Relation SSplit lifts RSplit to lists of entries in the obvious way.

A splitting ssp-$G=G_{1}\circ G_{2}$ : SSplit $G$ $G_{1}$ $G_{2}$ may be viewed as a separating conjunction $G_{1}\ast G_{2}$ (Reynolds2002).

Semantic actions require restructurings of the splitting tree, which are reminiscent of rotations on balanced trees. Here is an example for such a restructuring lemma. \ExecuteMetaData[Global0.tex]ssplit-compose It transforms the splitting tree in Figure 9(a) to the one in Figure 9(b), highlighting the new intermediate session context Gi. The proof is straightforward, but tedious.

4.2. Values and Value Environments

We continue bottom up by defining polarities and channel references in Fig. 10. The latter are augmented de Bruijn indices that describe channel values. There are two “zeroes” in type ChannelRef, here-pos and here-neg, depending on whether we found the positive or negative end of a channel indicated by its polarity argument. For the positive end, the session type s is copied from the context. For the negative end, the index is the dual of the session type in the context. In both cases, the remaining context must be inactive. The “successor” there skips over unavailable channels.

Values and value environments (Figure 11) are rather unsurprising at this point. A unit value (like any other primitive value) requires an inactive context. A pair value splits its resources among the components. A channel value consists of a po component, which indicates whether this value is the positive or negative end of the channel, and a channel reference cr that makes the actual connection to the session context G.

The empty environment vnil requires an inactive session context. A non-empty environment vcons splits the session context between the value and the rest of the environment.

4.3. Decomposing Expressions

This subsection explains the types involved in the evaluation of expressions and processes and how expression evaluation and the scheduler work together. The next subsection discusses the treatment of several illustrative cases across the levels. We start with the full type of decompose. \ExecuteMetaData[Session0.tex]decompose The decompose function is indexed by a type environment and by a global session context G, which are both split using their respective splitting relation. The splitting of the session context refines the splitting of the typing environment: A value bound to a variable may be a (nested) pair that contains several resources (channel ends). The refinement arises because the typing environment manages variable bindings, whereas the session context keeps track of single resources.

One part of the resources (indexed by G₁) is referenced in the environment and manipulated by the expression e. The other part (indexed by G₂) is referenced and manipulated by the continuation . A continuation (see Figure 12) is a syntactic object of type Cont G t where context G describes the resources held, is the typing for its variables, and t is its argument type. It is either halt, in which case an inactive session context indicates that all resources have been used up, or a bind continuation, which is a frozen call to decompose consisting of an expression, an environment, and another continuation along with splittings for variables and resources.

The decompose function returns a value of type Command G, where the session context G summarizes all resources contained in the command, i.e., in the values and continuations contained in it. A command is a request to the scheduler to perform an operation on behalf of the thread. It contains all parameters of the operation and a continuation to resume the thread. The next subsection discusses illustrative cases for commands.

An important point of this setup is that all values manipulated during execution are exposed in top-level data structures. All closures (in continuations and otherwise) are syntactic and can be inspected and modified at run time by traversing the respective data structure. This property is preserved up to the top-level where the scheduler processes the thread pool. We need this property in Section 4.6 when dealing with channel creation.

4.4. Issuing Commands

This subsection discusses selected cases of the decompose function and the corresponding cases of the Command type side by side. So there is a mix of code from the function definition of decompose and constructor definitions for Command.

The decompose function follows the evaluation context. To process an expression letbind sp e₁ e₂, the interpreter splits the value environment according to the split sp of the typing environment, and constructs a new continuation for e₁ by using bind to compose the frame for e₂ with the continuation .

At this point our choice of A-normal form pays off. Without A-normal form, we would have to perform the decomposition of letbind that leads to the construction of the bind continuation for each expression with more than one subexpression. \ExecuteMetaData[Session0.tex]decompose-bind The function split-env splits the incoming environment according to the splitting sp, split-rotate performs a splitting rotation for typing environments, and the action of ssplit-compose is explained in Figure 9. We omit their definitions from the paper.

If decompose finds a value expression (e.g., a variable, a unit, or a pair), it constructs the value and arranges to invoke the continuation. For illustration, we consider the case for unit. Execution of such a value expression creates a Ready command. It represents a pending computation by a value and a continuation. This command instructs the scheduler to apply the continuation to the value. \ExecuteMetaData[Session0.tex]Command-Ready

\ExecuteMetaData[Session0.tex]decompose-unit The argument to VUnit is the proof that the value environment contains no resources, which follows from the fact that the typing environment is unrestricted as evidenced by unr-. Lemma inactive-venv provides this proof.

The other value expressions follow the same pattern. For example, the implementation of variable access fetches the value from the environment using access and then requires some type manipulation using Agda’s rewrite facility, which we leave uncommented. As this pattern occurs for all one argument operations, we abstract it in a function decompose-one (type elided). \ExecuteMetaData[Session0.tex]decompose-var \ExecuteMetaData[Session0.tex]decompose-one

The remaining operations (fork, new, close, wait, recv, send) just yield an appropriate Command.

\ExecuteMetaData

[Session0.tex]Command-Fork The Fork command contains two continuations (thunks, really), one for the newly created thread and the other for continuing the existing thread. The scheduler applies each thunk to the unit value. Its construction in decompose is a tedious exercise in resource shuffling and hence omitted.

\ExecuteMetaData

[Session0.tex]Command-New

\ExecuteMetaData[Session0.tex]decompose-new The New command asks the scheduler to create a new channel. The s component specifies the session type of the channel and the continuation component expects a pair of channel endpoints with types s and dual s.

\ExecuteMetaData

[Session0.tex]Command-Close

\ExecuteMetaData[Session0.tex]decompose-close The Close command is just another one argument expression and can be treated like the variable access. The definition and processing of the Wait and Recv commands are analogous. Decomposition of the Send command is slightly more involved because the send expression takes a splitting, a channel value, and a value to send. Hence, before accessing the environment $\varrho$ as with close, we first have to split the incoming environment using split-env. Each part of the environment is treated as shown in decompose-one.

4.5. Executing Commands in the Thread Pool

The scheduler actually drives the execution. It operates on the thread pool, which is represented by a list of commands.

\ExecuteMetaData

[Session0.tex]ThreadPool The type of the thread pool ThreadPool G is indexed by the session context which is split among all commands (cf. Figure 7). The empty thread pool tnil holds no resources as indicated by Inactive G. A non-empty thread pool tcons splits the resources between the current thread and the rest of the thread pool.

Figure 13 contains type definitions for the scheduler. Its core is a step function that attempts a single reduction on the thread pool and the main scheduler executes steps in a round robin fashion. A step generates an Event that describes the reduction performed, if any. Terminated means that no further step can be taken because all threads have terminated. Restarted means that a Ready thread has been restarted. Stuck means that no step is possible due to a deadlock situation. We describe further events in the rest of this section, as they show up.

All events coming out of a step are accompanied by a thread pool. The particular session context after the step is obtained by context reduction as specified in Figure 14. A context reduction ⇒ either leaves the context unchanged (RedIdent), adds a new channel (RedNew), or performs a reduction step on an existing channel type (RedInternal) using the internal reduction relation ⇒′. This relation is structured analogously to de Bruijn indices. Either the reduction takes place at a context entry below the top (RedThere), the current channel gets closed (RedEnd), or the current channel performs a transmission operation (RedTransmit). The NextPool type encapsulates the event, the reduction, and the resulting context.

Figure 15 contains the type of step and the first few cases. The function traverses the thread pool using a zipper represented by two lists of type ThreadPool. The focus of the zipper is the head of the first list. The initial call is shown in single-step. It passes the current thread pool as the first argument and an empty pool as the second. The step function considers commands from the first list and either executes them or moves them to the second list.

In the first case for step, both lists are empty and the program terminates normally with the identity context reduction RedIdent.

In the second case, the first list is empty, but the second is not. This configuration indicates a deadlock because the step function was not able to execute any command in the thread pool.

The third case deals with the Ready command. It applies the continuation to the value from the command. Operationally, it resumes executing the body of the next enclosing letbind and decompose it. The thread is moved to the end of the pool (tsnoc) and the two parts of the pool are merged (tappend and treverse).888Round robin scheduling would put the current thread at the very end. We simplified this matter to avoid further trickery with splittings.

The fourth case deals with the Halt command. It indicates the termination of an individual thread, which is removed from the thread pool. Again, the two parts of the thread pool are merged.

Before carrying on with further cases of the step function, we take a look at the top-level scheduler. \ExecuteMetaData[Schedule3.tex]schedule The scheduler repeatedly applies the single-step function to a thread pool. At this point we cannot easily predict termination, so the scheduler runs on a provided supply of Gas. It either terminates by issuing an OutOfGas if the gas is depleted, Terminated if single-step came to an end, or Stuck if a deadlock was detected.

To load an expression, we construct a one-element thread pool from decomposing it and pass it to the scheduler. \ExecuteMetaData[Schedule3.tex]start

4.6. Channel Creation

The New command is quite instructive (see Figure 16). Creating a channel means to extend the global session context G with a new entry. Moreover, in the current thread the new entry must be just (s, POSNEG), but it must be nothing for everybody else.

This extension happens rather indirectly in the code. The telltales are the uses of the splitting constructor ss-left, which indicate that the user of the topmost resource is the VPair value in the ready thread. Inside the pair, ss-posneg indicates that the channel resource is split into its two ends, which are used up in the VChan values. Both refer to the topmost resource as indicated by the here-pos and here-neg indices. This information together with the type of the continuation fully determines the type of the topmost resource.

Moreover, the rest of the thread pool in tp and tp2 as well as the continuation are still typed with the previous context before creating the new channel. Hence, the scheduler must weaken every other command in the thread pool and the continuation by prepending nothing. Weakening a command consists of weakening its contents, recursively: continuations, value environments, values, and resource splittings. This weakening is straightforward because we chose to expose all values in a thread in traversable data types. Weakening is implemented by the lift functions.

4.7. Close and Wait

A waiting thread just stays in the thread pool as shown in Figure 17. The extra code implements one of the ubiquitous resource rotations.

To execute the Close command (Figure 18), the scheduler checks all other threads for a matching Wait command (with essentially the same typing up to the session type SEnd?). The key part of this tedious matching is to compare the channel references of two channel values, which is implemented in the vcr-match function. \ExecuteMetaData[AlternativeMatch3.tex]vcr-match The implementation is surprisingly straightforward (see Figure 19) and the proof obligations for the result can only be fulfilled by two matching channel ends. First, the channel references must refer to opposite ends of the same channel. Second, there has to be an internal context reduction step that leads to an inactive context. This requirement can be satisfied because the context G that we start with only holds the resources for the two channel ends. Closing this channel sets this resource to inactive, which is also apparent from the RedEnd reduction in Figure 14.

The enclosing function matchWaitAndGo is much more tricky to implement. It searches the thread pool for the wait command and actually closes the channel.

\ExecuteMetaData

[AlternativeMatch3.tex]matchWaitAndGo

The parameter G is the session context of the thread pool. It is first split into the resources needed for the Close command (Gc), the channel to be closed and the continuation, and the remaining thread pool (Gtp). The thread pool itself is passed as a worklist of type ThreadPool Gtpwl. The parameter of type ThreadPool Gtpacc is used in recursive calls as an accumulating parameter to collect commands that do not match the Close.

Most cases of matchWaitAndGo are boring as they deal with all non-Wait constructors in the same way. In each case, there is a minor resource rotation to account for reorganization of the pool. We show the case for the New command as an example. \ExecuteMetaData[AlternativeMatch3.tex]matchWaitAndGo-new

The interesting case for the Wait command is too involved to discuss it here. The main complication is due to resource rotations, the actual work is performed by vcr-match.

4.8. Send and Receive

Sending and receiving gives rise to two new commands for the scheduler, Send and Recv (Figure 20), which follow the same pattern as the commands discussed in Section 4.4.

The scheduler processes Send and Recv analogously to Close and Wait. A Send command triggers a search for a matching Recv among the other threads. The core of this search is again the matching of the channel ends implemented in vcr-match-2-sr, but its typing (in Figure 21) is more involved.

The main issue in this match is the transfer of resources between the two threads. Three parties participate in this transfer, the receiving thread, the sending thread, and the rest of the threadpool. The sender and receiver may exchange resources as channels may be transferred over channels, whereas the resources of the rest of the threadpool remain unaffected. To implement this transfer in terms of splitting trees, we rearrange the tree according to the type Junction (Figure 22). This single type (or its mirror image) with its two nested splittings is sufficient to manage all resource transfers in a binary session type system because there are never more than three parties involved, two active ones and one inactive.

In the reduction step the receiving end as well as the sending channel end change their type. Hence, all contexts on the path up to the global context (yellow boxes in Figure 22) need to make a reduction step with relation $\Rightarrow^{\prime}$ as indicated by the existentials in the type of vcr-match-2-sr. The last two components of the output tuple document this reduction. Furthermore, the function must prove that G₂, which contains all remaining resources of the system, remains unaffected by this update. The equality proofs are again instrumental to demonstrate that the vcr-match-2-sr function found the two ends of the same channel.

The scheduler actually transfers the resources from sending thread ($G_{12}$) to receiving thread ($G_{11}$). Figure 23 illustrates the transfer with an example. Figure 23(a) (left) shows the splitting tree before the communication and Figure 23(b) (right) illustrates the splitting immediately after. Before the communication the sender holds two resources: the sending end of a channel vchS and the value v that should be transmitted (in the brown box); the value v is itself a channel end. The receiver holds just one resource: the receiving end vchR corresponding to vchS. Hence, the transferred resource is a single channel end v in this example, but in general it could be an arbitrary chunk of resources.

After the communication (Figure 23(b)), the receiver $G_{11}^{\prime}$ holds two resources in the pair indexed with G1R: the channel end vchR and the received value v. The sender $G_{12}^{\prime}$ only retains the channel end vchS, but “lost” the resource in v. All context entries marked with “XX” change to account for the context reduction that models the send/receive operation.

The commands in both threads change to the command Ready, which holds a pair of channel end and received value and the continuation after receiving on the left and the other channel end and the continuation after sending on the right.

The code for implementing the resource rotation shown in Figure 23 is tedious and therefore omitted from the paper. The definition of type Junction, which contains two nested splits arranged as shown in Figure 22, embodies an important insight. It corresponds to the tip of the resource tree in Figure 23 and the insight is that this tip must be transformed as a whole.

5. The Full Picture

Building on the established basis of MicroSession, we discuss the addition of the remaining ingredients of session typing, which are present in the calculi of GayHole2005 and/or GayVasconcelos2010-jfp. In particular, we consider

(1) internal and external choice,

(2) functions and recursion, (3) recursive sessions,

(4) subtyping,

(5) structured gas,

(6) and asynchrony.

5.1. Internal and External Choice

Internal and external choice require an additional session type constructors. \ExecuteMetaData[Extension3.tex]SChoice This constructor represents $m$-ary choice where m is the number of alternatives and cases is a function from Fin m to STy, where Fin m is the finite type of numbers $\{0,\dots,m-1\}$.999Data.Fin from the Agda standard library.

Expressions extend in the obvious way. \ExecuteMetaData[Extension3.tex]SChoice-syntax The expression nselect lab ch corresponds to an internal choice of the alternative lab on channel ch. The result is a channel of the type selected by the lab.

The expression nbranch sp ch cases announces an external choice on channel ch. The cases argument holds a function that maps the alternative number lab to an expression that is abstracted over the corresponding continuation channel of type (alt lab).

The corresponding new commands follow the familiar pattern. \ExecuteMetaData[Extension3.tex]SChoice-commands Resources are split between the channel value vch, on which the choice is made, and the continuation. For internal choice (NSelect), there is only one continuation, whereas external choice (NBranch) selects its continuation according to the label received.

The step function leaves the passive NBranch command in the thread pool. The NSelect command invokes a function analogous to matchWaitAndGo, which in turn relies on a channel match similar to vcr-match. As there are no resources to transfer between the threads, the resource rotation is less involved than in Section 4.8.

Alternatively, we can follow DBLP:conf/esop/LindleyM15 or DBLP:conf/esop/Padovani17 who encode choice using sum types. However, Lindley and Morris create a new channel at every choice, which would change our invariants about resource usage, whereas Padovani requires clever retyping of the channel at the receiving end.

5.2. Recursive Sessions

To extend our model to recursive sessions, we revise the type structure following DBLP:journals/jfp/AbelAS17. Session types are modeled as the greatest fixed point of a functor STF, which models the different session type constructors. The greatest fixed point is obtained with a coinductive record type (SType). The channel type TChan refers to the unraveled session type STF SType, on which we can pattern match (unlike the type SType, the values of which need to be forced). This change causes only minor modifications of the code.

• •

We define a coinductive type equivalence relation and prove its reflexivity, symmetry, and transitivity. Definitions follow the same pattern as for STF and SType. Proofs are tedious, but straightforward. Uses of propositional equality on Type are replaced by explicit use of the equivalence relation.

• •

We provide a coinductive definition of duality along with a coinductive proof that duality is involutory.

• •

The types of expressions that manipulate session types force their session typed arguments, as in the type of new: \ExecuteMetaData[Extension3.tex]rectypes-new

5.3. Subtyping

Subtyping of session types arises from the choice types. Our notion of subtyping derives from Liskov’s substitution principle as in GV (GayVasconcelos2010-jfp). A channel with an internal choice can be subsumed to a choice with fewer alternatives (the supertype). Dually, a channel with an external choice can be subsumed to a choice with more alternatives, as it is always ok to accept more alternatives than needed.

In our modeling, a selection (internal choice) on a Fin m can be subsumed to any Fin $m^{\prime}$ with $m^{\prime}\leq m$. Analogously, a branch (external choice) on a Fin m can be subsumed to any Fin $m^{\prime}$ with $m\leq m^{\prime}$. In connection with recursive session types, the definition of subtyping is also coinductive. It uses the same style as the coinductive definition of session types.

The remaining changes in the framework are straightforward. Expressions are extended with an explicit subsumption constructor that implements the type subsumption rule. At run time, subsumption is implemented by a coercion that adjusts the type of channel values and expressions inside of continuations.

5.4. Adequacy

We investigated some metatheoretical properties of our model. As we implement the lambda calculus reductions indirectly via the stuttering CEK machine, an obvious question to ask is whether execution is adequate with respect to standard lambda calculus reductions.

For example, we investigate adequacy of beta reduction for functions and pairs in all contexts. In module Properties.StepBeta we show that $\mathtt{let}\ f=(\lambda x.e)\ \mathtt{in}\ \mathtt{let}\ z=(f\ y)\ \mathtt{in}\ E$ is equal to $\mathtt{let}\ z=e[y/x]\ \mathtt{in}\ E$. In module Properties.StepPair we show that $\mathtt{let}\ p=(a,b)\ \mathtt{in}\ \mathtt{let}\ (x,y)=p\ \mathtt{in}\ E$ is equal to $E[a,b/x,y]$. In both cases, equality is formalized as identity after a fixed number of steps as in restart (restart lhs) ≡ rhs. Here lhs is the machine state loaded with the term before reduction and rhs is the same after reduction. Function restart performs one step of the CEK machine. These modules are available in the GitHub repository.

There are analogous results about the execution of close/wait, fork, and new. However, these statements and their proofs refer to process calculus reductions and they are restricted to very simple contexts. The proofs for general contexts get very complex and we have not been able to complete them.

5.5. Structured Gas

The present scheduler relies on a Gas type that is isomorphic to the natural numbers. As the scheduler is a function, the execution only covers one particular schedule. To obtain arbitrary interleavings, we may adopt structured gas, which is isomorphic to a list of numbers. Whenever the scheduler is invoked with a gas element n, it rotates the thread pool by $n$ positions before trying to make a step. As the interpreter works with any structured gas value, any schedule can be explored in this way.

5.6. Asynchrony

The presented framework models synchronous communication and it is obvious to ask for a model of asynchronous communication. The standard formalization in the literature (GayVasconcelos2010-jfp) adds extra queue processes that keep sent messages until their receiver is ready to accept them. In contrast, we encode an asynchronous channel of type $s$ as a promise for such a channel. A promise for $s$ is a single-shot synchronous channel from which we can receive a synchronous payload channel of type $s$. \ExecuteMetaData[Typing3.tex]async Our scheme represents one asynchronous channel by three synchronous channels: the payload channel and one promise channel at each end. The promise channel is replaced by each operation so that there is a chain of promises at each end which simulates an unbounded buffer. We achieve asynchronous operation by performing all potentially blocking operations on promise and payload channels in a separate thread.

Asynchronous sending creates a new promise channel (with ends receiver and sender), forks a process to perform the send, and immediately returns the receiving end of the promise channel. The forked process synchronously receives the actual channel schan from the previous promise achan, sends the value, and finally sends the depleted channel to the new promise. Here is the pseudocode: