Session-Typed Concurrent Contracts

As a first simple example let’s take a process that receives one positive integer n and factors it into two integers p and q that are sent back where \(p \le q\). The part of the specification that is not enforced is that if n is not prime, p and q should be proper factors, but we at least enforce that all numbers are positive and \(n = p * q\). We are being very particular here, for the purpose of exposition, marking the place where the direction of communication changes with a shift (\({\uparrow }\)). Since a minimal number of shifts can be inferred during elaboration of the syntax [18], we suppress it in most examples.This is a one-time interaction (the session type \(\mathsf {factor\_t}\) is not recursive), so the monitor terminates. It terminates here by forwarding, but we could equally well have replaced it by its identity-expanded version at type \(\mathbf {1}\), which is \(\mathsf {wait}\; d \mathrel {;}\mathsf {close}\; c\).

The contract could be invoked by the provider or by the client. Let’s consider how a provider \(\mathsf {factor}\) might invoke it:To check that \(\mathsf {factor\_monitor}\) is a partial identity we need to track that p and q are received from the provider, in this order. In general, for any received message, we need to enter it into a message queue q and we need to check that the messages are passed on in the correct order. As a first cut (to be generalized several times), we write for negative types:which expresses that the two endpoints of the monitor are \(a : A^-\) and \(b : B^-\) (both negative), and we have already received the messages in q along a. The context \(\varPsi \) declares types for local variables.

A monitor, at the top level, is defined withwhere context \(\varPsi \) declares value variables x. The body P here is type-checked as one of (depending on the polarity of A)where \(\varPsi = (x_1{:}\tau _1)\cdots (x_n{:}\tau _n)\). A use such asis transformed intofor a fresh \(c'\) and type-checked accordingly.

In general, queues have the form \(q = m_1 \cdots m_n\) withwhere \(m_1\) is the front of the queue and \(m_n\) the back.

When a process P receives a message, we add it to the end of the queue q. We also need to add it to \(\varPsi \) context, marked as unrestricted (non-linear) to remember its type. In our example \(\tau = \mathsf {int}\).Conversely, when we send along b the message must be equal to the one at the front of the queue (and therefore it must be a variable). The m is a value variable and remains in the context so it can be reused for later assertion checks. However, it could never be sent again since it has been removed from the queue.All the other send and receive rules for negative types (\(\forall \), , ) follow exactly the same pattern. For positive types, a queue must be associated with the channel along which the monitor provides (the succedent of the sequent judgment).Moreover, when \(\mathsf {end}\) has been received along b the corresponding process has terminated and the channel is closed, so we generalize the judgment toThe shift messages change the direction of communication. They therefore need to switch between the two judgments and also ensure that the queue has been emptied before we switch direction. Here are the two rules for \({\uparrow }\), which appears in our simple example:We notice that after receiving a \(\mathsf {shift}\), the channel a already changes polarity (we now have to send along it), so we generalize the judgment, allowing the succedent to be either positive or negative. And conversely for the other judgment.When we send the final shift, we initialize a new empty queue. Because the queue is empty the two sides of the monitor must have the same type.The rules for forwarding are also straightforward. Both sides need to have the same type, and the queue must be empty. As a consequence, the immediate forward is always a valid monitor at a given type.

The current rules allow us to communicate only along the channels a and b that are being monitored. If we send channels along channels, however, these channels must be recorded in the typing judgment, but we are not allowed to communicate along them directly. On the other hand, if we spawn internal (local) channels, say, as auxiliary data structures, we should be able to interact with them since such interactions are not externally observable. Our judgment thus requires two additional contexts: \(\varDelta \) for channels internal to the monitor, and \(\varGamma \) for externally visible channels that may be sent along the monitored channels. Our full judgments therefore areSo far, it is given by the following rules

The most complex part of checking that a process is a valid monitor involves spawning new processes. In order to be able to spawn and use local (private) processes, we have introduced the (so far unused) context \(\varDelta \) that tracks such channels. We use it here only in the following two rules:The second premise (that is, the continuation of the monitor) remains the monitor, while the first premise corresponds to a freshly spawned local progress accessible through channel c. All the ordinary left rules for sending or receiving along channels in \(\varDelta \) are also available for the two monitor validity judgments. By the strong ownership discipline of intuitionistic session types, none of this information can flow out of the monitor.

It is also possible for a single monitor to decompose into two monitors that operate concurrently, in sequence. In that case, the queue q may be split anywhere, as long as the intermediate type has the right polarity. Note that \(\varGamma \) must be chosen to contain all channels in \(q_2\), while \(\varGamma '\) must contain all channels in \(q_1\).Why is this correct? The first messages sent along a will be the messages in \(q_1\). If we receive messages along c in the meantime, they will be first the messages in \(q_2\) (since P is a monitor), followed by any messages that P may have received along b if \(\omega = (b : B)\). The second rule is entirely symmetric, with the flow of messages in the opposite direction.The next two rules allow a monitor to be attached to a channel x that is passed between a and b. The monitored version of x is called \(x'\), where \(x'\) is chosen fresh. This apparently violates our property that we pass on all messages exactly as received, because here we pass on a monitored version of the original. However, if monitors are partial identities, then the original x and the new \(x'\) are indistinguishable (unless a necessary alarm is raised), which will be a tricky part of the correctness proof.There are two more versions of these rules, depending on whether the types of x and the monitored types are positive or negative. These rules play a critical role in monitoring higher-order processes, because monitoring may require us to monitor the continuation \(c : B^-\) (already covered) but also communication along the channel \(x : A^+\) received along c.

In actual programs, we mostly use cut \(x \leftarrow P \mathrel {;}Q\) in the form \(x \leftarrow p\; \overline{e} \leftarrow \overline{d} \mathrel {;}Q\) where p is a defined process. The rules are completely analogous, except that for those rules that require splitting a context in the conclusion, the arguments \(\overline{d}\) will provide the split for us. When a new sub-monitor is invoked in this way, we remember and eventually check that the process p must also be a partial identity process, unless we are already checking it. This has the effect that recursively defined monitors with proper recursive calls are in fact allowed. This is important, because monitors for recursive types usually have a recursive structure. An illustration of this can be seen in \(\mathsf {pos}\) in Fig. 1.

We need to show that monitors are transparent, that is, they are indeed observationally equivalent to partial identity processes. Because of the richness of types and process expressions and the generality of the monitors allowed, the proof has some complexities. First, we define the configuration typing, which consists of just three rules. Because we also send and receive ordinary values, we also need to type (closed) substitutions \(\sigma = (v_1/n_1, \ldots , v_k/n_k)\) using the judgment \(\sigma :\,\!: \varPsi \).For configurations, we use the judgmentwhich expresses that process configuration \(\mathcal {C}\) uses the channels in \(\varDelta \) and provides the channels in \(\varDelta '\). Channels that are neither used nor offered by \(\mathcal {C}\) are “passed through”. Messages are just a restricted form of processes, so they are typed exactly the same way. We write \({ {pred}}\) for either \(\mathsf {proc}\) or \(\mathsf {msg}\).To characterize observational equivalence of processes, we need to first characterize the possible messages and the direction in which they flow: towards the client (channel type is positive) or towards the provider (channel type is negative). We summarize these in the following table. In each case, c is the channel along with the message is transmitted, and \(c'\) is the continuation channel.The notion of observational equivalence we need does not observe “nontermination”, that is, it only compares messages that are actually received. Since messages can flow in two directions, we need to observe messages that arrive at either end. We therefore do not require, as is typical for bisimulation, that if one configuration takes a step, another configuration can also take a step. Instead we say if both configurations send an externally visible message, then the messages must be equivalent.

Supposing \(\varGamma \vdash \mathcal {C}: \varDelta \) and \(\varGamma \vdash \mathcal {D}:\,\!: \varDelta \), we write \(\varGamma \vdash \mathcal {C}\sim \mathcal {D}:\,\!: \varDelta \) for our notion of observational equivalence. It is the largest relation satisfying that \(\varGamma \vdash \mathcal {C}\sim \mathcal {D}: \varDelta \) implies

Clauses (1) and (2) correspond to absorbing a message into a configuration, which may later be received by a process according to clauses (5) and (6).

Clauses (3) and (4) correspond to observing messages, either by a client (clause (3)) or provider (clause (4)).

In clause (3) we take advantage of the property that a new continuation channel in the message P (one that does not appear already in \(\varGamma \)) is always chosen fresh when created, so we can consistently (and silently) rename it in \(\mathcal {C}'\), \(\varDelta _1'\), and P (and \(\mathcal {D}'\), \(\varDelta _2'\), and Q, respectively). This slight of hand allows us to match up the context and messages exactly. An analogous remark applies to clause (4). A more formal description would match up the contexts and messages modulo two renaming substitution which allow us to leave \(\varGamma \) and \(\varDelta \) fixed.

Clauses (5) and (6) make sense because a transition never changes the interface to a configuration, except when executing a forwarding \(\mathsf {proc}(a, a \leftarrow b)\) which substitutes b for a in the remaining configuration. We can absorb this renaming into the renaming substitution. Cut creates a new channel, which remains internal since it is linear and will have one provider and one client within the new configuration. Unfortunately, our notation is already somewhat unwieldy and carrying additional renaming substitutions further obscures matters. We therefore omit them in this presentation.

We now need to define a relation \(\sim _M\) such that (a) it satisfies the closure conditions of \(\sim \) and is therefore an observational equivalence, and (b) allows us to conclude that monitors satisfying our judgment are partial identities. Unfortunately, the theorem is rather complex, so we will walk the reader through a sequence of generalizations that account for various phenomena.

The   Fragment. For this fragment, we have no value variables, nor are we passing channels. Then the top-level properties we would like to show are     Of course, asserting that \(\mathsf {proc}(x, x \leftarrow y) \sim _M P\) will be insufficient, because this relation is not closed under the conditions of observational equivalence. For example, if we add a message along y to both sides, P will change its state once it receives the message, and the queue will record that this message still has to be sent. To generalize this, we need to define the queue that corresponds to a sequence of messages. First, a single message:We extend this to message sequences with \(\langle \!\langle \; \rangle \!\rangle = (\cdot )\) and \(\langle \!\langle \mathcal {E}_1, \mathcal {E}_2\rangle \!\rangle = \langle \!\langle \mathcal {E}_1\rangle \!\rangle \cdot \langle \!\langle \mathcal {E}_2\rangle \!\rangle \), provided \(\varDelta _0 \vdash \mathcal {E}_1 : \varDelta _1\) and \(\varDelta _1 \vdash \mathcal {E}_2 :\,\!: \varDelta _2\).

Then we build into the relation that sequences of messages correspond to the queue.    

When we add shifts the two propositions become mutually dependent, but otherwise they remain the same since the definition of \(\langle \!\langle \mathcal {E}\rangle \!\rangle \) is already general enough. But we need to generalize the type on the opposite side of queue to be either positive or negative, because it switches polarity after a shift has been received. Similarly, the channel might terminate when receiving \(\mathbf {1}\), so we also need to allow \(\omega \), which is either empty or of the form y : B.     Next, we can permit local state in the monitor (rules \(\mathsf {cut}_1^+\) and \(\mathsf {cut}_1^-\)). The fact that neither of the two critical endpoints y and x, nor any (non-local) channel,s can appear in the typing of the local process is key. That local process will evolve to a local configuration, but its interface will not change and it cannot access externally visible channels. So we generalize to allow a configuration \(\mathcal {D}\) that does not use any channels, and any channels it offers are used by P.     Next, we can allow value variables necessitated by the universal and existential quantifiers. Since they are potentially dependent, we need to apply the closing substitution \(\sigma \) to a number of components in our relation.     Breaking up the queue by spawning a sequence of monitors (rule \(\mathsf {cut}_2^+\) and \(\mathsf {cut}_2^-\)) just comes down to the compositionally of the partial identity property. This is a new and separate way that two configurations might be in the \(\sim _M\) relation, rather than a replacement of a previous definition.    

At this point, the only types that have not yet accounted for are \(\otimes \) and . If these channels were only “passed through” (without the four \(\mathsf {cut}_3\) rules), this would be rather straightforward. However, for higher-order channel-passing programs, a monitor must be able to spawn a monitor on a channel that it receives before sending on the monitored version. First, we generalize properties (5) to allow the context \(\varGamma \) of channels that may occur in the queue q and the process P, but that P may not interact with.     In addition we need to generalize property (6) into (8) and (9) to allow multiple monitors to run concurrently in a configuration.    

At this point we can state the main theorem regarding monitors.

By applying it as in equations (\(1^+\)) and (\(1^-\)), generalized to include value variables as in (\(5^+\)) and (\(5^-\)) we obtain:

We first augment messages and processes to include casts as follows. We write \(\langle A \Leftarrow B \rangle ^{\rho }\) to denote a cast from type B to type A, where \(\rho \) is a unique label for the cast. The cast for values is written as (\(\langle \tau \Leftarrow \tau ' \rangle ^{\rho }\)). Here, the types \(\tau '\) and \(\tau \) are refinement types of the form \(\{n{:}t\mid b\}\), where b is a boolean expression that expresses simple properties of the value n.Adding casts to forwarding is expressive enough to encode a more general cast \(\langle A \Leftarrow B \rangle ^{\rho } P\). For instance, the process \(x{:}A \leftarrow \langle A \Leftarrow B \rangle ^{\rho }{P} \mathrel {;}Q_x\) can be encoded as: \( y{:}B \leftarrow P; x{:}A \leftarrow \langle A \Leftarrow B \rangle ^{\rho }\ y \mathrel {;}Q_x\).

One of the additional rules to type casts is shown below (both rules can be found in Fig. 6). We only allow casts between two types that are compatible with each other (written \(A\sim B\)), which is co-inductively defined based on the structure of the types (the full definition is omitted from the paper).

At run time, casts are translated into monitoring processes. A cast \(a\leftarrow \langle A \Leftarrow B \rangle ^{\rho }\ b\) is implemented as a monitor. This monitor ensures that the process that offers a service on channel b behaves according to the prescribed type A. Because of the typing rules, we are assured that channel b must adhere to the type B.

Figure 4 is a summary of all the translation rules, except recursive types. The translation is of the form: \([\![\langle A \Leftarrow B \rangle ^{\rho }]\!]_{a, b} = P\), where A, B are types; the channels a and b are the offering channel and monitoring channel (respectively) for the resulting monitoring process P; and \(\rho \) is a label of the monitor (i.e., the contract).

Note that this differs from blame labels for high-order functions, where the monitor carries two labels, one for the argument, and one for the body of the function. Here, the communication between processes is bi-directional. Though the blame is always triggered by processes sending messages to the monitor, our contracts may depend on a set of the values received so far, so it does not make sense to blame one party. Further, in the case of forwarding, the processes at either end of the channel are behaving according to the types (contracts) assigned to them, but the cast may forcefully connect two processes that have incompatible types. In this case, it is unfair to blame either one of the processes. Instead, we raise an alarm of the label of the failed contract.

The translation is defined inductively over the structure of the types. The \(\mathsf {tensor}\) rule generates a process that first receives a channel (x) from the channel being monitored (b). It then spawns a new monitor (denoted by the \(\mathsf {@monitor}\) keyword) to monitor channel x, making sure that it behaves as type \(A_1\), and passes the new monitor’s offering channel y to channel a. Finally, the monitor continues to monitor b to make sure that it behaves as type \(A_2\). The \(\mathsf {lolli}\) rule is similar to the \(\mathsf {tensor}\) rule, except that the monitor first receives a channel from its offering channel. Similar to the higher-order function case, the argument position is contravariant, so the newly spawned monitor checks that the received channel behaves as type \(B_1\). The \(\mathsf {exists}\) rule generates a process that first receives a value from the channel b, then checks the boolean condition e to validate the contract. The \(\mathsf {forall}\) rule is similar, except the argument position is contravariant, so the boolean expression \(e'\) is checked on the offering channel a. The \(\mathsf {with}\) rule generates a process that checks that all of the external choices promised by the type are offered by the process being monitored. If a label in the set I is not implemented, then the monitor aborts with the label \(\rho \). The \(\mathsf {plus}\) rule requires that, for internal choices, the monitor checks that the monitored process only offers choices within the labels in the set \({\oplus }\{\ell : A_\ell \}_{\ell \in I}\).

For ease of explanation, we omit details for translating casts involving recursive types. Briefly, these casts are translated into recursive processes. For each pair of compatible recursive types A and B, we generate a unique monitor name f and record its type \(f:\{A \leftarrow B\}\) in a context \(\varPsi \). The translation algorithm needs to take additional arguments, including \(\varPsi \) to generate and invoke the appropriate recursive process when needed. For instance, when generating the monitor process for \(f:\{\mathsf {list}\leftarrow \mathsf {list}\}\), we follow the rule for translating internal choices. For \([\![\langle \mathsf {list} \Leftarrow \mathsf {list} \rangle ^{\rho }]\!]_{y, x}\) we apply the \(\mathsf {cons}\) case in the translation to get \(@\mathsf {monitor}\ y\leftarrow \ f\ \leftarrow x\).

We prove two formal properties of cast-based monitors: safety and transparency.

Because of the expressiveness of our contracts, a general safety (or blame) theorem is difficult to achieve. However, for cast-based contracts, we can prove that a cast which enforces a subtyping relation, and the corresponding monitor, will not raise an alarm. We first define our subtyping relation in Fig. 5. In addition to the subtyping between refinement types, we also include label subtyping for our session types. A process that offers more external choices can always be used as a process that offers fewer external choices. Similarly, a process that offers fewer internal choices can always be used as a process that offers more internal choices (e.g., non-empty list can be used as a list). The subtyping rules for internal and external choices are drawn from work by Acay and Pfenning [1]. For recursive types, we directly examine their definitions. Because of these recursive types, our subtyping rules are co-inductively defined.

We prove a safety theorem (i.e., well-typed casts do not raise alarms) via the standard preservation theorem. The key is to show that the monitor process generated from the translation algorithm in Fig. 4 is well-typed under a typing relation which guarantees that no \(\mathsf {abort}\) state can be reached. We refer to the type system presented thus far in the paper as T, where monitors that may evaluate to \(\mathsf {abort}\) can be typed. We define a stronger type system S which consists of the rules in T with the exception of the \(\mathsf {abort}\) rule and we replace the \(\mathsf {assert}\) rule with the \(\mathsf {assert\_strong}\) rule. The new rule for assert, which semantically verifies that the condition b is true using the fact that the refinements are stored in the context \(\varPsi \), is shown below. The two type systems are summarized in Fig. 6.

As a corollary, we can show that when executing in a well-typed context, a monitor process translated from a well-typed cast will never raise an alarm.

Finally, we prove that monitors translated from casts are partial identify processes.