Session-Typed Concurrent Contracts

Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10801)

Abstract

In sequential languages, dynamic contracts are usually expressed as boolean functions without externally observable effects, written within the language. We propose an analogous notion of concurrent contracts for languages with session-typed message-passing concurrency. Concurrent contracts are partial identity processes that monitor the bidirectional communication along channels and raise an alarm if a contract is violated. Concurrent contracts are session-typed in the usual way and must also satisfy a transparency requirement, which guarantees that terminating compliant programs with and without the contracts are observationally equivalent. We illustrate concurrent contracts with several examples. We also show how to generate contracts from a refinement session-type system and show that the resulting monitors are redundant for programs that are well-typed.

Keywords

Contracts Session types Monitors 

1 Introduction

Contracts, specifying the conditions under which software components can safely interact, have been used for ensuring key properties of programs for decades. Recently, contracts for distributed processes have been studied in the context of session types [15, 17]. These contracts can enforce the communication protocols, specified as session types, between processes. In this setting, we can assign each channel a monitor for detecting whether messages observed along the channel adhere to the prescribed session type. The monitor can then detect any deviant behavior the processes exhibit and trigger alarms. However, contracts based solely on session types are inherently limited in their expressive power. Many contracts that we would like to enforce cannot even be stated using session types alone. As a simple example, consider a “factorization service” which may be sent a (possibly large) integer x and is supposed to respond with a list of prime factors. Session types can only express that the request is an integer and the response is a list of integers, which is insufficient.

In this paper, we show that by generalizing the class of monitors beyond those derived from session types, we can enforce, for example, that multiplying the numbers in the response yields the original integer x. This paper focuses on monitoring more expressive contracts, specifically those that cannot be expressed with session types, or even refinement types.

To handle these contracts, we have designed a model where our monitors execute as transparent processes alongside the computation. They are able to maintain internal state which allows us to check complex properties. These monitoring processes act as partial identities, which do not affect the computation except possibly raising an alarm, and merely observe the messages flowing through the system. They then perform whatever computation is needed, for example, they can compute the product of the factors, to determine whether the messages are consistent with the contract. If the message is not consistent, they stop the computation and blame the process responsible for the mistake. To show that our contracts subsume refinement-based contracts, we encode refinement types in our model by translating refinements into monitors. This encoding is useful because we can show a blame (safety) theorem stating that monitors that enforce a less precise refinement type than the type of the process being monitored will not raise alarms. Unfortunately, the blame theory for the general model is challenging because the contracts cannot be expressed as types.

The main contributions of this paper are:
  • A novel approach to contract checking via partial-identity monitors

  • A method for verifying that monitors are partial identities, and a proof that the method is correct

  • Examples showing the breadth of contracts that our monitors can enforce

  • A translation from refinement types to our monitoring processes and a blame theorem for this fragment

The rest of this paper is organized as follows. We first review the background on session types in Sect. 2. Next, we show a range of example contracts in Sect. 3. In Sect. 4, we show how to check that a monitor process is a partial identity and prove the method correct. We then show how we can encode refinements in our system in Sect. 5. We discuss related work in Sect. 6. Due to space constraints, we only present the key theorems. Detailed proofs can be found in our companion technical report [12].

2 Session Types

Session types prescribe the communication behavior of message-passing concurrent processes. We approach them here via their foundation in intuitionistic linear logic [4, 5, 22]. The key idea is that an intuitionistic linear sequent
$$ A_1, \ldots , A_n \vdash C $$
is interpreted as the interface to a process expression P. We label each of the antecedents with a channel name \(a_i\) and the succedent with a channel name c. The \(a_i\) are the channels used and c is the channel provided by P.
$$ a_1:A_1, \ldots , a_n:A_n \vdash P :\,\!: (c : C) $$
We abbreviate the antecedents by \(\varDelta \). All the channels \(a_i\) and c must be distinct, and bound variables may be silently renamed to preserve this invariant in the rules. Furthermore, the antecedents are considered modulo exchange. Cut corresponds to parallel composition of two processes that communicate along a private channel x, where P is the provider along x and Q the client.Operationally, the process \(x \leftarrow P \mathrel {;}Q\) spawns P as a new process and continues as Q, where P and Q communicate along a fresh channel a, which is substituted for x. We sometimes omit the type A of x in the syntax when it is not relevant.

In order to define the operational semantics rigorously, we use multiset rewriting [6]. The configuration of executing processes is described as a collection \(\mathcal {C}\) of propositions \(\mathsf {proc}(c, P)\) (process P is executing, providing along c) and \(\mathsf {msg}(c, M)\) (message M is sent along c). All the channels c provided by processes and messages in a configuration must be distinct.

A \(\mathsf {cut}\) spawns a new process, and is in fact the only way new processes are spawned. We describe a transition \(\mathcal {C}\longrightarrow \mathcal {C}'\) by defining how a subset of \(\mathcal {C}\) can be rewritten to a subset of \(\mathcal {C}'\), possibly with a freshness condition that applies to all of \(\mathcal {C}\) in order to guarantee the uniqueness of each channel provided.
$$ \mathsf {proc}(c, x{:}A \leftarrow P \mathrel {;}Q) \longrightarrow \mathsf {proc}(a, [a/x]P), \mathsf {proc}(c, [a/x]Q) \quad (a~fresh) $$
Each of the connectives of linear logic then describes a particular kind of communication behavior which we capture in similar rules. Before we move on to that, we consider the identity rule, in logical form and operationally.Operationally, it corresponds to identifying the channels a and b, which we implement by substituting b for a in the remainder \(\mathcal {C}\) of the configuration (which we make explicit in this rule). The process offering a terminates. We refer to \(a \leftarrow b\) as forwarding since any messages along a are instead “forwarded” to b.

We consider each class of session type constructors, describing their process expression, typing, and asynchronous operational semantics. The linear logical semantics can be recovered by ignoring the process expressions and channels.

Internal and External Choice. Even though we distinguish a provider and its client, this distinction is orthogonal to the direction of communication: both may either send or receive along a common private channel. Session typing guarantees that both sides will always agree on the direction and kind of message that is sent or received, so our situation corresponds to so-called binary session types.

First, the internal choice \(c : A \oplus B\) requires the provider to send a token \(\mathsf {inl}\) or \(\mathsf {inr}\) along c and continue as prescribed by type A or B, respectively. For practical programming, it is more convenient to support n-ary labelled choice \({\oplus }\{\ell : A_\ell \}_{\ell \in L}\) where L is a set of labels. A process providing \(c : {\oplus }\{\ell : A_\ell \}_{\ell \in L}\) sends a label \(k \in L\) along c and continues with type \(A_k\). The client will operate dually, branching on a label received along c.The operational semantics is somewhat tricky, because we communicate asynchronously. We need to spawn a message carrying the label \(\ell \), but we also need to make sure that the next message sent along the same channel does not overtake the first (which would violate session fidelity). Sending a message therefore creates a fresh continuation channel \(c'\) for further communication, which we substitute in the continuation of the process. Moreover, the recipient also switches to this continuation channel after the message is received.
$$ \begin{array}{l} \mathsf {proc}(c, c.k \mathrel {;}P) \longrightarrow \mathsf {proc}(c', [c'/c]P), \mathsf {msg}(c, c.k \mathrel {;}c \leftarrow c') \quad (c'~fresh)\\ \mathsf {msg}(c, c.k \mathrel {;}c \leftarrow c'), \mathsf {proc}(d, \mathsf {case}\; c\; (\ell \Rightarrow Q_\ell )_{\ell \in L}) \longrightarrow \mathsf {proc}(d, [c'/c]Q_k) \end{array} $$
It is interesting that the message along c, followed by its continuation \(c'\) can be expressed as a well-typed process expression using forwarding \(c.k \mathrel {;}c \leftarrow c'\). This pattern will work for all other pairs of send/receive operations.
External choice reverses the roles of client and provider, both in the typing and the operational rules. Below are the semantics and the typing is in Fig. 6.
$$ \begin{array}{l} \mathsf {proc}(d, c.k \mathrel {;}Q) \longrightarrow \mathsf {msg}(c', c.k \mathrel {;}c' \leftarrow c), \mathsf {proc}(d, [c'/c]Q) \quad (c'~fresh) \\ \mathsf {proc}(c, \mathsf {case}\; c\; (\ell \Rightarrow P_\ell )_{\ell \in L}), \mathsf {msg}(c', c.k \mathrel {;}c' \leftarrow c) \longrightarrow \mathsf {proc}(c', [c'/c]P_k) \end{array} $$
Sending and Receiving Channels. Session types are higher-order in the sense that we can send and receive channels along channels. Sending a channel is perhaps less intuitive from the logical point of view, so we show that and just summarize the rules for receiving.
If we provide \(c : A \otimes B\), we send a channel a : A along c and continue as B. From the typing perspective, it is a restricted form of the usual two-premise \({\otimes }R\) rule by requiring the first premise to be an identity. This restriction separates spawning of new processes from the sending of channels.The operational rules follow the same patterns as the previous case.
$$ \begin{array}{l} \mathsf {proc}(c, \mathsf {send}\; c\; a \mathrel {;}P) \longrightarrow \mathsf {proc}(c', [c'/c]P), \mathsf {msg}(\mathsf {send}\; c\; a \mathrel {;}c \leftarrow c') \quad (c'~fresh) \\ \mathsf {msg}(c, \mathsf {send}\; c\; a \mathrel {;}c \leftarrow c'), \mathsf {proc}(d, x \leftarrow \mathsf {recv}\; c \mathrel {;}Q) \longrightarrow \mathsf {proc}(d, [c'/c][a/x]Q) \end{array} $$
Receiving a channel (written as a linear implication Open image in new window ) works symmetrically. Below are the semantics and the typing is shown in Fig. 6.
$$ \begin{array}{l} \mathsf {proc}(d, \mathsf {send}\; c\; a \mathrel {;}Q) \longrightarrow \mathsf {msg}(c', \mathsf {send}\; c\; a \mathrel {;}c' \leftarrow c), \mathsf {proc}(d, [c'/c]Q) \quad (c'~\text{ fresh }) \\ \mathsf {proc}(c, x \leftarrow \mathsf {recv}\; c \mathrel {;}P), \mathsf {msg}(c', \mathsf {send}\; c\; a \mathrel {;}c' \leftarrow c) \longrightarrow \mathsf {proc}(c', [c'/c][a/x]P) \end{array} $$
Termination. We have already seen that a process can terminate by forwarding. Communication along a channel ends explicitly when it has type \(\mathbf {1}\) (the unit of \(\otimes \)) and is closed. By linearity there must be no antecedents in the right rule.Since there cannot be any continuation, the message takes a simple form.
$$ \begin{array}{l} \mathsf {proc}(c, \mathsf {close}\; c) \longrightarrow \mathsf {msg}(c, \mathsf {close}\; c)\\ \mathsf {msg}(c, \mathsf {close}\; c), \mathsf {proc}(d, \mathsf {wait}\; c \mathrel {;}Q) \longrightarrow \mathsf {proc}(d, Q) \end{array} $$
Quantification. First-order quantification over elements of domains such as integers, strings, or booleans allows ordinary basic data values to be sent and received. At the moment, since we have no type families indexed by values, the quantified variables cannot actually appear in their scope. This will change in Sect. 5 so we anticipate this in these rules.
The proof of an existential quantifier contains a witness term, whose value is what is sent. In order to track variables ranging over values, a new context \(\varPsi \) is added to all judgments and the preceding rules are modified accordingly. All value variables n declared in context \(\varPsi \) must be distinct. Such variables are not linear, but can be arbitrarily reused, and are therefore propagated to all premises in all rules. We write \(\varPsi \vdash v : \tau \) to check that value v has type \(\tau \) in context \(\varPsi \).
$$ \begin{array}{l} \mathsf {proc}(c, \mathsf {send}\; c\; v \mathrel {;}P) \longrightarrow \mathsf {proc}(c', [c'/c]P), \mathsf {msg}(c, \mathsf {send}\; c\; v \mathrel {;}c \leftarrow c') \\ \mathsf {msg}(c, \mathsf {send}\; c\; v \mathrel {;}c \leftarrow c'), \mathsf {proc}(d, n \leftarrow \mathsf {recv}\; c \mathrel {;}Q) \longrightarrow \mathsf {proc}(d, [c'/c][v/n]Q) \end{array} $$
The situation for universal quantification is symmetric. The semantics are given below and the typing is shown in Fig. 6.
$$ \begin{array}{l} \mathsf {proc}(d, \mathsf {send}\; c\; v \mathrel {;}Q) \longrightarrow \mathsf {msg}(c', \mathsf {send}\; c\; v \mathrel {;}c' \leftarrow c), \mathsf {proc}(d, [c'/c]Q) \\ \mathsf {proc}(c, x \leftarrow \mathsf {recv}\; c \mathrel {;}P), \mathsf {msg}(c', \mathsf {send}\; c\; v \mathrel {;}c' \leftarrow c) \longrightarrow \mathsf {proc}(c', [c'/c][v/n]P) \end{array} $$
Processes may also make internal transitions while computing ordinary values, which we don’t fully specify here. Such a transition would have the form
$$ \mathsf {proc}(c, P[e]) \longrightarrow \mathsf {proc}(c, P[e']) \quad \text{ if }\quad e \mapsto e' $$
where P[e] would denote a process with an ordinary value expression in evaluation position and \(e \mapsto e'\) would represent a step of computation.
Shifts. For the purpose of monitoring, it is important to track the direction of communication. To make this explicit, we polarize the syntax and use shifts to change the direction of communication (for more detail, see prior work [18]).From the perspective of the provider, all negative types receive and all positive types send. It is then clear that \({\uparrow }A\) must receive a \(\mathsf {shift}\) message and then start sending, while \({\downarrow }A\) must send a \(\mathsf {shift}\) message and then start receiving. For this restricted form of shift, the logical rules are otherwise uninformative. The semantics are given below and the typing is shown in Fig. 6.
$$ \begin{array}{l} \mathsf {proc}(c, \mathsf {send}\; c\; \mathsf {shift} \mathrel {;}P) \longrightarrow \mathsf {proc}(c', [c'/c]P), \mathsf {msg}(c, \mathsf {send}\; c\; \mathsf {shift} \mathrel {;}c \leftarrow c') \quad \text{( }c' \text{ fresh) } \\ \mathsf {msg}(c, \mathsf {send}\; c\; \mathsf {shift} \mathrel {;}c \leftarrow c'), \mathsf {proc}(d, \mathsf {shift} \leftarrow \mathsf {recv}\; d \mathrel {;}Q) \longrightarrow \mathsf {proc}(d, [c'/c]Q) \\ \mathsf {proc}(d, \mathsf {send}\; d\; \mathsf {shift} \mathrel {;}Q) \longrightarrow \mathsf {msg}(c', \mathsf {send}\; c\; \mathsf {shift} \mathrel {;}c' \leftarrow c), \mathsf {proc}(d, [c'/c]Q) \\ \mathsf {proc}(c, \mathsf {shift} \leftarrow \mathsf {recv}\; c \mathrel {;}P), \mathsf {msg}(c', \mathsf {send}\; c\; \mathsf {shift} \mathrel {;}c' \leftarrow c) \longrightarrow \mathsf {proc}(c', [c'/c]P) \end{array} $$
Recursive Types. Practical programming with session types requires them to be recursive, and processes using them also must allow recursion. For example, lists with elements of type \(\mathsf {int}\) can be defined as the purely positive type \(\mathsf {list}^+\).
A provider of type \(c : \mathsf {list}\) is required to send a sequence such as \(\mathsf {cons} \cdot v_1 \cdot \mathsf {cons} \cdot v_2 \cdots \) where each \(v_i\) is an integer. If it is finite, it must be terminated with \(\mathsf {nil} \cdot \mathsf {end}\). In the form of a grammer, we could write
$$ { {From}} :\,\!:= \mathsf {cons} \cdot v \cdot { {From}} \mid \mathsf {nil} \cdot \mathsf {end} $$
A second example is a multiset (bag) of integers, where the interface allows inserting and removing elements, and testing if it is empty. If the bag is empty when tested, the provider terminates after responding with the \(\mathsf {empty}\) label.
The protocol now describes the following grammar of exchanged messages, where \({ {To}}\) goes to the provider, \({ {From}}\) comes from the provider, and v stands for integers.
$$ \begin{array}{lcl} { {To}} &{} :\,\!:= &{} \mathsf {insert} \cdot v \cdot { {To}} \mid \mathsf {remove} \cdot v \cdot { {To}} \mid \mathsf {is\_empty} \cdot \mathsf {shift} \cdot { {From}} \\ { {From}} &{} :\,\!:= &{} \mathsf {empty} \cdot \mathsf {end} \mid \mathsf {nonempty} \cdot \mathsf {shift} \cdot { {To}} \end{array} $$
For these protocols to be realized in this form and support rich subtyping and refinement types without change of protocol, it is convenient for recursive types to be equirecursive. This means a defined type such as \(\mathsf {list}^+\) is viewed as equal to its definition \({\oplus }\{ \ldots \}\) rather than isomorphic. For this view to be consistent, we require type definitions to be contractive [11], that is, they need to provide at least one send or receive interaction before recursing.

The most popular formalization of equirecursive types is to introduce an explicit \(\mu \)-constructor. For example, \( \mathsf {list} = \mu \alpha .\, {\oplus }\{\ \mathsf {cons} : \exists n{:}\mathsf {int}.\, \alpha , \mathsf {nil} : \mathbf {1}\ \} \) with rules unrolling the type \(\mu \alpha .\, A\) to \([(\mu \alpha .\, A)/\alpha ]A\). An alternative (see, for example, Balzers and Pfenning 2017 [3]) is to use an explicit definition just as we stated, for example, \(\mathsf {list}\) and \(\mathsf {bag}\), and consider the left-hand side equal to the right-hand side in our discourse. In typing, this works without a hitch. When we consider subtyping explicitly, we need to make sure we view inference systems on types as being defined co-inductively. Since a co-inductively defined judgment essentially expresses the absence of a counterexample, this is exactly what we need for the operational properties like progress, preservation, or absence of blame. We therefore adopt this view.

Recursive Processes. In addition to recursively defined types, we also need recursively defined processes. We follow the general approach of Toninho et al. [23] for the integration of a (functional) data layer into session-typed communication. A process can be named p, ascribed a type, and be defined as follows.
$$ \begin{array}{l} p : \forall n_1{:}\tau _1.\, \ldots , \forall n_k{:}\tau _k. \{ A \leftarrow A_1, \ldots , A_m \} \\ x \leftarrow p\, n_1\, \ldots \, n_k \leftarrow y_1, \ldots , y_m = P \end{array} $$
where we check \( (n_1{:}\tau _1, \ldots , n_k{:}\tau _k) \mathrel {;}(y_1{:}A_1, \ldots , y_m{:}A_m) \vdash P :\,\!: (x : A) \)
We use such process definitions when spawning a new process with the syntax
$$ c \leftarrow p\, e_1\, \ldots , e_k \leftarrow d_1, \ldots , d_m \mathrel {;}P $$
which we check with the ruleAfter evaluating the value arguments, the call consumes the channels \(d_j\) (which will not be available to the continuation Q, due to linearity). The continuation Q will then be the (sole) client of c and The new process providing c will execute \([c/x][d_1/y_1]\ldots [d_m/y_m]P\).

One more quick shorthand used in the examples: a tail-call \(c \leftarrow p\; \overline{e} \leftarrow \overline{d}\) in the definition of a process that provides along c is expanded into \(c' \leftarrow p\; \overline{e} \leftarrow \overline{d} \mathrel {;}c \leftarrow c'\) for a fresh \(c'\). Depending on how forwarding is implemented, however, it may be much more efficient [13].

Stopping Computation. Finally, in order to be able to successfully monitor computation, we need the capability to stop the computation. We add an \(\mathsf {abort} \ l\) construct that aborts on a particular label. We also add \(\mathsf {assert}\) blocks to check conditions on observable values. The semantics are given below and the typing is in Fig. 6.
$$ \begin{array}{l} \mathsf {proc}(c, \mathsf {assert} \ l \ \mathsf {True};Q) \longrightarrow \mathsf {proc}(c,Q) \mathsf {proc}(c, \mathsf {assert} \ l \ \mathsf {False};Q) \longrightarrow \mathsf {abort}(l) \end{array} $$
Progress and preservation were proven for the above system, with the exception of the \(\mathsf {abort}\) and \(\mathsf {assert}\) rules, in prior work [18]. The additional proof cases do not change the proof significantly.

3 Contract Examples

In this section, we present monitoring processes that can enforce a variety of contracts. The examples will mainly use lists as defined in the previous section. Our monitors are transparent, that is, they do not change the computation. We accomplish this by making them act as partial identities (described in more detail in Sect. 4). Therefore, any monitor that enforces a contract on a list must peel off each layer of the type one step at a time (by sending or receiving over the channel as dictated by the type), perform the required checks on values or labels, and then reconstruct the original type (again, by sending or receiving as appropriate).

Refinement. The simplest kind of monitoring process we can write is one that models a refinement of an integer type; for example, a process that checks whether every element in the list is positive. This is a recursive process that receives the head of the list from channel b, checks whether it is positive (if yes, it continues to the next value, if not it aborts), and then sends the value along to reconstruct the monitored list a. We show three refinement monitors in Fig. 1. The process pos implements the refinement mentioned above.
Fig. 1.

Refinement examples

Our monitors can also exploit information that is contained in the labels in the external and internal choices. The \(\mathtt {empty}\) process checks whether the list b is empty and aborts if b sends the label \(\mathtt {cons}\). Similarly, the \(\mathtt {nempty}\) monitor checks whether the list b is not empty and aborts if b sends the label \(\mathtt {nil}\). These two monitors can then be used by a process that zips two lists and aborts if they are of different lengths. These two monitors enforce the refinements \(\{\mathtt{nil}\} \subseteq \{\mathtt{nil}, \mathtt{cons}\}\) and \(\{\mathtt{cons}\} \subseteq \{\mathtt{nil}, \mathsf {cons}\}\). We discuss how to generate monitors from refinement types in more detail in Sect. 5.

Monitors with Internal State. We now move beyond refinement contracts, and model contracts that have to maintain some internal state (Fig. 2).

We first present a monitor that checks whether the given list is sorted in ascending order (\(\mathtt {ascending}\)). The monitor’s state consists of a lower bound on the subsequent elements in the list. This value has an option type, which can either be \(\mathtt {None}\) if no bound has yet been set, or Some b if b is the current bound.
Fig. 2.

Monitors using internal state

If the list is empty, there is no bound to check, so no contract failure can happen. If the list is nonempty, we check to see if a bound has already been set. If not, we set the bound to be the first received element. If there is already a bound in place, then we check if the received element is greater or equal to the bound. If it is not, then the list must be unsorted, so we abort with a contract failure. Note that the output list m is the same as the input list n because every element that we examine is then passed along unchanged to m.

We can use the \(\mathtt {ascending}\) monitor to verify that the output list of a sorting procedure is in sorted order. To take the example one step further, we can verify that the elements in the output list are in fact a permutation of the elements in the input list of the sorting procedure as follows. Using a reasonable hash function, we hash each element as it is sent to the sorting procedure. Our monitor then keeps track of a running total of the sum of the hashes, and as elements are received from the sorting procedure, it computes their hash and subtracts it from the total. After all of the elements are received, we check that the total is 0 – if it is, with high probability, the two lists are permutations of each other. This example is an instance of result checking, inspired by Wasserman and Blum [26]. The monitor encoding is straightforward and omitted from the paper.

Our next example match validates whether a set of right and left parentheses match. The monitor can use its internal state to push every left parenthesis it sees on its stack and to pop it off when it sees a right parenthesis. For brevity, we model our list of parentheses by marking every left parenthesis with a 1 and right parenthesis with a -1. So the sequence ()()) would look like \(1, -1, 1, -1, -1\). As we can see, this is not a proper sequence of parenthesis because adding all of the integer representations does not yield 0. In a similar vein, we can implement a process that checks that a tree is serialized correctly, which is related to recent work on context-free session types by Thiemann and Vasconcelos [21].
Fig. 3.

Higher-order monitor

Mapper. Finally, we can also define monitors that check higher-order contracts, such as a contract for a mapping function (Fig. 3). Consider the mapper which takes an integer and doubles it, and a function \(\mathtt {map}\) that applies this mapper to a list of integers to produce a new list of integers. We can see that any integer that the mapper has produced will be strictly larger than the original integer, assuming the original integer is positive. In order to monitor this contract, it makes sense to impose a contract on the mapper itself. This \(\mathtt {mapper\_mon}\) process enforces both the precondition, that the original integer is positive, and the postcondition, that the resulting integer is greater than the original. We can now run the monitor on the mapper, in the \(\mathtt {map}\) process, before applying the mapper to the list l.

4 Monitors as Partial Identity Processes

In the literature on contracts, they are often depicted as guards on values sent to and returned from functions. In our case, they really are processes that monitor message-passing communications between processes. For us, a central property of contracts is that a program may be executed with or without contract checking and, unless an alarm is raised, the observable outcome should be the same. This means that contract monitors should be partial identity processes passing messages back and forth along channels while testing properties of the messages.

This may seem very limiting at first, but session-typed processes can maintain local state. For example, consider the functional notion of a dependent contract, where the contract on the result of a function depends on its input. Here, a function would be implemented by a process to which you send the arguments and which sends back the return value along the same channel. Therefore, a monitor can remember any (non-linear) “argument values” and use them to validate the “result value”. Similarly, when a list is sent element by element, properties that can be easily checked include constraints on its length, or whether it is in ascending order. Moreover, local state can include additional (private) concurrent processes.

This raises a second question: how can we guarantee that a monitor really is a partial identity? The criterion should be general enough to allow us to naturally express the contracts from a wide range of examples. A key constraint is that contracts are expressed as session-typed processes, just like functional contracts should be expressed within the functional language, or object contracts within the object oriented language, etc.

The purpose of this section is to present and prove the correctness of a criterion on session-typed processes that guarantees that they are observationally equivalent to partial identity processes. All the contracts in this paper can be verified to be partial identities under our definition.

4.1 Buffering Values

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.
$$ \begin{array}{l} \mathsf {factor\_t} = \forall n{:}\mathsf {int}.\, {\uparrow }\, \exists p{:}\mathsf {int}.\, \exists q{:}\mathsf {int}.\, \mathbf {1}\\ \mathsf {factor\_monitor} : \{\mathsf {factor\_t} \leftarrow \mathsf {factor\_t}\} \\ c \leftarrow \mathsf {factor\_monitor} \leftarrow d = \\ \quad n \leftarrow \mathsf {recv}\; c \mathrel {;}\mathsf {assert}\; (n> 0)^{\rho _1} \mathrel {;}\mathsf {shift} \leftarrow \mathsf {recv}\; c \mathrel {;}\mathsf {send}\; d\; n \mathrel {;}\mathsf {send}\; d\; \mathsf {shift} \mathrel {;}\\ \quad p \leftarrow \mathsf {recv}\; d \mathrel {;}\mathsf {assert} (p> 0)^{\rho _2} \mathrel {;}q \leftarrow \mathsf {recv}\; d \mathrel {;}\mathsf {assert} (q > 0)^{\rho _3} \mathrel {;}\mathsf {assert} (p \le q)^{\rho _4} \mathrel {;}\\ \quad \mathsf {assert} (n = p * q)^{\rho _5} \mathrel {;}\mathsf {send}\; c\; p \mathrel {;}\mathsf {send}\; c\; q \mathrel {;}c \leftarrow d \end{array} $$
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:
$$ \begin{array}{l} \mathsf {factor} : \{\mathsf {factor\_t}\} \\ c \leftarrow \mathsf {factor} = \\ \quad c' \leftarrow \mathsf {factor\_raw} \mathrel {;}c' \leftarrow \mathsf {factor\_monitor} \leftarrow c' \mathrel {;}c \leftarrow c' \end{array} $$
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:
$$ [q](b : B^-) \mathrel {;}\varPsi \vdash P :\,\!: (a : A^-) $$
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 with
$$ \begin{array}{l} { {mon}} : \tau _1 \rightarrow \ldots \rightarrow \tau _n \rightarrow \{A \leftarrow A\} \\ a \leftarrow { {mon}}\; x_1 \ldots x_n \leftarrow b = P \end{array} $$
where context \(\varPsi \) declares value variables x. The body P here is type-checked as one of (depending on the polarity of A)
$$ \begin{array}{l} [\; ](b : A^-) \mathrel {;}\varPsi \vdash P :\,\!: (a : A^-) \quad \text{ or }\quad (b : A^+) \mathrel {;}\varPsi \vdash P :\,\!: [\;](a : A^+) \end{array} $$
where \(\varPsi = (x_1{:}\tau _1)\cdots (x_n{:}\tau _n)\). A use such as
$$ c \leftarrow { {mon}}\; e_1 \ldots e_n \leftarrow c $$
is transformed into
$$ \begin{array}{l} c' \leftarrow { {mon}}\; e_1 \ldots e_n \leftarrow c \mathrel {;}c \leftarrow c' \end{array} $$
for 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 \), Open image in new window , Open image in new window ) 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).
$$ (b : B^+) \mathrel {;}\varPsi \vdash Q :\,\!: [q](a : A^+) $$
Moreover, when \(\mathsf {end}\) has been received along b the corresponding process has terminated and the channel is closed, so we generalize the judgment to
$$ \omega \mathrel {;}\varPsi \vdash Q :\,\!: [q](a : A^+) \qquad \text{ with }~ \omega = \cdot \mid (b : B). $$
The 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.
$$ \begin{array}{l} [q](b:B^-) \mathrel {;}\varPsi \vdash P :\,\!: (a : A) \\ \omega \mathrel {;}\varPsi \vdash Q :\,\!: [q](a : A^+) \quad \text{ where } \omega = \cdot \mid (b : B) \end{array} $$
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.

4.2 Rule Summary

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 are
$$ \begin{array}{l} [q](b:B^-) \mathrel {;}\varPsi \mathrel {;}\varGamma \mathrel {;}\varDelta \vdash P :\,\!: (a : A)\\ \omega \mathrel {;}\varPsi \mathrel {;}\varGamma \mathrel {;}\varDelta \vdash Q :\,\!: [q](a : A^+) \quad \text{ where } \omega = \cdot \mid (b : B) \end{array} $$
So far, it is given by the following rules

4.3 Spawning New Processes

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 Open image in new window 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.

4.4 Transparency

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 judgment
$$ \varDelta \vdash \mathcal {C}:\,\!: \varDelta ' $$
which 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
  1. 1.

    If \(\varGamma ' \vdash \mathsf {msg}^+(c, P) :\,\!: \varGamma \) then \(\varGamma ' \vdash (\mathsf {msg}^+(c, P), \mathcal {C}) \sim (\mathsf {msg}^+(c, P), \mathcal {D}) :\,\!: \varDelta \).

     
  2. 2.

    If \(\varDelta \vdash \mathsf {msg}^-(c, P) :\,\!: \varDelta '\) then \(\varGamma \vdash (\mathcal {C}, \mathsf {msg}^-(c,P)) \sim (\mathcal {D}, \mathsf {msg}^-(c,P)) :\,\!: \varDelta '\).

     
  3. 3.

    If \(\mathcal {C}= (\mathcal {C}', \mathsf {msg}^+(c,P))\) with \(\varGamma \vdash \mathcal {C}' :\,\!: \varDelta _1'\) and \(\varDelta _1' \vdash \mathsf {msg}^+(c,P) :\,\!: \varDelta \)

    and \(\mathcal {D}= (\mathcal {D}', \mathsf {msg}^+(c,Q))\) with \(\varGamma \vdash \mathcal {D}' :\,\!: \varDelta _2'\) and \(\varDelta _2' \vdash \mathsf {msg}^+(c,Q) :\,\!: \varDelta \)

    then \(\varDelta _1' = \varDelta _2' = \varDelta '\) and \(P = Q\) and \(\varGamma \vdash \mathcal {C}' \sim \mathcal {D}' :\,\!: \varDelta '\).

     
  4. 4.

    If \(\mathcal {C}= (\mathsf {msg}^-(c,P), \mathcal {C}')\) with \(\varGamma \vdash \mathsf {msg}^-(c,P) :\,\!: \varGamma _1'\) and \(\varGamma _1' \vdash \mathcal {C}' :\,\!: \varDelta \)

    and \(\mathcal {D}= (\mathsf {msg}^-(c,Q), \mathcal {D}')\) with \(\varGamma \vdash \mathsf {msg}^-(c,Q):\,\!: \varGamma _2'\) and \(\varGamma _2' \vdash \mathcal {D}' :\,\!: \varDelta \)

    then \(\varGamma _1' = \varGamma _2' = \varGamma '\) and \(P = Q\) and \(\varGamma ' \vdash \mathcal {C}' \sim \mathcal {D}' :\,\!: \varDelta \).

     
  5. 5.

    If \(\mathcal {C}\longrightarrow \mathcal {C}'\) then \(\varGamma \vdash \mathcal {C}' \sim \mathcal {D}:\,\!: \varDelta \).

     
  6. 6.

    If \(\mathcal {D}\longrightarrow \mathcal {D}'\) then \(\varGamma \vdash \mathcal {C}\sim \mathcal {D}' :\,\!: \varDelta \).

     

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  Open image in new window  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  
(\(1^+\))

If \((y:A^+) \mathrel {;}\cdot \mathrel {;}\cdot \vdash P :\,\!: (x:A^+)[\;]\)

then \(y : A^+ \vdash \mathsf {proc}(x, x \leftarrow y) \sim _M P :\,\!: (x : A^+)\)

(\(1^-\))

If \([\;](y:A^-) \mathrel {;}\cdot \mathrel {;}\cdot \vdash P :\,\!: (x:A^-)\)

then \(y:A^- \vdash \mathsf {proc}(x, x\leftarrow y) \sim _M P :\,\!: (x : A^-)\)

  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.  
(\(2^+\))

If \((y {:} B^+) \mathrel {;}\cdot \mathrel {;}\cdot \mathrel {;}\cdot \vdash P :\,\!: (x {:} A^+)[\langle \!\langle \mathcal {E}\rangle \!\rangle ]\) then \(y:B^+ \vdash \mathcal {E}\sim _M \mathsf {proc}(x,P) :\,\!: (x : A^+)\).

(\(2^-\))

If \([\langle \!\langle \mathcal {E}\rangle \!\rangle ](y{:}B^-) \cdot \mathrel {;}\cdot \mathrel {;}\cdot \vdash P :\,\!: (x{:}A^-)\) then \(y{:}B^- \vdash \mathcal {E}\sim _M \mathsf {proc}(x,P) :\,\!: (x{ :} A^-)\).

 
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.  
(\(3^+\))

If \(\omega \mathrel {;}\cdot \mathrel {;}\cdot \mathrel {;}\cdot \vdash P :\,\!: (x {:} A^+)[\langle \!\langle \mathcal {E}\rangle \!\rangle ]\) then \(\omega \vdash \mathcal {E}\sim _M \mathsf {proc}(x,P) :\,\!: (x {:} A^+)\).

(\(3^-\))

If \([\langle \!\langle \mathcal {E}\rangle \!\rangle ](y{:}B^-) \mathrel {;}\cdot \mathrel {;}\cdot \mathrel {;}\cdot \vdash P :\,\!: (x{:}A)\) then \(y{:}B^- \vdash \mathcal {E}\sim _M \mathsf {proc}(x,P) :\,\!: (x {:}x A)\).

  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.  
(\(4^+\))

If \(\omega \mathrel {;}\cdot \mathrel {;}\cdot \mathrel {;}\varDelta \vdash P :\,\!: [\langle \!\langle \mathcal {E}\rangle \!\rangle ](x : A^+)\) and \(\cdot \vdash \mathcal {D}:\,\!: \varDelta \) then \(\omega \vdash \mathcal {E}\sim _M \mathcal {D}, \mathsf {proc}(x,P) :\,\!: [q](x : A^+)\).

(\(4^-\))

If \([\langle \!\langle \mathcal {E}\rangle \!\rangle ](y:B^-) \mathrel {;}\cdot \mathrel {;}\cdot \mathrel {;}\varDelta \vdash P :\,\!: (x:A)\) and \(\cdot \vdash \mathcal {D}:\,\!: \varDelta \) then \(\varGamma , y:B^- \vdash \mathcal {E}\sim _M \mathcal {D}, \mathsf {proc}(x,P) :\,\!: (x : A)\).

  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.  
(\(5^+\))

If \(\omega \mathrel {;}\varPsi \mathrel {;}\cdot \mathrel {;}\varDelta \vdash P :\,\!: [q](x : A^+)\) and \(\sigma : \varPsi \) and \(q[\sigma ] = \langle \!\langle \mathcal {E}\rangle \!\rangle \) and \(\cdot \vdash \mathcal {D}:\,\!: \varDelta [\sigma ]\) then \(\omega [\sigma ] \vdash \mathcal {E}\sim _M \mathcal {D}, \mathsf {proc}(x,P[\sigma ]) :\,\!: (x : A^+[\sigma ])\).

(\(5^-\))

If \([q](y:B^-) \mathrel {;}\varPsi \mathrel {;}\cdot \mathrel {;}\varDelta \vdash P :\,\!: (x:A)\) and \(\sigma : \varPsi \) and \(q[\sigma ] = \mathcal {E}\) and \(\cdot \vdash \mathcal {D}:\,\!: \varDelta [\sigma ]\) then \(y:B^-[\sigma ] \vdash \mathcal {E}\sim _M \mathcal {D}, \mathsf {proc}(x,P[\sigma ]) :\,\!: (x : A[\sigma ])\).

  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.  
(6)

If \(\omega \vdash \mathcal {E}_1 \sim _M \mathcal {D}_1 :\,\!: (z : C)\) and \((z : C) \vdash \mathcal {E}_2 \sim _M \mathcal {D}_2 :\,\!: (x : A)\) then \(\omega \vdash (\mathcal {E}_1,\mathcal {E}_2) \sim _M (\mathcal {D}_1,\mathcal {D}_2) :\,\!: (x : A)\).

 
At this point, the only types that have not yet accounted for are \(\otimes \) and Open image in new window . 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.  
(\(7^+\))

If \(\omega \mathrel {;}\varPsi \mathrel {;}\varGamma \mathrel {;}\varDelta \vdash P :\,\!: [q](x : A^+)\) and \(\sigma : \varPsi \) and \(q[\sigma ] = \langle \!\langle \mathcal {E}\rangle \!\rangle \) and \(\cdot \vdash \mathcal {D}:\,\!: \varDelta [\sigma ]\) then \(\varGamma [\sigma ], \omega [\sigma ] \vdash \mathcal {E}\sim _M \mathcal {D}, \mathsf {proc}(x,P[\sigma ]) :\,\!: (x : A^+[\sigma ])\).

(\(7^-\))

If \([q](y:B^-) \mathrel {;}\varPsi \mathrel {;}\varGamma \mathrel {;}\varDelta \vdash P :\,\!: (x:A)\) and \(\sigma : \varPsi \) and \(q[\sigma ] = \mathcal {E}\) and \(\cdot \vdash \mathcal {D}:\,\!: \varDelta [\sigma ]\) then \(\varGamma [\sigma ], y:B^-[\sigma ] \vdash \mathcal {E}\sim _M \mathcal {D}, \mathsf {proc}(x,P[\sigma ]) :\,\!: (x : A[\sigma ])\).

  In addition we need to generalize property (6) into (8) and (9) to allow multiple monitors to run concurrently in a configuration.  
(8)

If \(\varGamma \vdash \mathcal {E}\sim _M \mathcal {D}:\,\!: \varDelta \) then \((\varGamma ', \varGamma ) \vdash \mathcal {E}\sim _M \mathcal {D}:\,\!: (\varGamma ', \varDelta )\).

(9)

If \(\varGamma _1 \vdash \mathcal {E}_1 \sim _M \mathcal {D}_1 :\,\!: \varGamma _2\) and \(\varGamma _2 \vdash \mathcal {E}_2 \sim _M \mathcal {D}_2 :\,\!: \varGamma _3\) then \(\varGamma _1 \vdash (\mathcal {E}_1,\mathcal {E}_2) \sim _M (\mathcal {D}_1,\mathcal {D}_2) :\,\!: \varGamma _3\).

 

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

Theorem 1

If \(\varGamma \vdash \mathcal {E}\sim _M \mathcal {D}:\,\!: \varDelta \) according to properties \((7^+), (7^-), (8), and (9)\) then \(\varGamma \vdash \mathcal {E}\sim \mathcal {D}:\,\!: \varDelta \).

Proof

By closure under conditions 1–6 in the definition of \(\sim \).

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

Corollary 1

If \([\; ](b : A^-) \mathrel {;}\varPsi \vdash P :\,\!: (a : A^-)\) or \((b : A^+) \mathrel {;}\varPsi \vdash P :\,\!: [\;](a : A^+)\) then P is a partial identity process.

5 Refinements as Contracts

In this section we show how to check refinement types dynamically using our contracts. We encode refinements as type casts, which allows processes to remain well-typed with respect to the non-refinement type system (Sect. 2). These casts are translated at run time to monitors that validate whether the cast expresses an appropriate refinement. If so, the monitors behave as identity processes; otherwise, they raise an alarm and abort. For refinement contracts, we can prove a safety theorem, analogous to the classic “Well-typed Programs Can’t be Blamed” [25], stating that if a monitor enforces a contract that casts from type A to type B, where A is a subtype of B, then this monitor will never raise an alarm.

5.1 Syntax and Typing Rules

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.
$$ \begin{array}{lcl} P&:\,\!:=&\cdots \mid x \leftarrow \langle \tau \Leftarrow \tau ' \rangle ^{\rho }\ v \mathrel {;}Q \mid a{:}A \leftarrow \langle A \Leftarrow B \rangle ^{\rho }\ b \end{array} $$
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).

5.2 Translation to Monitors

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.
Fig. 4.

Cast translation

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 Open image in new window 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\).

5.3 Metatheory

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.
Fig. 5.

Subtyping

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.
Fig. 6.

Typing process expressions

Theorem 2

(Monitors are well-typed). Let \(\varPsi \) be the context containing the type bindings of all recursive processes.

  1. 1.

    \(\varPsi \mathrel {;}b:B \vdash _T [\![\langle A \Leftarrow B \rangle ^{\rho }]\!]_{a,b}^\varPsi \) : : (a : A).

     
  2. 2.

    If \(B \le A\), then \( \varPsi \mathrel {;}b:B \vdash _S [\![\langle A \Leftarrow B \rangle ^{\rho }]\!]_{a,b}^\varPsi :\,\!: (a : A)\).

     

Proof

The proof is by induction over the monitor translation rules. For 2, we need to use the sub-typing relation to show that (1) for the internal and external choice cases, no branches that include \(\mathsf {abort}\) are generated; and (2) for the forall and exists cases, the assert never fails (i.e., the \(\mathsf {assert\_strong}\) rule applies).    \(\square \)

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.

Corollary 2

(Well-typed casts cannot raise alarms). \(\vdash \mathcal {C}:\,\!: b:B\) and \(B \le A\) implies Open image in new window .

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

Theorem 3

(Casts are transparent).  

\(b:B \vdash \mathsf {proc}(b, a\leftarrow b)\sim \mathsf {proc}(a, [\![\langle A \Leftarrow B \rangle ^{\rho }]\!]_{a,b}) :\,\!: (a: A)\).

Proof

We just need to show that the translated process passes the partial identity checks. We can show this by induction over the translation rules and by applying the rules in Sect. 4. We note that rules in Sect. 4 only consider identical types; however, our casts only cast between two compatible types. Therefore, we can lift A and B to their super types (i.e., insert abort cases for mismatched labels), and then apply the checking rules. This does not change the semantics of the monitors.

6 Related Work

There is a rich body of work on higher-order contracts and the correctness of blame assignments in the context of the lambda calculus [2, 7, 8, 10, 16, 24, 25]. The contracts in these papers are mostly based on refinement or dependent types. Our contracts are more expressive than the above, and can encode refinement-based contracts. While our monitors are similar to reference monitors (such as those described by Schneider [19]), they have a few features that are not inherent to reference monitors such as the fact that our monitors are written in the target language. Our monitors are also able to monitor contracts in a higher-order setting by spawning a separate monitor for the sent/received channel.

Disney et al.’s [9] work, which investigates behavioral contracts that enforce temporal properties for modules, is closely related to our work. Our contracts (i.e., session types) also enforce temporal properties; the session types specify the order in which messages are sent and received by the processes. Our contracts can also make use of internal state, as those of Disney et al, but our system is concurrent, while their system does not consider concurrency.

Recently, gradual typing for two-party session-type systems has been developed [14, 20]. Even though this formalism is different from our contracts, the way untyped processes are gradually typed at run time resembles how we monitor type casts. Because of dynamic session types, their system has to keep track of the linear use of channels, which is not needed for our monitors.

Most recently, Melgratti and Padovani have developed chaperone contracts for higher-order session types [17]. Their work is based on a classic interpretation of session types, instead of an intuitionistic one like ours, which means that they do not handle spawning or forwarding processes. While their contracts also inspect messages passed between processes, unlike ours, they cannot model contracts which rely on the monitor making use of internal state (e.g., the parenthesis matching). They proved a blame theorem relying on the notion of locally correct modules, which is a semantic categorization of whether a module satisfies the contract. We did not prove a general blame theorem; instead, we prove a somewhat standard safety theorem for cast-based contracts.

The Whip system [27] addresses a similar problem as our prior work [15], but does not use session types. They use a dependent type system to implement a contract monitoring system that can connect services written in different languages. Their system is also higher order, and allows processes that are monitored by Whip to interact with unmonitored processes. While Whip can express dependent contacts, Whip cannot handle stateful contracts. Another distinguishing feature of our monitors is that they are partial identity processes encoded in the same language as the processes to be monitored.

7 Conclusion

We have presented a novel approach for contract-checking for concurrent processes. Our model uses partial identity monitors which are written in the same language as the original processes and execute transparently. We define what it means to be a partial identity monitor and prove our characterization correct. We provide multiple examples of contracts we can monitor including ones that make use of the monitor’s internal state, ones that make use of the idea of probabilistic result checking, and ones that cannot be expressed as dependent or refinement types. We translate contracts in the refinement fragment into monitors, and prove a safety theorem for that fragment.

Notes

Acknowledgment

This research was supported in part by NSF grant CNS1423168 and a Carnegie Mellon University Presidential Fellowship.

References

  1. 1.
    Acay, C., Pfenning, F.: Intersections and unions of session types. In: Proceedings Eighth Workshop on Intersection Types and Related Systems, ITRS 2016, Porto, Portugal, pp. 4–19, 26 June 2016. https://dx.doi.org/10.4204/EPTCS.242.3MathSciNetCrossRefGoogle Scholar
  2. 2.
    Ahmed, A., Findler, R.B., Siek, J.G., Wadler, P.: Blame for all. In: 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011) (2011). https://doi.acm.org/10.1145/1570506.1570507
  3. 3.
    Balzer, S., Pfenning, F.: Manifest sharing with session types. Proc. ACM Program. Lang. 1(ICFP), 37:1–37:29 (2017).  https://doi.org/10.1145/3110281CrossRefGoogle Scholar
  4. 4.
    Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_16CrossRefGoogle Scholar
  5. 5.
    Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(3), 367–423 (2016)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Cervesato, I., Scedrov, A.: Relating state-based and process-based concurrency through linear logic. Inf. Comput. 207(10), 1044–1077 (2009).  https://doi.org/10.1016/j.ic.2008.11.006CrossRefMATHGoogle Scholar
  7. 7.
    Dimoulas, C., Findler, R.B., Flanagan, C., Felleisen, M.: Correct blame for contracts: no more scapegoating. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 215–226. ACM, New York (2011). https://doi.acm.org/10.1145/1926385.1926410
  8. 8.
    Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Complete monitors for behavioral contracts. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 214–233. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28869-2_11CrossRefGoogle Scholar
  9. 9.
    Disney, T., Flanagan, C., McCarthy, J.: Temporal higher-order contracts. In: 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) (2011). https://doi.acm.org/10.1145/2034773.2034800
  10. 10.
    Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP 2002, pp. 48–59. ACM, New York (2002). https://doi.acm.org/10.1145/581478.581484
  11. 11.
    Gay, S.J., Hole, M.: Subtyping for session types in the \(\pi \)-calculus. Acta Informatica 42(2–3), 191–225 (2005).  https://doi.org/10.1007/s00236-005-0177-zMathSciNetCrossRefMATHGoogle Scholar
  12. 12.
    Gommerstadt, H., Jia, L., Pfenning, F.: Session-typed concurrent contracts. Technical report CMU-CyLab-17-004, CyLab, Carnegie Mellon University, February 2018Google Scholar
  13. 13.
    Griffith, D.: Polarized Substructural Session Types. Ph.D. thesis, University of Illinois at Urbana-Champaign, April 2016Google Scholar
  14. 14.
    Igarashi, A., Thiemann, P., Vasconcelos, V.T., Wadler, P.: Gradual session types. Proc. ACM Program. Lang. 1(ICFP), 38:1–38:28 (2017).  https://doi.org/10.1145/3110282CrossRefGoogle Scholar
  15. 15.
    Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 582–594. ACM, New York (2016). https://doi.acm.org/10.1145/2837614.2837662
  16. 16.
    Keil, M., Thiemann, P.: Blame assignment for higher-order contracts with intersection and union. In: 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015) (2015). https://doi.acm.org/10.1145/2784731.2784737
  17. 17.
    Melgratti, H., Padovani, L.: Chaperone contracts for higher-order sessions. Proc. ACM Program. Lang. 1(ICFP), 35:1–35:29 (2017).  https://doi.org/10.1145/3110279CrossRefGoogle Scholar
  18. 18.
    Pfenning, F., Griffith, D.: Polarized substructural session types. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 3–22. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46678-0_1CrossRefGoogle Scholar
  19. 19.
    Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000).  https://doi.org/10.1145/353323.353382CrossRefGoogle Scholar
  20. 20.
    Thiemann, P.: Session types with gradual typing. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 144–158. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45917-1_10CrossRefGoogle Scholar
  21. 21.
    Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pp. 462–475. ACM, New York (2016). https://acm.doi.org/10.4230/LIPIcs.ECOOP.2016.9
  22. 22.
    Toninho, B.: A Logical Foundation for Session-based Concurrent Computation. Ph.D. thesis, Carnegie Mellon University and New University of Lisbon (2015)Google Scholar
  23. 23.
    Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 350–369. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_20CrossRefMATHGoogle Scholar
  24. 24.
    Wadler, P.: A complement to blame. In: 1st Summit on Advances in Programming Languages (SNAPL 2015) (2015). https://doi.acm.org/10.4230/LIPIcs.SNAPL.2015.309
  25. 25.
    Wadler, P., Findler, R.B.: Well-typed programs can’t be blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1–16. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00590-9_1CrossRefGoogle Scholar
  26. 26.
    Wasserman, H., Blum, M.: Software reliability via run-time result-checking. J. ACM 44(6), 826–849 (1997).  https://doi.org/10.1145/268999.269003MathSciNetCrossRefMATHGoogle Scholar
  27. 27.
    Waye, L., Chong, S., Dimoulas, C.: Whip: higher-order contracts for modern services. Proc. ACM Program. Lang. 1(ICFP), 36:1–36:28 (2017).  https://doi.org/10.1145/3110280CrossRefGoogle Scholar

Copyright information

© The Author(s) 2018

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Carnegie Mellon UniversityPittsburghUSA

Personalised recommendations