First-Order Store and Visibility in Name-Passing Calculi

The $\pi$-calculus is one of the best known process calculi. It has a handful of operators  – parallelism, input, output, restriction being the main ones  – with which it achieves an amazing expressive power. Yet, it has a rich algebraic theory and a wide spectrum of proof techniques. In the $\pi$-calculus, computation is communication, by means of message-passing synchronisations between processes. Names are the communication units; new names may be created, and may themselves be exchanged in communications. When used for modelling, $\pi$-calculus is normally typed, so to be able to support structured data values, beginning with basic first-order values such as integers and booleans.

The $\pi$-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. For instance, the representation of functions as $\pi$-calculus processes has been widely studied, beginning with Milner’s seminal work [16]. Usually, higher-order languages include forms of store. It is therefore important to understand how expected semantic properties of store can be captured in a language for pure concurrency such as the $\pi$-calculus.

An aspect of store with strong semantic consequences is the distinction between higher-order and first-order store. The term “first-order store” refers to a memory model where variables can hold only basic data types such as integers and booleans. This contrasts with a higher-order store, where variables can also store functions, or code, or references to these. Limiting the store to first-order data makes it easier to reason about program behaviours, and verify behavioural properties. It may also enhance security and predictability guarantees by preventing unintended behaviours associated with dynamic function storage and code injection. A striking example of a property that may be broken with higher-order store is termination. For instance, the simply-typed $\lambda$-calculus is strongly normalising and therefore terminating. This property is maintained by the addition of first-order store, but not with higher-order store, as functions may recursively reference and invoke each other through the store. In game semantics of higher-order languages, the distinction between first-order and higher-order store has led to studying the concept of visibility. Intuitively, visibility ensures us that each move in a computational game is justified by prior interactions. With the introduction of higher-order store, the visibility condition has to be relaxed, reflecting the added complexity in tracking information flow within a program.

The goal of this paper is precisely to understand the meaning of first-order store and visibility within the $\pi$-calculus. In functional languages based on the $\lambda$-calculus, imposing first-order store is simply determined by the constraint that all references may only store first-order values. In the $\pi$-calculus, in contrast, there is no explicit notion of reference, and therefore the meaning of “first-order store” requires some care. In $\pi$-calculi, a piece of store is usually represented by an output message. For instance $\overline{h}⟨5⟩$ may be thought of as the statement that name $h$ currently contains $5$. A process that inputs at $h$ and then re-emits a message at $h$, such as $h(z).\overline{h}⟨z+1⟩$, is a process that acts on such a store. In this case, $h$ is a first-order name, hence $h$ implements a piece of first-order store. An example of higher-order store is given by the process

Here, $\overline{b}(d)$ is a bound output, and represents the output of a “new” name $d$, and similarly for $\overline{b}(d^{\prime })$; whereas, e.g., $d.R$ and $c.Q$ (where $Q$ is $\overline{b}(d^{\prime }).d^{\prime }.R^{\prime }$) represent inputs in which no value is exchanged (i.e., $d$ and $c$ carry unit values). In $P$, name $a$ is higher-order, in that $a$ carries a (pointer to a) service. In the input at $a$, the service name received in the input (the parameter $b$) is used after the input, but it is also stored, and used later when $c$ is invoked. In other words, the visibility of $c$ (the services that $c$ may call when invoked) depends on interactions that have occurred earlier, at $a$. For this reason, $P$ implements a form of higher-order store. When this does not happen, that is, the visibility of a higher-order name (the set of services that may be called when the name is invoked) may be determined at the point in which the name is created, the process implements a form of first-order store. (The word “service” is freely used, here and elsewhere, to indicate the input end of a name; in $\pi$-calculus, a name may have multiple input occurrences, in arbitrary syntactic positions within a process, in contrast with, say, the function declarations in functional languages, which are supposed to be unique.)

The amazing expressive power of the $\pi$-calculus also makes the contexts of the calculus very discriminating; as a consequence, behavioural equivalences, which are supposed to be preserved by the contexts of the calculus, are rather demanding relations. A well-established way of imposing constraints on the set of legal contexts, thus obtaining usefully coarser behavioural equivalences, is to adopt behavioural type systems. Types may be used in order to capture communication patterns on the usage of names, such as capabilities, linearity, sessions, and so on, e.g., [19, 11, 6, 1]. Type systems have also been designed to capture specific properties of processes, such as termination, deadlock-freedom, lock-freedom, e.g., [24, 12, 18].

A further step is then to tune the proof techniques of the $\pi$-calculus to such type systems, so to be able to actually prove the behavioural equalities that only hold in presence of types. For instance, in the case of may testing (or contextual equivalence) this may yield to refinements or modifications of the notion of trace equivalence; whereas in the case of barbed equivalence this may lead to refinements or modifications of the standard notion of labelled bisimilarity. The resulting proof techniques must be sound with respect to initial contextually-defined relations; ideally, they should also be complete.

In this paper we propose a type system that guarantees first-order store in $\pi$-calculus processes. The type system makes use of visibility functions, that is, partial finite functions that specify, for each higher-order name $b$ that may occur free in a process, the set of services (i.e., higher-order names) that may be invoked when a call at $b$ is made. In order to better understand the behavioural effects of visibility, we combine it first with sequentiality and then with well-bracketing. “Sequentiality” intuitively indicates the existence of a single thread of computation. That is, at any point there is a single process that is active and decides what the next computation step can be. In the encodings of the $\lambda$-calculus  [16, 21], a process is active, i.e., it carries the thread, when it contains an unguarded output at a higher-order name. When encoding $\lambda$-calculi with first-order references, an active process may also expose the thread by exhibiting an input at a first-order name. We follow such a convention also in the paper: higher-order names carry the thread via outputs, first-order names via inputs (other choices technically would however be possible). Sequentiality allows us to expose, in isolation, the causality properties of service calls, within a standard (interleaving) semantics. These aspects would be partially or totally obscured by the presence of other concurrent threads.

In higher-order languages, the effects of having first-order store are particularly strong in absence of control operators; that is, using a terminology borrowed from game semantics, in a “well-bracketed” setting, where the call-return interaction behaviour between a term and its context follows a stack discipline. We therefore also consider the refinement of our visibility-based type system under the well-bracketing hypothesis. To see an example of the effect of visibility, consider the following well-bracketed example:

Here, an external service $a$ is called, exporting a local service $c$ capable of incrementing a private reference $h$, and with a return channel $q$. If visibility holds, then the external environment cannot store $c$. Therefore, after providing an answer at $q$ , the environment is unable to call $c$ again, thus incrementing $h$, unless an access to $c$ is explicitly provided again (by process $Q$). This property may be used to perform optimisations, possibly including garbage-collection of the service $c$ if at some point $c$ is not used anymore in $Q$.

We then study characterisations for both may testing and barbed equivalence, as special forms of trace equivalence and of labelled bisimilarity. Following the tradition of testing, the language includes special success signals, that are used by testers (i.e, processes running in parallel with the testees), and may be used at any time, to report success.

When developing such characterisations, some care is necessary so to distinguish between the visibility of the tested and of the tester processes, as they need not be the same. For this, we introduce visibility-constrained LTSs, in which process transitions are constrained by a visibility function, intuitively expressing the possibility for processes to perform a certain transition given a certain visibility function for the external observer. As a consequence of the transition, the visibility function may need to be updated, so to yield the visibility function for the next transition. In the case of well-bracketing, the constraints given by visibility have to be coupled with those given by the stack names used to track well-bracketing (and again, a distinction has to be made between the stacks for the testers and those for the testees). Based on these LTSs, we introduce forms of trace equivalence and of labelled bisimilarity that are proved to be sound and complete, for may testing and barbed equivalence, both in the case of sequentiality and in that of well-bracketing.

We present the version of the $\pi$-calculus with higher-order and first-order names in Section 2. In Section 3, we define the type system implementing visibility for sequential processes. We define typed labelled transitions and present labelled characterisations of behavioural equivalences in Section 4. Section 5 is devoted to the extension with well-bracketing. For lack of space, the results about labelled bisimilarities are presented in [4].

The $\pi$-calculus language that will be used is called, technically, Internal $\pi$ ($\pi$I) [22] (all channels exchanged are fresh – no free object outputs), with the addition of first-order values (such as integers and booleans), and expressions that evaluate to first-order values, called first-order expressions. We do not specify what exactly first-order values and first-order expressions are. We simply assume that, in a closed process, a first-order expression evaluates to a first-order value. Moreover, only the output capability of names may be exported. This means that, for instance, in an input $a(b).P$ name $b$ may only be used in output in $P$. This constraint is often followed in theory and applications of the $\pi$-calculus, as it simplifies various technical matters.

We assume that names are distinguished (partitioned) into higher-order names and first-order names, and success names. Higher-order names are the ordinary $\pi$I names; first-order names may only carry first-order values, and they may not be passed around (the second constraint simplifies the technical details, though it is not mandatory, see Section 3). In later sections, first-order names will be used to represent references. The fact that these names may only carry first-order values, together with constraints on visibility, will ensure that the calculus does not have (implicit or explicit forms of) higher-order store. The success names are used, in the tradition of testing equivalences, by tester processes so to report results of experiments on tested processes (thus, the processes compared in the examples of the paper do not contain success names).

The calculi in the paper will be typed. For simplicity we define our type systems as refinements of the most basic type system for $\pi$-calculus, namely Milner’s sorting [15], in which names are partitioned into a collection of types (or sorts), and a sorting function maps types onto types. We assume that there is a sorting system under which all processes we manipulate are well-typed. Thus, the sorting system separates higher-order and first-order names; moreover we assume that first-order names are monadic, and that higher-order names carry a pair of a first-order value and a higher-order name. Thus $\overline{a}⟨v⟩(b).P$ is the output of the first-order value $v$ and of the fresh higher-order name $b$ at the (higher-order) name $a$, with continuation $P$. When writing examples, we allow different sortings; for instance, writing $a.P$ and $\overline{b}.Q$ for inputs and outputs in which no value is exchanged.

The syntactic categories of the calculus are presented in Table 1. As usual, input and restriction are binding constructs, and give rise to the expected definitions of free and bound names. An expression or a process is closed if it does not have free (first-order) variables. It is intended that transitions are defined on closed processes.

The definition of structural congruence, written $\equiv$, and of the strong and weak (untyped) labelled transitions, written $\stackrel{\mu }{⟶}$, $⟹$, and $\stackrel{\widehat{\mu }}{⟹}$, are standard and are given in Appendix A (later we will introduce typed variants of the LTS). We note $\mathrm{𝚏𝚗}(P)$ (resp. $\mathrm{𝚏𝚗}(\mu )$) the set of free names of $P$ (resp. $\mu$). We sometimes abbreviate reductions $P\stackrel{\tau }{⟶}{P}^{\prime }$ as $P⟶P^{\prime }$.

As behavioural equivalences we consider both may-testing and barbed equivalence. Both relations are contextual, in that they are defined by requiring a closure under all “observers”. They both use “barbs” (or “success”) signals; barbed equivalence, in addition, makes use of a bisimulation game on reductions. We write ${\Downarrow }_{\omega }$ to indicate the possibility of exhibiting an $\omega$ barb, possibly after some reductions; i.e., $P{\Downarrow }_{\omega }$ holds if there is $P^{\prime }$ with $P⟹P^{\prime }$ and $P^{\prime }$ has an unguarded occurrence of $\omega$. Thus intuitively two processes are behaviourally equal if they can produce “the same barbs” under all legal observers running in parallel with them. As we are in a typed setting, observer and tested processes should have compatible typings. The meaning of “compatible” depends on the specific type system. For visibility, the meaning will be specified in Sections 3 and 5. We write $\mathrm{\Delta }⊢P$, and say that $P$ is a $\mathrm{\Delta }$-process, if $P$ is typable under $\mathrm{\Delta }$, and $\mathrm{\Delta }⊢P,Q$ if both $\mathrm{\Delta }⊢P$ and $\mathrm{\Delta }⊢Q$ hold. Behavioural equivalences are defined on closed processes; they are extended to open processes (i.e., processes with free first-order variables) in the usual manner, by considering all possible closing substitutions. We only consider weak behavioural equivalences (i.e., equivalences that abstract from internal moves of processes, the reductions), as these are, in practice, the most useful ones.

We write $P\cong Q$ (resp. $P\approxeq Q$) when $P{\cong }_{\mathrm{\Delta }}^{\mathrm{\Gamma }}Q$ (resp. $P{\approxeq }_{\mathrm{\Delta }}^{\mathrm{\Gamma }}Q$) holds under any typing $\mathrm{\Delta }$ for $P,Q$ and any $\mathrm{\Gamma }$ compatible with $\mathrm{\Delta }$.

We now introduce some notations that will be useful below. In the paper we use partial functions whose codomains are finite powersets. If $\mathrm{\Delta }$ is such a function, then $\mathrm{\Delta };i\mapsto A$ is the extension of $\mathrm{\Delta }$ in which $i$ is mapped onto $A$, assuming that $i$ is not in $\mathrm{𝚍𝚘𝚖}(\mathrm{\Delta })\cup \mathrm{𝚌𝚘𝚍𝚘𝚖}(\mathrm{\Delta })$ ; conversely ${\mathrm{\Delta }}^{-i}$ is the restriction of $\mathrm{\Delta }$ in which the entry for $i$ is erased, both in the domain and codomain of $\mathrm{\Delta }$. We also write $i\mapsto A,j$ as an abbreviation for $i\mapsto (A\cup \{j\})$; and $\mathrm{\Delta }\downharpoonleft i$ (resp. $\mathrm{\Delta }\cancel{}\downharpoonleft i$) means that $\mathrm{\Delta }$ is (resp. is not) defined on $i$. Function ${\mathrm{\Delta }}_1\cap {\mathrm{\Delta }}_2$ has domain $\mathrm{𝚍𝚘𝚖}({\mathrm{\Delta }}_1)\cap \mathrm{𝚍𝚘𝚖}({\mathrm{\Delta }}_2)$, and then is defined as $({\mathrm{\Delta }}_1\cap {\mathrm{\Delta }}_2)(p)={\mathrm{\Delta }}_1(p)\cap {\mathrm{\Delta }}_2(p)$; and likewise for ${\mathrm{\Delta }}_1\cup {\mathrm{\Delta }}_2$. We write ${\mathrm{\Delta }}_1\subseteq {\mathrm{\Delta }}_2$ if $\mathrm{𝚍𝚘𝚖}({\mathrm{\Delta }}_1)\subseteq \mathrm{𝚍𝚘𝚖}({\mathrm{\Delta }}_2)$, and for each $i\in \mathrm{𝚍𝚘𝚖}({\mathrm{\Delta }}_1)$, we have ${\mathrm{\Delta }}_1(i)\subseteq {\mathrm{\Delta }}_1(i)$.

Our type system for visibility is built on top of that for sequentiality [3]. While visibility could be defined as a standalone notion, the combination with sequentiality makes the behavioural effects sharper and easier to grasp.

Intuitively, sequentiality ensures us that at any time at most one interaction can occur; i.e., there is a single computation thread. A process that holds the thread, called active, decides what the next interaction can be. It does so by offering a single particle (input or output) that controls the thread. A given name may exercise the control on the thread either in output or in input. Following [3], we require that, in higher-order names, the thread is carried by outputs, whereas, in first-order names, it is carried by inputs. An input that carries the thread maintains the thread, whereas an output releases it. (These appear to be, practically, the most interesting combinations; other combinations could be adopted, with the expected modifications.) Thus, for instance, the following process $P$ is well-typed:

The initial particles in $P$ are the input at $h$ and the output at $k$; however only the input at $h$ carries the thread, as $h$ and $k$ are first-order. Underneath the input, the thread is maintained and released in the output at $a$ (the thread will be acquired by the process in the external environment performing the input at $a$); later, when the input at $b$ is performed, process $Q$ obtains the thread back. Sequentiality however does not exclude non-determinism: e.g., an output particle may have the possibility of interacting with different inputs.

The type system for visibility intuitively allows us to specify which possible higher-order outputs can be performed by a process that becomes active. Type environments are partial functions, called visibility functions, acting on higher-order names and, for active processes, on the special token $\ast$, representing the active thread. (Later, when studying well-bracketing, type environments will have both a visibility function and a name stack.)

To see the use of $\ast$, suppose $\mathrm{\Delta }(\ast )=\{a,b\}$; this means that a $\mathrm{\Delta }$-process is active, and may only perform outputs at $a$ and $b$, as in the following process:

Name $c$ is created in the output at $a$ and therefore $c$ inherits $a$’s visibility.

Similarly, if $\mathrm{\Delta }(d)=\{a,b\}$ then, in a $\mathrm{\Delta }$-process $d(x,c).P$, the continuation $P$ of the input at $d$ may only perform outputs at $a$, $b$ or at $c$ (as $c$ is the higher-order name received in the input). The use of visibility functions also allows us to rule out implicit forms of higher order store; in the following example, $p,q$ are higher order names used for continuations.

When extending $\mathrm{\Delta }$, we impose in $\mathrm{\Delta };a\mapsto A$ that $a\notin \mathrm{𝚍𝚘𝚖}(\mathrm{\Delta })\cup \mathrm{𝚌𝚘𝚍𝚘𝚖}(\mathrm{\Delta })$, that is, $a$ is fresh for $\mathrm{\Delta }$. Similarly, $\mathrm{\Delta };\ast \mapsto A$ is defined only when $\ast \notin \mathrm{𝚍𝚘𝚖}(\mathrm{\Delta })$.

Transitivity ensures us that the visibility functions, viewed as “named sets”, represent transitive sets. Transitivity is needed to guarantee the behavioural expectations of visibility. If a process $P$ calls a service $a$, with actual (higher-order) parameter $b$, then an output triggered by such a call (and possibly directed back to $P$) should be either at $b$ or at a name in the visibility of $a$; however, the server $a$ might call an external service $c$; this call should not allow an increase of the visibility associated to $a$; hence the transitivity constraint that the visibility of $c$ is contained in that of $a$. Technically, transitivity is necessary to ensure preservation of typing under reduction (see Theorem 10 and Example 11).

In the typing of a parallel composition, the visibility function has to be split between the two components of the composition. This is important for elements of the domain of the function that are linear, and therefore may only appear in one, but not both, components; this is the case for $\ast$, and the linear continuation names that will be introduced in Section 5.

The typing rules are given in Table 1. We comment on a few of them. Rule $𝙾\text{-}\mathrm{𝙷𝙾}$ specifies that an output at a HO name $a$ owns the thread, and that name $a$ must be in the current visibility. In the continuation $P$ (which is not active) the visibility for $b$ is determined by the current visibility $\mathrm{\Delta }(\ast )$ together with $b$ itself, to allow for recursive calls at $b$. Symmetrically, in rule $𝙸\text{-}\mathrm{𝙷𝙾}$, a process performing an input at $a$ acquires the thread, with a visibility given by $\mathrm{\Delta }(a)$ plus the received name $b$. A replicated input is well-typed only if it is not active (rule $\mathrm{𝚁𝙴𝙿}$). When typing parallel composition, we use split to insure that at most one of the components holds the thread. We simply remove the name from $\mathrm{\Delta }$ when typing a restriction (rule $\mathrm{𝚁𝙴𝚂}\text{-}\mathrm{𝙷𝙾}$). Visibility plays no role in rules $𝙸\text{-}\mathrm{𝙵𝙾}$ and $𝙾\text{-}\mathrm{𝙵𝙾}$; the only checks made are given by sequentiality, concerning the respect of the thread.

The following lemma shows that a visibility function may always be enlarged (both in the domain and codomain), as long as sequentiality (i.e., being defined on $\ast$) is respected.

Some other technical lemmas that are used in proofs are presented in Appendix B.1.

To adapt the generic definitions of behavioural equivalence in Section 2 to the type system for visibility, we only have to specify the meaning of compatibility between typing environments (which in our case are visibility functions). Compatibility means ensuring that processes typed under the two typing environments cannot both be active.

We discuss some examples of equivalences in which the behavioural constraints imposed on legal observers by visibility are essential: the equivalences would otherwise be broken.

The following example illustrates the use of visibility to perform garbage-collection on names that will never be used. We refer to Appendix B.3 for the full definition of the corresponding pruning function.

In this paper we have studied the meaning of visibility, originating from game-semantics interpretations of typed $\lambda$-calculi and reflecting absence of higher-order store, in a calculus of pure name-passing such as the $\pi$-calculus. In contrast with $\lambda$-calculi, in the $\pi$-calculus there is no explicit notion of store, and no unique identities (e.g., the input end of a name may have multiple occurrences, arbitrarily structured). These aspects determine considerable differences in the semantic analysis of visibility. For instance, in the $\pi$-calculus visibility has to be enforced by means of a dedicated type system; and the visibility functions have to satisfy special properties such as transitivity. We have highlighted such differences, and investigated the behavioural effects of visibility. In particular, we have shown full abstract characterisations of may testing and barbed equivalence, as forms of trace equivalence and labelled bisimilarity.

There are several directions for future work that we would like to pursue. In game semantics, further aspects related to first-order store have been studied; for instance allowing first-order references as values (that can be passed around) [13, 9], or allowing to store first-order references (i.e., references with types such as int ref ref [17, 10]). The distinction between first-order and higher-order state has also been studied in [14]. We would like to investigate the effects of such distinctions on our types and proof techniques.

We have worked with $\pi$I, a dialect of $\pi$-calculus in which all names exchanged are newly created. Thus $\pi$I lacks the free-output construct, where the communication of existing names is permitted. As shown in the literature [5, 25, 8], $\pi$I is closer to game semantics than the standard $\pi$-calculus. We would like to see whether our results can be adapted so to accommodate also the free output construct. While free output can be modelled in $\pi$I [2], it allows a direct representation of idioms such as “delegate to someone else the task of answering’, or the expression of tail-call recursion.

We have studied visibility on top of type systems for sequentiality and well-bracketing. Allowing concurrency would probably require relaxing the definition of the visibility functions; we leave the details to future work.