The type {xj :Aj z:A} is the type of a term which encapsulates an open process that uses the linear channels xj :Aj and offers A along channel z. This formulation has the added benefit of formalising the integration of session-typed processes in a functional language and forms the basis for the concurrent programming language SILL [37,50]. The typing rules for the new constructs are (for simplicity we assume no shared channels in process monads):

$$\frac{\Psi; ; ; \overline{x\_i : A\_i} \vdash P :: z : A}{\Psi \vdash \{z \leftarrow P \leftarrow \overline{x\_i : A\_i}\} : ; \{\overline{x\_i : A\_i} \vdash z : A\}} \tag{1}$$

$$\frac{\Psi \vdash M : \{\overline{x\_i : A\_i} \vdash x : A\} \quad \Delta\_1 = \overline{y\_i : A\_i} \quad \Psi; \Gamma; \Delta\_2, x : A \vdash Q :: z : C}{\Psi; \Gamma; \Delta\_1, \Delta\_2 \vdash x \leftarrow M \leftarrow \overline{y\_i}; Q :: z : C} \tag{1}$$

Rule {}I embeds processes in the term language by essentially quoting an open process that is well-typed according to the type specification in the monadic type. Dually, rule {}E allows for processes to use monadic values through composition that *consumes* some of the ambient channels in order to provide the monadic term with the necessary context (according to its type). These constructs are discussed in substantial detail in [50]. The reduction semantics of the process construct is given by (we tacitly assume that the names y and c do not occur in P and omit the congruence case):

$$(c \leftarrow \{z \leftarrow P \leftarrow \overline{x\_i:A\_i}\} \leftarrow \overline{y\_i};Q) \rightarrow (\nu c)(P\{\overline{y}/\overline{x\_i}\{c/z\}\} \mid Q)$$

The semantics allows for the underlying monadic term M to evaluate to a (quoted) process P. The process P is then executed in parallel with the continuation Q, sharing the linear channel c for subsequent interactions. We illustrate the higher-order extension with following typed process (we write {x ← P} when P does not depend on any linear channels and assume Q :: d:Nat ∧ **1**):

$$P \triangleq (\nu c)(c \langle \{d \gets Q\} \rangle.c(x).\mathbf{0} \mid c(y).d \gets y; d(n).c \langle n \rangle.\mathbf{0})\tag{2}$$

Process P above gives an abstract view of a communication idiom where a process (the left-hand side of the parallel composition) sends another process Q which potentially encapsulates some complex computation. The receiver then *spawns* the execution of the received process and inputs from it a result value that is sent back to the original sender. An execution of P is given by:

$$\begin{array}{c} P \rightarrow (\nu c)(c(x).\mathbf{0} \mid d \leftarrow \{d \leftarrow Q\}; d(n).c\langle n\rangle.\mathbf{0}) \rightarrow (\nu c)(c(x).\mathbf{0} \mid (\nu d)(Q \mid d(n).c\langle n\rangle.\mathbf{0})) \\ \rightarrow ^+(\nu c)(c(x).\mathbf{0} \mid c\langle 42\rangle.\mathbf{0}) \rightarrow \mathbf{0} \end{array}$$

Given the seminal work of Sangiorgi [46], such a representation naturally begs the question of whether or not we can develop a *typed* encoding of higher-order processes into the first-order setting. Indeed, we can achieve such an encoding with a fairly simple extension of the encoding of *§* **4.2** to Sessπλ+ by observing that monadic values are processes that need to be potentially provided with extra sessions in order to be executed correctly. For instance, a term of type {x:A y:B} denotes a process that given a session x of type A will then offer y:B. Exploiting this observation we encode this type as the session A - B, ensuring subsequent usages of such a term are consistent with this interpretation.

$$\begin{array}{l} \left\| \{ \overline{x\_{j}:A\_{j}} \vdash z:A \} \right\| \quad \triangleq \begin{array}{l} \left\| \overline{A\_{j}} \right\| \ \neg \left\| A \right\| \\ \hline \end{array} \\ \left\| \{ x \leftarrow P \rightarrow \overline{y\_{i}} \} \right\| \; \triangleq \; z(y\_{0}) \dots z(y\_{n}) . \left\| P \{ z/x \} \right\| \quad (z \notin fn(P)) \\ \left\| x \leftarrow M \leftarrow \overline{y\_{i}}; Q \right\| \triangleq \left( \nu x \right) (\left\| M \right\|\_{x} \mid \overline{x} \langle a\_{0} \rangle . ([a\_{0} \leftrightarrow y\_{0}] \mid \cdot \cdot \mid x \langle a\_{n} \rangle . ([a\_{n} \leftrightarrow y\_{n}] \mid [\![Q] \} \ldots .))) \end{array}$$

To encode the monadic type {xj :Aj z:A}, denoting the type of process P that is typed by xj :Aj P :: z:A, we require that the session in the image of the translation specifies a sequence of channel inputs with behaviours Aj that make up the linear context. After the contextual aspects of the type are encoded, the session will then offer the (encoded) behaviour of A. Thus, the encoding of the monadic type is -A0 - ... - -An - -A, which we write as -Aj - -A. The encoding of monadic expressions adheres to this behaviour, first performing the necessary sequence of inputs and then proceeding inductively. Finally, the encoding of the elimination form for monadic expressions behaves dually, composing the encoding of the monadic expression with a sequence of outputs that instantiate the consumed names accordingly (via forwarding). The encoding of process P from Eq. 2 is thus:

$$\begin{array}{l} \{P\} = (\nu c)(\lceil c\langle\{d \gets Q\}\rangle.c(x).\mathbf{0}) \mid \lceil c(y).d \gets y; d(n).c\langle n\rangle.\mathbf{0})\} \\ = (\nu c)(\overline{c}\langle w\rangle.(\lvert w(d).\lbrack Q\}\mid c(x).\mathbf{0})c(y).\langle \nu d\rangle(\overline{y}\langle b\rangle.\lbrack b \gets d\vert \mid d(n).\overline{c}\langle m\rangle.\langle \overline{n}\langle e\rangle.\lbrack e \gets m\vert \mid \mathbf{0}\rangle)\} \end{array}$$

**Properties of the Encoding.** As in our previous development, we can show that our encoding for Sessπλ+ is type sound and satisfies operational correspondence. The full development is omitted but can be found in [52].

We encode Sessπλ+ into λ-terms, extending *§* **4.2** with:

$$\begin{array}{l} \{\{\overline{x\_{i}:A\_{i}}\vdash z:A\}\} \triangleq \overline{\{A\_{i}\}} \multimap \{A\} \\\{x \leftarrow M \leftarrow \overline{y\_{i}}; Q\} \triangleq \{Q\} \{ (\{M\}\,\overline{y\_{i}})/x\} \end{array} \quad \{\{x \leftarrow P \leftarrow \overline{w\_{i}}\}\} \triangleq \lambda w\_{0} \dots \lambda w\_{n}. \{P\} \end{array}$$

The encoding translates the monadic type {xi:Ai z:A} as a linear function Ai - A, which captures the fact that the underlying value must be provided with terms satisfying the requirements of the linear context. At the level of terms, the encoding for the monadic term constructor follows its type specification, generating a nesting of λ-abstractions that closes the term and proceeding inductively. For the process encoding, we translate the monadic application construct analogously to the translation of a linear cut, but applying the appropriate variables to the translated monadic term (which is of function type). We remark the similarity between our encoding and that of the previous section, where monadic terms are translated to a sequence of inputs (here a nesting of λ-abstractions). Our encoding satisfies type soundness and operational correspondence, as usual. Further showcasing the applications of our development, we obtain a novel strong normalisation result for this higher-order session-calculus "for free", through encoding to the λ-calculus.

**Theorem 4.9 (Strong Normalisation).** *Let* Ψ; Γ; Δ P :: z:A*. There is no infinite reduction sequence starting from* P*.*

**Theorem 4.10 (Inverse Encodings).** *If* Ψ; Γ; Δ P :: z:A *then* -Pz ≈L -P*. Also, if* Ψ M : τ *then* -Mz =β M*.*

**Theorem 4.11.** *Let* M : τ *,* N : τ *,* P :: z:A *and* Q :: z:A*.* M =βη N *iff* -Mz ≈L -Nz *and* -P ≈L -Q *iff* P =βη Q*.*

### **5 Related Work and Concluding Remarks**

**Process Encodings of Functions.** Toninho et al. [49] study encodings of the simply-typed λ-calculus in a logically motivated session π-calculus, via encodings to the linear λ-calculus. Our work differs since they do not study polymorphism nor reverse encodings; and we provide deeper insights through applications of the encodings. Full abstraction or inverse properties are not studied.

Sangiorgi [43] uses a fully abstract compilation from the higher-order πcalculus (HOπ) to the π-calculus to study full abstraction for Milner's encodings of the λ-calculus. The work shows that Milner's encoding of the lazy λ-calculus can be recovered by restricting the semantic domain of processes (the so-called *restrictive* approach) or by enriching the λ-calculus with suitable constants. This work was later refined in [45], which does not use HOπ and considers an operational equivalence on λ-terms called *open applicative bisimulation* which coincides with L´evy-Longo tree equality. The work [47] studies general conditions under which encodings of the λ-calculus in the π-calculus are fully abstract wrt L´evy-Longo and B¨ohm Trees, which are then applied to several encodings of (callby-name) λ-calculus. The works above deal with *untyped calculi*, and so reverse encodings are unfeasible. In a broader sense, our approach takes the restrictive approach using linear logic-based session typing and the induced observational equivalence. We use a λ-calculus with booleans as observables and reason with a Morris-style equivalence instead of tree equalities. It would be an interesting future work to apply the conditions in [47] in our typed setting.

Wadler [54] shows a correspondence between a linear functional language with session types GV and a session-typed process calculus with polymorphism based on classical linear logic CP. Along the lines of this work, Lindley and Morris [26], in an exploration of inductive and coinductive session types through the addition of least and greatest fixed points to CP and GV, develop an encoding from a linear λ-calculus with session primitives (Concurrent μGV) to a pure linear λ-calculus (Functional μGV) via a CPS transformation. They also develop translations between μCP and Concurrent μGV, extending [25]. Mapping to the terminology used in our work [17], their encodings are shown to be operationally complete, but no results are shown for the operational soundness directions and neither full abstraction nor inverse properties are studied. In addition, their operational characterisations do not compose across encodings. For instance, while strong normalisation of Functional μGV implies the same property for Concurrent μGV through their operationally complete encoding, the encoding from μCP to μGV does not necessarily preserve this property.

Types for π-calculi delineate sequential behaviours by restricting composition and name usages, limiting the contexts in which processes can interact. Therefore typed equivalences offer a *coarser* semantics than untyped semantics. Berger et al. [5] study an encoding of System F in a polymorphic linear π-calculus, showing it to be fully abstract based on game semantics techniques. Their typing system and proofs are more complex due to the fine-grained constraints from game semantics. Moreover, they do not study a reverse encoding. Orchard and Yoshida [33] develop embeddings to-and-from PCF with parallel effects and a sessiontyped π-calculus, but only develop operational correspondence and semantic soundness results, leaving the full abstraction problem open.

**Polymorphism and Typed Behavioural Semantics.** The work of [7] studies parametric session polymorphism for the intuitionistic setting, developing a behavioural equivalence that captures parametricity, which is used (denoted as ≈L) in our paper. The work [39] introduces a typed bisimilarity for polymorphism in the π-calculus. Their bisimilarity is of an intensional flavour, whereas the one used in our work follows the extensional style of Reynolds [41]. Their typing discipline (originally from [53], which also develops type-preserving encodings of polymorphic λ-calculus into polymorphic π-calculus) differs significantly from the linear logic-based session typing of our work (e.g. theirs does not ensure deadlock-freedom). A key observation in their work is the coarser nature of typed equivalences with polymorphism (in analogy to those for IO-subtyping [38]) and their interaction with channel aliasing, suggesting a use of typed semantics and encodings of the π-calculus for fine-grained analyses of program behaviour.

**F-Algebras and Linear-F.** The use of initial and final (co)algebras to give a semantics to inductive and coinductive types dates back to Mendler [28], with their strong definability in System F appearing in [1,19]. The definability of inductive and coinductive types using parametricity also appears in [40] in the context of a logic for parametric polymorphism and later in [6] in a linear variant of such a logic. The work of [55] studies parametricity for the polymorphic linear λ-calculus of this work, developing encodings of a few inductive types but not the initial (or final) algebraic encodings in their full generality. Inductive and coinductive session types in a logical process setting appear in [26,51]. Both works consider a calculus with built-in recursion – the former in an intuitionistic setting where a process that offers a (co)inductive protocol is composed with another that consumes the (co)inductive protocol and the latter in a classical framework where composed recursive session types are dual each other.

**Conclusion and Future Work.** This work answers the question of what kind of type discipline of the π-calculus can exactly capture and is captured by λcalculus behaviours. Our answer is given by showing the first mutually inverse and fully abstract encodings between two calculi with polymorphism, one being the Polyπ session calculus based on intuitionistic linear logic, and the other (a linear) System F. This further demonstrates that the linear logic-based articulation of name-passing interactions originally proposed by [8] (and studied extensively thereafter e.g. [7,9,25,36,50,51,54]) provides a clear and applicable tool for message-passing concurrency. By exploiting the proof theoretic equivalences between natural deduction and sequent calculus we develop mutually inverse and fully abstract encodings, which naturally extend to more intricate settings such as process passing (in the sense of HOπ). Our encodings also enable us to derive properties of the π-calculi "for free". Specifically, we show how to obtain adequate representations of least and greatest fixed points in Polyπ through the encoding of initial and final (co)algebras in the λ-calculus. We also straightforwardly derive a strong normalisation result for the higher-order session calculus, which otherwise involves non-trivial proof techniques [5,7,12,13,36]. Future work includes extensions to the classical linear logic-based framework, including multiparty session types [10,11]. Encodings of session π-calculi to the λ-calculus have been used to implement session primitives in functional languages such as Haskell (see a recent survey [32]), OCaml [24,34,35] and Scala [48]. Following this line of work, we plan to develop encoding-based implementations of this work as embedded DSLs. This would potentially enable an exploration of algebraic constructs beyond initial and final co-algebras in a session programming setting. In particular, we wish to further study the meaning of functors, natural transformations and related constructions in a session-typed setting, both from a more fundamental viewpoint but also in terms of programming patterns.

**Acknowledgements.** The authors thank Viviana Bono, Dominic Orchard and the reviewers for their comments, suggestions and pointers to related works. This work is partially supported by EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1 and NOVA LINCS (UID/CEC/04516/2013).

### **References**

**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 chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter'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.

### **Concurrent Kleene Algebra: Free Model and Completeness**

Tobias Kapp´e(B), Paul Brunet, Alexandra Silva, and Fabio Zanasi

University College London, London, UK<EMAIL_ADDRESS>
**Abstract.** Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the axioms for CKA with bounded parallelism are complete for the semantics proposed in the original paper; consequently, these semantics are the free model for this fragment. This result settles a conjecture of Hoare and collaborators. Moreover, the technique developed to this end allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.

### **1 Introduction**

Concurrent Kleene Algebra (CKA) [8] is a mathematical formalism which extends Kleene Algebra (KA) with a parallel composition operator, in order to express concurrent program behaviour.1 In spite of such a seemingly simple addition, extending the existing KA toolkit (notably, completeness) to the setting of CKA turned out to be a challenging task. A lot of research happened since the original paper, both foundational [13,20] and on how CKA could be used to reason about important verification tasks in concurrent systems [9,11]. However, and despite several conjectures [9,13], the question of the characterisation of the free CKA and the completeness of the axioms remained open, making it impractical to use CKA in verification tasks. This paper settles these two open questions. We answer positively the conjecture that the free model of CKA is formed by series parallel pomset languages, downward-closed under Gischer's subsumption order [6]—a generalisation of regular languages to sets of partially ordered words. To this end, we prove that the original axioms proposed in [8] are indeed complete.

Our proof of completeness is based on extending an existing completeness result that establishes series-parallel rational pomset languages as the free Bi-Kleene Algebra (BKA) [20]. The extension to the existing result for BKA provides a clear understanding of the difficulties introduced by the presence of the exchange axiom and shows how to separate concerns between CKA and BKA, a technique which is also useful elsewhere. For one, our construction also provides

c The Author(s) 2018

1 In its original formulation, CKA also features an operator (*parallel star*) for unbounded parallelism: in harmony with several recent works [13,14], we study the variant of CKA without parallel star, sometimes called "weak" CKA.

A. Ahmed (Ed.): ESOP 2018, LNCS 10801, pp. 856–882, 2018. https://doi.org/10.1007/978-3-319-89884-1\_30

an extension of (half of) Kleene's theorem for BKA [14] to CKA, establishing pomset automata as an operational model for CKA and opening the door to decidability procedures similar to those previously studied for KA. Furthermore, it reduces deciding the equational theory of CKA to deciding the equational theory of BKA.

BKA is defined as CKA with the only (but significant) omission of the *exchange law*, (e f) · (g h) -CKA (e · g) - (f · h). The exchange law is the core element of CKA as it softens true concurrency: it states that when two sequentially composed programs (i.e., e · g and f · h) are composed in parallel, they can be implemented by running their heads in parallel, followed by running their tails in parallel (i.e., e f, then g h). The exchange law allows the implementer of a CKA expression to interleave threads at will, without violating the specification.

To illustrate the use of the exchange law, consider a protocol with three actions: query a channel c, collect an answer from the same channel, and print an unrelated message m on screen. The specification for this protocol requires the query to happen before reception of the message, but the printing action being independent, it may be executed concurrently. We will write this specification as (q(c) · r(c)) p(m), with the operator · denoting sequential composition. However, if one wants to implement this protocol in a sequential programming language, a total ordering of these events has to be introduced. Suppose we choose to implement this protocol by printing m while we wait to receive an answer. This implementation can be written q(c) · p(m) · r(c). Using the laws of CKA, we can prove that q(c) · p(m) · r(c) -CKA (q(c) · r(c)) p(m), which we interpret as the fact that this implementation respects the specification. Intuitively, this means that the specification lists the necessary dependencies, but the implementation can introduce more.

Having a complete axiomatisation of CKA has two main benefits. First, it allows one to get certificates of correctness. Indeed, if one wants to use CKA for program verification, the decision procedure presented in [3] may be used to test program equivalence. If the test gives a negative answer, this algorithm provides a counter-example. However if the answer is positive, no meaningful witness is produced. With the completeness result presented here, that is constructive in nature, one could generate an axiomatic proof of equivalence in these cases. Second, it gives one a simple way of checking when the aforementioned procedure applies. By construction, we know that two terms are semantically equivalent whenever they are equal in every concurrent Kleene algebra, that is any model of the axioms of CKA. This means that if we consider a specific semantic domain, one simply needs to check that the axioms of CKA hold in there to know that the decision procedure of [3] is sound in this model.

While this paper was in writing, a manuscript with the same result appeared [19]. Among other things, the proof presented here is different in that it explicitly shows how to syntactically construct terms that express certain pomset languages, as opposed to showing that such terms must exist by reasoning on a semantic level. We refer to Sect. 5 for a more extensive comparison.

The remainder of this paper is organised as follows. In Sect. 2, we give an informal overview of the completeness proof. In Sect. 3, we introduce the necessary concepts, notation and lemmas. In Sect. 4, we work out the proof. We discuss the result in a broader perspective and outline further work in Sect. 5.

### **2 Overview of the Completeness Proof**

We start with an overview of the steps necessary to arrive at the main result. As mentioned, our strategy in tackling CKA-completeness is to build on the existing BKA-completeness result. Following an observation by Laurence and Struth, we identify *downward-closure* (under Gischer's subsumption order [6]) as the feature that distinguishes the pomsets giving semantics to BKA-expressions from those associated with CKA-expressions. In a slogan,

CKA-semantics = BKA-semantics + downward-closure.

This situation is depicted in the upper part of the commuting diagram in Fig. 1. Intuitively, downward-closure can be thought of as the semantic outcome of adding the exchange axiom, which distinguishes CKA from BKA. Thus, if a and b are events that can happen in parallel according to the BKA-semantics of a term, then a and b may also be ordered in the CKA-semantics of that same term.

**Fig. 1.** The connection between BKA and CKA semantics mediated by closure.

The core of our CKA-completeness proof will be to construct a syntactic counterpart to the semantic closure. Concretely, we shall build a function that maps a CKA term e to an equivalent term e↓, called the (syntactic) *closure* of e. The lower part of the commuting diagram in Fig. 1 shows the property that e↓ must satisfy in order to deserve the name of closure: its BKA semantics has to be the same as the CKA semantics of e.

*Example 2.1.* Consider e = a b, whose CKA-semantics prescribe that a and b are events that may happen in parallel. One closure of this term would be e↓ = a b+a·b+b·a, whose BKA-semantics stipulate that either a and b execute purely in parallel, or a precedes b, or b precedes a—thus matching the optional parallelism of a and b. For a more non-trivial example, take e = a- b-, which represents that finitely many repetitions of a and b occur, possibly in parallel. A closure of this term would be e↓ = (a- b-) - : finitely many repetitions of a and b occur truly in parallel, which is repeated indefinitely.

In order to find e↓ systematically, we are going to construct it in stages, through a completely syntactic procedure where each transformation has to be valid according to the axioms. There are three main stages.

As a straightforward consequence of the closure construction, we obtain a completeness theorem for CKA, which establishes the set of closed series-rational pomset languages as the free CKA.

### **3 Preliminaries**

We fix a finite set of symbols Σ, the *alphabet*. We use the symbols a, b and c to denote elements of Σ. The two-element set {0, 1} is denoted by 2. Given a set S, the set of subsets (*powerset*) of S is denoted by 2S.

In the interest of readability, the proofs for technical lemmas in this section can be found in the full version [15].

### **3.1 Pomsets**

A trace of a sequential program can be modelled as a word, where each letter represents an atomic event, and the order of the letters in the word represents the order in which the events took place. Analogously, a trace of a concurrent program can be thought of as word where letters are partially ordered, i.e., there need not be a causal link between events. In literature, such a partially ordered word is commonly called a *partial word* [7], or *partially ordered multiset* (*pomset*, for short) [6]; we use the latter term.

A formal definition of pomsets requires some work, because the partial order should order *occurrences* of events rather than the events themselves. For this reason, we first define a labelled poset.

**Definition 3.1.** *A* labelled poset *is a tuple* S, ≤, λ*, where* S, ≤ *is a partially ordered set (i.e.,* S *is a set and* ≤ *is a partial order on* S*), in which* S *is called the* carrier *and* ≤ *is the* order*;* λ : S → Σ *is a function called the* labelling*.*

We denote labelled posets with lower-case bold symbols **u**, **v**, et cetera. Given a labelled poset **u**, we write S**u** for its carrier, ≤**u** for its order and λ**u** for its labelling. We write **1** for the empty labelled poset. We say that two labelled posets are *disjoint* if their carriers are disjoint.

Disjoint labelled posets can be composed parallelly and sequentially; parallel composition simply juxtaposes the events, while sequential composition imposes an ordering between occurrences of events originating from the left operand and those originating from the right operand.

**Definition 3.2.** *Let* **u** *and* **v** *be disjoint. We write* **u v** *for the* parallel composition *of* **u** *and* **v***, which is the labelled poset with the carrier* S**u**∪**v** = S**u** ∪S**v***, the order* ≤**uv** = ≤**u** ∪ ≤**v** *and the labeling* λ**uv** *defined by*

$$
\lambda\_{\mathbf{u}\parallel\mathbf{v}}(x) = \begin{cases}
\lambda\_{\mathbf{u}}(x) & x \in S\_{\mathbf{u}}; \\
\lambda\_{\mathbf{v}}(x) & x \in S\_{\mathbf{v}}.
\end{cases}
$$

*Similarly, we write* **u** · **v** *for the* sequential composition *of* **u** *and* **v***, that is, labelled poset with the carrier* S**u**∪**v** *and the partial order*

$$
\leq\_{\mathbf{u}\cdot\mathbf{v}} = \leq\_{\mathbf{u}} \cup \leq\_{\mathbf{v}} \cup (S\_{\mathbf{u}} \times S\_{\mathbf{v}}),
$$

*as well as the labelling* λ**u**·**v** = λ**uv***.*

Note that **1** is neutral for sequential and parallel composition, in the sense that we have **1 u** = **1** · **u** = **u** = **u** · **1** = **u** -**1**.

There is a natural ordering between labelled posets with regard to concurrency.

**Definition 3.3.** *Let* **u**, **v** *be labelled posets. A* subsumption *from* **u** *to* **v** *is a bijection* h : S**u** → S**v** *that preserves order and labels, i.e.,* u ≤**u** u *implies that* h(u) ≤**v** h(u )*, and* λ**v** ◦h = λ**u***. We simplify and write* h : **u** → **v** *for a subsumption from* **u** *to* **v***. If such a subsumption exists, we write* **v u***. Furthermore,* h *is an* isomorphism *if both* h *and its inverse* h−1 *are subsumptions. If there exists an isomorphism from* **u** *to* **v** *we write* **u** ∼= **v***.*

Intuitively, if **u v**, then **u** and **v** both order the same set of (occurrences of) events, but **u** has more causal links, or "is more sequential" than **v**. One easily sees that is a preorder on labelled posets of finite carrier.

Since the actual contents of the carrier of a labelled poset do not matter, we can abstract from them using isomorphism. This gives rise to pomsets.

**Definition 3.4.** *A* pomset *is an isomorphism class of labelled posets, i.e., the class* [**v**] {**u** : **u** ∼= **v**} *for some labelled poset* **v***. Composition lifts to pomsets: we write* [**u**] - [**v**] *for* [**u v**] *and* [**u**] · [**v**] *for* [**u** · **v**]*. Similarly, subsumption also lifts to pomsets: we write* [**u**] [**v**]*, precisely when* **u v***.*

We denote pomsets with upper-case symbols U, V , et cetera. The *empty pomset*, i.e., [**1**] = {**1**}, is denoted by 1; this pomset is neutral for sequential and parallel composition. To ensure that [**v**] is a set, we limit the discussion to labelled posets whose carrier is a subset of some set S. The labelled posets in this paper have finite carrier; it thus suffices to choose S = N to represent all pomsets with finite (or even countably infinite) carrier.

Composition of pomsets is well-defined: if **u** and **v** are not disjoint, we can find **u** , **v** disjoint from **u**, **v** respectively such that **u** ∼= **u** and **v** ∼= **v** . The choice of representative does not matter, for if **u** ∼= **u** and **v** ∼= **v** , then **u** · **v** ∼= **u** · **v** . Subsumption of pomsets is also well-defined: if **u** ∼= **u v** ∼= **v** , then **u v** . One easily sees that is a partial order on finite pomsets, and that sequential and parallel composition are monotone with respect to , i.e., if U W and V X, then U · V W · X and U - V W - X. Lastly, we note that both types of composition are associative, both on the level of pomsets and labelled posets; we therefore omit parentheses when no ambiguity is likely.

**Series-Parallel Pomsets.** If a ∈ Σ, we can construct a labelled poset with a single element labelled by a; indeed, since any labelled poset thus constructed is isomorphic, we also use a to denote this isomorphism class; such a pomset is called a *primitive pomset*. A pomset built from primitive pomsets and sequential and parallel composition is called *series-parallel*; more formally:

**Definition 3.5.** *The set of* series-parallel *pomsets, denoted* SP(Σ)*, is the smallest set such that* 1 ∈ SP(Σ) *as well as* a ∈ SP(Σ) *for every* a ∈ Σ*, and is closed under parallel and sequential composition.*

We elide the sequential composition operator when we explicitly construct a pomset from primitive pomsets, i.e., we write ab instead of a · b for the pomset obtained by sequentially composing the (primitive) pomsets a and b. In this notation, sequential composition takes precedence over parallel composition.

All pomsets encountered in this paper are series-parallel. A useful feature of series-parallel pomsets is that we can deconstruct them in a standard fashion [6].

**Lemma 3.1.** *Let* U ∈ SP(Σ)*.

In the sequel, it will be useful to refer to pomsets that are *not* of the third kind above, i.e., cannot be written as U0 · U1 for U0, U1 ∈ SP(Σ) \ {1}, as *nonsequential* pomsets. Lemma 3.1 gives a normal form for series-parallel pomsets, as follows.

 We now go over some lemmas on pomsets that will allow us to factorise pomsets later on. First of all, one easily shows that subsumption is irrelevant on empty and primitive pomsets, as witnessed by the following lemma.

 If* U *is empty or primitive, then* U = V *.*

We can also consider how pomset composition and subsumption relate. It is not hard to see that if a pomset is subsumed by a sequentially composed pomset, then this sequential composition also appears in the subsumed pomset. A similar statement holds for pomsets that subsume a parallel composition.

 Then there exist pomsets* U0 *and* U1 *such that:*

U = U0 · U1, U0 V0, and U1 V1.

*Also, if* U0*,* U1 *and* V *are pomsets such that* U0 - U1 V *, then there exist pomsets* V0 *and* V1 *such that:*

$$V = V\_0 \parallel V\_1, \ U\_0 \sqsubseteq V\_0, \text{ and } U\_1 \sqsubseteq V\_1.$$

The next lemma can be thought of as a generalisation of Levi's lemma [21], a well-known statement about words, to pomsets. It says that if a sequential composition is subsumed by another (possibly longer) sequential composition, then there must be a pomset "in the middle", describing the overlap between the two; this pomset gives rise to a factorisation.

**Lemma 3.4.** *Let* U *and* V *be pomsets, and let* W0, W1,...,Wn−1 *with* n > 0 *be non-empty pomsets such that* U · V W0 · W1 ··· Wn−1*.

Levi's lemma also has an analogue for parallel composition.

**Lemma 3.5.** *Let* U, V, W, X *be pomsets such that* U - V = W - X*. There exist pomsets* Y0, Y1, Z0, Z1 *such that*

$$U = Y\_0 \parallel Y\_1, \; V = Z\_0 \parallel Z\_1, \; W = Y\_0 \parallel Z\_0, \; and \; X = Y\_1 \parallel Z\_1.$$

The final lemma is useful when we have a sequentially composed pomset subsumed by a parallelly composed pomset. It tells us that we can factor the involved pomsets to find subsumptions between smaller pomsets. This lemma first appeared in [6], where it is called the interpolation lemma.

**Lemma 3.6 (Interpolation).** *Let* U, V, W, X *be pomsets such that* U · V *is subsumed by* W -X*. Then there exist pomsets* W0, W1, X0, X1 *such that*

$$W\_0 \cdot W\_1 \subseteq W, \, X\_0 \cdot X\_1 \subseteq X, \, U \subseteq W\_0 \parallel X\_0, \, and \, V \subseteq W\_1 \parallel X\_1.$$

*Moreover, if* W *and* X *are series-parallel, then so are* W0*,* W1*,* X0 *and* X1*.*

On a semi-formal level, the interpolation lemma can be understood as follows. If U · V W - X, then the events in W are partitioned between those that end up in U, and those that end up in V ; these give rise to the "sub-pomsets" W0 and W1 of W, respectively. Similarly, X partitions into "sub-pomsets" X0 and X1. We refer to Fig. 2 for a graphical depiction of this situation.

Now, if y precedes z in W0 - X0, then y must precede z in W - X, and therefore also in U · V . Since y and z are both events in U, it then follows that y precedes z in U, establishing that U W0 - X0. Furthermore, if y precedes z in W, then we can exclude the case where y is in W1 and z in W0, for then z precedes y in U · V , contradicting that y precedes z in U · V . Accordingly, either y and z both belong to W0 or W1, or y is in W0 while z is in W1; in all of these cases, y must precede z in W0 · W1. The other subsumptions hold analogously.

**Fig. 2.** Splitting pomsets in the interpolation lemma

**Pomset Languages.** The semantics of BKA and CKA are given in terms of sets of series-parallel pomsets.

**Definition 3.6.** *A subset of* SP(Σ) *is referred to as a* pomset language*.*

As a convention, we denote pomset languages by the symbols U, V, et cetera. Sequential and parallel composition of pomsets extends to pomset languages in a pointwise manner, i.e.,

$$\mathcal{U} \cdot \mathcal{V} \stackrel{\ominus}{=} \{ U \cdot V : U \in \mathcal{U}, V \in \mathcal{V} \}$$

and similarly for parallel composition. Like languages of words, pomset languages have a Kleene star operator, which is similarly defined, i.e., U- n∈N U n, where the nth power of U is inductively defined as U0 {1} and U n+1 U n · U.

 The *closure under subsumption* (or simply *closure*) of a pomset language U, denoted U↓, is defined as the smallest pomset language that contains U and is closed, i.e.,

$$\mathcal{U} \upharpoonright \underline{\mathcal{C}} \upharpoonright \{U' \in \mathsf{SP}(\Sigma) : \exists U \in \mathcal{U}. \ U' \sqsubseteq U\},$$

Closure relates to union, sequential composition and iteration as follows.

**Lemma 3.7.** *Let* U, V *be pomset languages; then:*

(U∪V)↓ = U↓ ∪ V↓, (U·V)↓ = U↓ · V↓, and U-↓ = U↓-.

*Proof.* The first claim holds for infinite unions, too, and follows immediately from the definition of closure.

For the second claim, suppose that U ∈ U and V ∈ V, and that W U · V . By Lemma 3.3, we find pomsets W0 and W1 such that W = W0 · W1, with W0 U and W1 V . It then holds that W0 ∈ U↓ and W1 ∈ V↓, meaning that W = W0 · W1 ∈ U↓·V↓. This shows that (U·V)↓ U↓·V↓. Proving the reverse inclusion is a simple matter of unfolding the definitions.

For the third claim, we can calculate directly using the first and second parts of this lemma:

$$\mathcal{U}^{\star}\downarrow = \left(\bigcup\_{n\in\mathbb{N}}\underbrace{\mathcal{U}\cdot\mathcal{U}\cdots\mathcal{U}}\_{n\text{ times}}\right)\downarrow = \bigcup\_{n\in\mathbb{N}}\left(\underbrace{\mathcal{U}\cdot\mathcal{U}\cdots\mathcal{U}}\_{n\text{ times}}\right)\downarrow = \bigcup\_{n\in\mathbb{N}}\underbrace{\mathcal{U}\downarrow\mathcal{U}\downarrow\cdots\mathcal{U}}\_{n\text{ times}}\underbrace{\mathcal{U}^{\star}}\_{n\text{ times}} = \mathcal{U}\downarrow^{\star}$$

#### **3.2 Concurrent Kleene Algebra**

We now consider two extensions of Kleene Algebra (KA), known as *Bi-Kleene Algebra* (BKA) and *Concurrent Kleene Algebra* (CKA). Both extend KA with an operator for parallel composition and thus share a common syntax.

**Definition 3.7.** *The set* T *is the smallest set generated by the grammar*

e, f ::= 0 | 1 | a ∈ Σ | e + f | e · f | e f | e-

The BKA-semantics of a term is a straightforward inductive application of the operators on the level of pomset languages. The CKA-semantics of a term is the BKA-semantics, downward-closed under the subsumption order; the CKAsemantics thus includes all possible sequentialisations.

**Definition 3.8.** *The function* -−BKA : T → 2SP(Σ) *is defined as follows:*

$$\begin{aligned} \left[\mathbb{I}\right]\_{\mathsf{BK}} & \stackrel{\scriptstyle \Delta}{=} \emptyset \end{aligned} \qquad \qquad \left[e+f\right]\_{\mathsf{BK}} \stackrel{\scriptstyle \Delta}{=} \left[e\right]\_{\mathsf{BK}} \cup \left[f\right]\_{\mathsf{BK}} \qquad \left[e^{\star}\right]\_{\mathsf{BK}} \stackrel{\scriptstyle \Delta}{=} \left[e\right]\_{\mathsf{BK}}^{\star}$$

$$\left[1\right]\_{\mathsf{BK}} \stackrel{\scriptstyle \Delta}{=} \left\{1\right\} \qquad \left[e\cdot f\right]\_{\mathsf{BK}} \stackrel{\scriptstyle \Delta}{=} \left[e\right]\_{\mathsf{BK}} \cdot \left[f\right]\_{\mathsf{BK}}$$

$$\left[a\right]\_{\mathsf{BK}} \stackrel{\scriptstyle \Delta}{=} \left\{a\right\} \qquad \left[e\parallel f\right]\_{\mathsf{BK}} \stackrel{\scriptstyle \Delta}{=} \left[e\right]\_{\mathsf{BK}} \parallel \left[f\right]\_{\mathsf{BK}}$$

*Finally,* -−CKA : T → 2SP(Σ) *is defined as* eCKA eBKA↓*.*

To axiomatise semantic equivalence between terms, we build the following relations, which match the axioms proposed in [20]. The axioms of CKA as defined in [8] come from a double quantale structure mediated by the exchange law; these imply the ones given here. The converse implication does not hold; in particular, our syntax does not include an infinitary greatest lower bound operator. However, BKA (as defined in this paper) does have a *finitary* greatest lower bound [20], and by the existence of closure, so does CKA.

 The final (conditional) axiom is referred to as the* least fixpoint axiom*.*

*The relation* ≡CKA *is the smallest congruence on* T *that satisfies the rules of* ≡BKA*, and furthermore satisfies the* exchange law *for all* e, f, g, h ∈ T *:*

$$(e \parallel f) \cdot (g \parallel h) \leq\_{\mathsf{c\&A}} (e \cdot g) \parallel (f \cdot h)$$

*where we similarly use* e -CKA f *as a shorthand for* e + f ≡CKA f*.*

We can see that ≡BKA includes the familiar axioms of KA, and stipulates that is commutative and associative with unit 1 and annihilator 0, as well as distributive over +. When using CKA to model concurrent program flow, the exchange law models sequentialisation: if we have two programs, the first of which executes e followed by g, and the second of which executes f followed by h, then we can sequentialise this by executing e and f in parallel, followed by executing g and h in parallel.

We use the symbol T in statements that are true for T ∈ {BKA, CKA}. The relation ≡T is sound for equivalence of terms under T [13].

**Lemma 3.8.** *Let* e, f ∈ T *. If* e ≡T f*, then* eT = fT*.*

Since all binary operators are associative (up to ≡T), we drop parentheses when writing terms like e + f + g—this does not incur ambiguity with regard to -−T. We furthermore consider · to have precedence over -, which has precedence over +; as usual, the Kleene star has the highest precedence of all operators. For instance, when we write e + f · g- h, this should be read as e + ((f ·(g-)) h).

In case of BKA, the implication in Lemma 3.8 is an equivalence [20], and thus gives a complete axiomatisation of semantic BKA-equivalence of terms.2

**Theorem 3.1.** *Let* e, f ∈ T *. Then* e ≡BKA f *if and only if* eBKA = fBKA*.*

Given a term e ∈ T , we can determine syntactically whether its (BKA or CKA) semantics contains the empty pomset, using the function defined below.

2 Strictly speaking, the proof in [20] includes the parallel star operator in BKA. Since this is a conservative extension of BKA, this proof applies to BKA as well.

**Definition 3.10.** *The* nullability function : T → 2 *is defined as follows:*

*in which* ∨ *and* ∧ *are understood as the usual lattice operations on* 2*.*

That encodes the presence of 1 in the semantics is witnessed by the following.

**Lemma 3.9.** *Let* e ∈ T *. Then* (e) -T e *and* 1 ∈ eT *if and only if* (e)=1*.*

In the sequel, we need the *(parallel) width* of a term. This is defined as follows.

**Definition 3.11.** *Let* e ∈ T *. The* (parallel) width *of* e*, denoted by* |e|*, is defined as* 0 *when* e ≡BKA 0*; for all other cases, it is defined inductively, as follows:*

The width of a term is invariant with respect to equivalence of terms.

**Lemma 3.10.** *Let* e, f ∈ T *. If* e ≡BKA f*, then* |e| = |f|*.*

The width of a term is related to its semantics as demonstrated below.

 Then* |e| > 0*.*

#### **3.3 Linear Systems**

KA is equipped to find the least solutions to linear inequations. For instance, if we want to find X such that e · X + f -KA X, it is not hard to show that e- · f is the *least solution* for X, in the sense that this choice of X satisfies the inequation, and for any choice of X that also satisfies this inequation it holds that e- · f -KA X. Since KA is contained in BKA and CKA, the same constructions also apply there. These axioms generalise to systems of linear inequations in a straightforward manner; indeed, Kozen [18] exploited this generalisation to axiomatise KA. In this paper, we use systems of linear inequations to construct particular expressions. To do this, we introduce vectors and matrices of terms.

For the remainder of this section, we fix I as a finite set.

**Definition 3.12.** *An* I-vector *is a function from* I *to* T *. Addition of* I*-vectors is defined pointwise, i.e., if* p *and* q *are* I*-vectors, then* p + q *is the* I*-vector defined for* i ∈ I *by* (p + q)(i) p(i) + q(i)*.*

*An* I-matrix *is a function from* I2 *to* T *. Left-multiplication of an* I*-vector by an* I*-matrix is defined in the usual fashion, i.e., if* M *is an* I*-matrix and* p *is an* I*-vector, then* M · p *is the* I*-vector defined for* i ∈ I *by*

$$(M \cdot p)(i) \stackrel{\Delta}{=} \sum\_{j \in I} M(i, j) \cdot p(j)$$

Equivalence between terms extends pointwise to I-vectors. More precisely, we write p ≡T q for I-vectors p and q when p(i) ≡T q(i) for all i ∈ I, and p -T q when p + q ≡T q.

**Definition 3.13.** *An* I-linear system L *is a pair* M, p *where* M *is an* I*-matrix and* p *is an* I*-vector. A* solution *to* L *in* T *is an* I*-vector* s *such that* M·s+p -T s*. A* least solution *to* L *in* T *is a solution* s *in* T *such that for any solution* t *in* T *it holds that* s -T t*.*

It is not very hard to show that least solutions of a linear system are unique, up to ≡T; we therefore speak of *the* least solution of a linear system.

Interestingly, *any* I-linear system has a least solution, and one can construct this solution using only the operators of KA. The construction proceeds by induction on |I|. In the base, where I is empty, the solution is trivial; for the inductive step it suffices to reduce the problem to finding the least solution of a strictly smaller linear system. This construction is not unlike Kleene's procedure to obtain a regular expression from a finite automaton [17]. Alternatively, we can regard the existence of least solutions as a special case of Kozen's proof of the fixpoint for matrices over a KA, as seen in [18, Lemma 9].

As a matter of fact, because this construction uses the axioms of KA exclusively, the least solution that is constructed is the same for both BKA and CKA.

**Lemma 3.12.** *Let* L *be an* I*-linear system. One can construct a single* I*vector* x *that is the least solution to* L *in both* BKA *and* CKA*.*

We include a full proof of the lemma above using the notation of this paper in the full version of this paper [15].

### **4 Completeness of CKA**

We now turn our attention to proving that ≡CKA is complete for CKA-semantic equivalence of terms, i.e., that if e, f ∈ T are such that eCKA = fCKA, then e ≡CKA f. In the interest of readability, proofs of technical lemmas in this section can be found in the full version of this paper [15].

As mentioned before, our proof of completeness is based on the completeness result for BKA reproduced in Theorem 3.1. Recall that eCKA = eBKA↓. To reuse completeness of BKA, we construct a syntactic variant of the closure operator, which is formalised below.

**Definition 4.1.** *Let* e ∈ T *. We say that* e↓ *is a* closure *of* e *if both* e ≡CKA e↓ *and* e↓BKA = eBKA↓ *hold.*

*Example 4.1.* Let e = a b; as proposed in Sect. 2, we claim that e↓ = a - b+b·a+a·b is a closure of e. To see why, first note that e -CKA e↓ by construction. Furthermore,

> ab ≡CKA (a - 1) · (1 b) -CKA (a · 1) - (1 · b) ≡CKA a b

and similarly ba -CKA e; thus, e ≡CKA e↓. Lastly, the pomsets in eBKA↓ and e↓BKA are simply a b, ab and ba, and therefore e↓BKA = eBKA↓.

Laurence and Struth observed that the existence of a closure for every term implies a completeness theorem for CKA, as follows.

**Lemma 4.1.** *Suppose that we can construct a closure for every element of* T *. If* e, f ∈ T *such that* eCKA = fCKA*, then* e ≡CKA f*.*

*Proof.* Since eCKA = eBKA↓ = e↓BKA and similarly fCKA = f↓BKA, we have e↓BKA = f↓BKA. By Theorem 3.1, we get e↓ ≡BKA f↓, and thus e↓ ≡CKA f↓, since all axioms of BKA are also axioms of CKA. By e ≡CKA e↓ and f↓ ≡CKA f, we can then conclude that e ≡CKA f.

The remainder of this section is dedicated to showing that the premise of Lemma 4.1 holds. We do this by explicitly constructing a closure e↓ for every e ∈ T . First, we note that closure can be constructed for the base terms.

**Lemma 4.2.** *Let* e ∈ 2 *or* e = a *for some* a ∈ Σ*. Then* e *is a closure of itself.*

Furthermore, closure can be constructed compositionally for all operators except parallel composition, in the following sense.

**Lemma 4.3.** *Suppose that* e0, e1 ∈ T *, and that* e0 *and* e1 *have closures* e0↓ *and* e1↓*. Then (i)* e0↓+e1↓ *is a closure of* e0 +e1*, (ii)* e0↓ · e1↓ *is a closure of* e0 · e1*, and (iii)* (e0↓) *is a closure of* e- 0*.*

*Proof.* Since e0↓ ≡CKA e0 and e1↓ ≡CKA e1, by the fact that ≡CKA is a congruence we obtain e0↓ + e1↓ ≡CKA e0 + e1. Similar observations hold for the other operators. We conclude using Lemma 3.7.

It remains to consider the case where e = e0 e1. In doing so, our induction hypothesis is that any f ∈ T with |f| < |e0 e1| has a closure, as well as any strict subterm of e0 e1.

### **4.1 Preclosure**

To get to a closure of a parallel composition, we first need an operator on terms that is not a closure quite yet, but whose BKA-semantics is "closed enough" to cover the non-sequential elements of the CKA-semantics of the term.

**Definition 4.2.** *Let* e ∈ T *. A* preclosure *of* e *is a term* e˜ ∈ T *such that* e˜ ≡CKA e*.  Suppose that e0 e1 = (a b) c. A preclosure of e0 e1 could be

$$\tilde{e} = a \parallel b \parallel c + (a \cdot b + b \cdot a) \parallel c + (b \cdot c + c \cdot b) \parallel a + (a \cdot c + c \cdot a) \parallel b$$

To verify this, note that e -CKA e˜ by construction; remains to show that ˜e -CKA e. This is fairly straightforward: since a·b+b·a -CKA a b, we have (a·b+b·a) c -CKA e; the other terms are treated similarly. Consequently, e ≡CKA e˜. Furthermore, there are seven non-sequential pomsets in eCKA; they are

a b c ab c ba c bc a cb a ac b ca b

Each of these pomsets is found in e˜BKA. It should be noted that ˜e is *not* a closure of e; to see this, consider for instance that abc ∈ eCKA, while abc ∈ e˜BKA.

The remainder of this section is dedicated to showing that, under the induction hypothesis, we can construct a preclosure for any parallelly composed term. This is not perfectly straightforward; for instance, consider the term e0 e1 discussed in Example 4.2. At first glance, one might be tempted to choose e0↓ e1↓ as a preclosure, since e0↓ and e1↓ exist by the induction hypothesis. In that case, e0↓ = a b+a · b+b · a is a closure of e0. Furthermore, e1↓ = c is a closure of e1, by Lemma 4.2. However, e0↓ e1↓ is not a preclosure of e0 e1, since (a · c) b is non-sequential and found in e0 e1CKA, but not in e0↓ e1↓BKA.

The problem is that the preclosure of e0 and e1 should also allow (partial) sequentialisation of *parallel parts* of e0 and e1; in this case, we need to sequentialise the a part of a b with c, and leave b untouched. To do so, we need to be able to *split* e0 e1 into pairs of constituent terms, each of which represents a possible way to divvy up its parallel parts. For instance, we can split e0 e1 = (a b) c parallelly into a b and c, but also into a and b c, or into a c and b. The definition below formalises this procedure.

**Definition 4.3.** *Let* e ∈ T *;* Δe *is the smallest relation on* T *such that*

$$\begin{array}{ccccc}\hline\hline\frac{1}{1}\,\Delta\_{e}\,e &\stackrel{\begin{subarray}{c}\ell\end{subarray}}{\ell\end{subarray}}{e\,\bigtriangleup\_{e}\,1} &\stackrel{\begin{subarray}{c}\ell\,\Delta\_{e\_{0}}\,r\\\ell\,\Delta\_{e\_{1}+e\_{0}}\,r\end{subarray}}{\ell\,\Delta\_{e\_{1}+e\_{0}}\,r} &\stackrel{\begin{subarray}{c}\ell\,\Delta\_{e\_{1}}\,r\\\ell\,\Delta\_{e\_{0}+e\_{1}}\,r\end{subarray}}{\ell\,\Delta\_{e\_{0}+e\_{1}}\,r} &\stackrel{\begin{subarray}{c}\ell\,\Delta\_{e\_{1}}\,r\\\ell\,\Delta\_{e\_{0}+e\_{1}}\,r\end{subarray}}{\ell\,\Delta\_{e\_{0}}\,r}\\\hline\hline\end{array}\\\begin{array}{ccccc}\begin{array}{ccccc}\ell\,\Delta\_{e}\,r\\\ell\,\Delta\_{e\_{1}}\,r\\\ell\,\Delta\_{e\_{0}}\,r\end{array}\\\&\begin{array}{c}\ell\,\Delta\_{e\_{1}}\,r\\\ell\,\Delta\_{e\_{0}}\,r\end{array}\\\hline\end{array}$$

Given e ∈ T , we refer to Δe as the *parallel splitting relation* of e, and to the elements of Δe as *parallel splices* of e. Before we can use Δe to construct the preclosure of e, we go over a number of properties of the parallel splitting relation. The first of these properties is that a given e ∈ T has only finitely many parallel splices. This will be useful later, when we involve *all* parallel splices of e in building a new term, i.e., to guarantee that the constructed term is finite.

### **Lemma 4.4.** *For* e ∈ T *,* Δe *is finite.*

We furthermore note that the parallel composition of any parallel splice of e is ordered below e by -BKA. This guarantees that parallel splices never contain extra information, i.e., that their semantics do not contain pomsets that do not occur in the semantics of e. It also allows us to bound the width of the parallel splices by the width of the term being split, as a result of Lemma 3.10.

#### **Lemma 4.5.** *Let* e ∈ T *. If* Δe r*, then* r -BKA e*.*

**Corollary 4.1.** *Let* e ∈ T *. If* Δe r*, then* || + |r|≤|e|*.*

Finally, we show that Δe is *dense* when it comes to parallel pomsets, meaning that if we have a parallelly composed pomset in the semantics of e, then we can find a parallel splice where one parallel component is contained in the semantics of one side of the pair, and the other component in that of the other.

**Lemma 4.6.** *Let* e ∈ T *, and let* V,W *be pomsets such that* V - W ∈ eBKA*. Then there exist* , r ∈ T *with* Δe r *such that* V ∈ -BKA *and* W ∈ rBKA*.*

*Proof.* The proof proceeds by induction on e. In the base, we can discount the case where e = 0, for then the claim holds vacuously. This leaves us two cases.

For the inductive step, there are four cases to consider.

	- Suppose that Ui = 1 for some i ∈ 2, meaning that V - W = U0 · U1 = U1−i ∈ e1−iBKA for this i. By induction, we find , r ∈ T with Δe1−i r, and V ∈ -BKA as well as W ∈ rBKA. Since Ui = 1 ∈ eiBKA, we have that (ei) = 1 by Lemma 3.9, and thus Δe r.
	- Suppose that V = 1 or W = 1. In the former case, V - W = W = U0 · U1 ∈ eCKA. We then choose = 1 and r = e to satisfy the claim. In the latter case, we can choose = e and r = 1 to satisfy the claim analogously.

If n > 0, we can assume without loss of generality that, for 0 ≤ i<n, it holds that Ui = 1. By Lemma 3.1, there are two subcases to consider.

• Suppose that V,W = 1; then n = 1 (for otherwise Uj = 1 for some 0 ≤ j<n by Lemma 3.1, which contradicts the above). Since V - W = U0 ∈ e0BKA, we find by induction , r ∈ T with Δe0 r such that V ∈ -BKA and W ∈ rBKA. The claim then follows by the fact that Δe r. • Suppose that V = 1 or W = 1. In the former case, V - W = W = U0 · U1 ···Un−1 ∈ eCKA. We then choose = 1 and r = e to satisfy the claim. In the latter case, we can choose = e and r = 1 to satisfy the claim analogously.

*Example 4.3.* Let U = a c and V = b, and note that U - V ∈ e0 e1CKA. We can then find that a Δa 1 and 1 Δb b, and thus a - 1 Δe0 1 b. Since also c Δc 1, it follows that (a - 1) c Δe0e1 (1 b) - 1. We can then choose = (a - 1) c and r = (1 b) - 1 to find that U ∈ -BKA and V ∈ rBKA, while Δe0e1 r.

With parallel splitting in hand, we can define an operator on terms that combines all parallel splices of a parallel composition in a way that accounts for all of their downward closures.

**Definition 4.4.** *Let* e, f ∈ T *, and suppose that, for every* g ∈ T *such that* |g| < |e| + |f|*, there exists a closure* g↓*. The term* e f *is defined as follows:*

$$e \odot f \stackrel{\Delta}{=} e \parallel f + \sum\_{\substack{\ell \Delta\_{e \parallel f} r \\ |\ell|, |r| < |e||f|}} \ell \downarrow \parallel r \downarrow$$

Note that ef is well-defined: the sum is finite since Δef is finite by Lemma 4.4, and furthermore ↓ and r↓ exist, as we required that ||, |r| < |e f|.

*Example 4.4.* Let us compute e0 e1 and verify that we obtain a preclosure of e0 e1. Working through the definition, we see that Δe0e1 consists of the pairs

Since closure is invariant with respect to ≡CKA, we can simplify these terms by applying the axioms of CKA. After folding the unit subterms, we are left with

$$\langle 1, a \parallel b \parallel c \rangle \qquad \langle c, a \parallel b \rangle \qquad \langle b, a \parallel c \rangle \qquad \langle b \parallel c, a \rangle \qquad \langle a, b \parallel c \rangle \qquad \langle a \parallel c, b \rangle$$

Recall that a b + a · b + b · a is a closure of a b. Now, we find that

$$\begin{aligned} e\_0 \odot e\_1 &= (a \parallel b) \parallel c + c \parallel (a \parallel b + a \cdot b + b \cdot a) \\ &+ b \parallel (a \parallel c + a \cdot c + c \cdot a) + (b \parallel c + b \cdot c + c \cdot b) \parallel a \\ &+ a \parallel (b \parallel c + b \cdot c + c \cdot b) + (a \parallel c + a \cdot c + c \cdot a) \parallel b \\ \equiv\_{c \ltimes a} a \parallel b \parallel c + a \parallel (b \cdot c + c \cdot b) + b \parallel (a \cdot c + c \cdot a) + c \parallel (a \cdot b + b \cdot a) \end{aligned}$$

which was shown to be a preclosure of e0 e1 in Example 4.2.

The general proof of correctness for as a preclosure plays out as follows.

**Lemma 4.7.** *Let* e, f ∈ T *, and suppose that, for every* g ∈ T *with* |g| < |e|+|f|*, there exists a closure* g↓*. Then* e f *is a preclosure of* e f*.*

*Proof.* We start by showing that ef ≡CKA e f. First, note that e f -BKA ef by definition of ef. For the other direction, suppose that , r ∈ T are such that Δef r. By definition of closure, we know that ↓ r↓ ≡CKA r. By Lemma 4.5, we have r -BKA e f. Since every subterm of ef is ordered below e f by -CKA, we have that e f -CKA e f. It then follows that e f ≡CKA e f.

For the second requirement, suppose that X ∈ e fCKA is non-sequential. We then know that there exists a Y ∈ e fBKA such that X Y . This leaves us two cases to consider.

This means that ↓ r↓ -BKA e f. Since X0 ∈ -↓BKA and X1 ∈ r↓BKA by definition of closure, we can derive by Lemma 3.8 that

$$X = X\_0 \parallel X\_1 \in \left[ \ell \downarrow \parallel r \downarrow \right]\_{\mathsf{BKA}} \subseteq \left[ e \odot f \right]\_{\mathsf{BKA}} \tag{7}$$

#### **4.2 Closure**

The preclosure operator discussed above covers the non-sequential pomsets in the language e fCKA; it remains to find a term that covers the sequential pomsets contained in e fCKA.

To better give some intuition to the construction ahead, we first explore the observations that can be made when a sequential pomset W · X appears in the language e fCKA; without loss of generality, assume that W is nonsequential. In this setting, there must exist U ∈ eBKA and V ∈ fBKA such that W · X U -V . By Lemma 3.6, we find pomsets U0, U1, V0, V1 such that

$$W \subseteq U\_0 \parallel V\_0 \qquad \qquad X \subseteq U\_1 \parallel V\_1 \qquad \qquad U\_0 \cdot U\_1 \subseteq U \qquad \qquad V\_0 \cdot V\_1 \subseteq V$$

This means that U0 · U1 ∈ eCKA and V0 · V1 ∈ fCKA. Now, suppose we could find e0, e1, f0, f1 ∈ T such that

$$\begin{array}{ccccc} e\_0 \cdot e\_1 \leq\_{\mathsf{C\mathsf{A}}\mathsf{A}} e & & U\_0 \in \left[e\_0\right]\_{\mathsf{C\mathsf{A}}} & & U\_1 \in \left[e\_1\right]\_{\mathsf{C\mathsf{A}}}, \\\\ f\_0 \cdot f\_1 \leq\_{\mathsf{c\mathsf{A}}\mathsf{A}} f & & V\_0 \in \left[f\_0\right]\_{\mathsf{C\mathsf{A}}} & & V\_1 \in \left[f\_1\right]\_{\mathsf{C\mathsf{A}}}. \end{array}$$

Then we have W ∈ e0 f0BKA, and X ∈ e1 f1CKA. Thus, if we can find a closure of e1 f1, then we have a term whose BKA-semantics contains W · X.

There are two obstacles that need to be resolved before we can use the observations above to find the closure of e f. The first problem is that we need to be sure that this process of splitting terms into sequential components is at all possible, i.e., that we can split e into e0 and e1 with e0 ·e1 -CKA e and Ui ∈ eiCKA for i ∈ 2. We do this by designing a sequential analogue to the parallel splitting relation seen before. The second problem, which we will address later in this section, is whether this process of splitting a parallel term e f according to the exchange law and finding a closure of remaining term e1 f1 is well-founded, i.e., if we can find "enough" of these terms to cover all possible ways of sequentialising e f. This will turn out to be possible, by using the fixpoint axioms of KA as in Sect. 3.3 with linear systems.

We start by defining the sequential splitting relation.3

**Definition 4.5.** *Let* e ∈ T *;* ∇e *is the smallest relation on* T *such that*

$$
\begin{array}{ccccccccc}
\hline
\overline{1\,\nabla\_{1}1} & \overline{a\,\nabla\_{a}1} & \overline{1\,\nabla\_{a}a} & \overline{1\,\nabla\_{a}a} & \overline{1\,\nabla\_{e\_{0}^{\*}}1} & \overline{\ell\,\nabla\_{e\_{0}+e\_{1}}r} & \overline{\ell\,\nabla\_{e\_{0}+e\_{1}}r} \\
\hline
\ell\,\nabla\_{e\_{0}\,{}^{c}}\,\boldsymbol{r} & & & & \ell\_{0}\,\nabla\_{e\_{0}\,{}^{c}}\,\boldsymbol{r} & \\
\hline
\ell\,\nabla\_{e\_{0}\,{}^{c}}\,\boldsymbol{r}\,\boldsymbol{r}\,\boldsymbol{e}\_{1} & & & \ell\_{0}\,\ell\,\nabla\_{e\_{0}\,{}^{c}}\,\boldsymbol{r} & \overline{\ell\,\nabla\_{e\_{0}}\,\boldsymbol{r}} & \overline{\ell\,\nabla\_{e\_{0}}\,\boldsymbol{r} \\
\hline
\end{array}
$$

Given e ∈ T , we refer to ∇e as the *sequential splitting relation* of e, and to the elements of ∇e as *sequential splices* of e. We need to establish a few properties of the sequential splitting relation that will be useful later on. The first of these properties is that, as for parallel splitting, ∇e is finite.

### **Lemma 4.8.** *For* e ∈ T *,* ∇e *is finite.*

We also have that the sequential composition of splices is provably below the term being split. Just like the analogous lemma for parallel splitting, this guarantees that our sequential splices never give rise to semantics not contained in the split term. This lemma also yields an observation about the width of sequential splices when compared to the term being split.

**Lemma 4.9.** *Let* e ∈ T *. If* , r ∈ T *with* ∇e r*, then* · r -CKA e*.*

**Corollary 4.2.** *Let* e ∈ T *. If* , r ∈ T *with* ∇e r*, then* ||, |r|≤|e|*.*

Lastly, we show that the splices cover every way of (sequentially) splitting up the semantics of the term being split, i.e., that ∇e is dense when it comes to sequentially composed pomsets.

**Lemma 4.10.** *Let* e ∈ T *, and let* V *and* W *be pomsets such that* V ·W ∈ eCKA*. Then there exist* , r ∈ T *with* ∇e r *such that* V ∈ -CKA *and* W ∈ rCKA*.*

*Proof.* The proof proceeds by induction on e. In the base, we can discount the case where e = 0, for then the claim holds vacuously. This leaves us two cases.

3 The contents of this relation are very similar to the set of *left- and right-spines* of a NetKAT expression as used in [5].

For the inductive step, there are four cases to consider.

For the case where n > 0, we find by Lemma 3.4 an 0 ≤ m<n and seriesparallel pomsets X, Y such that X · Y Um, and V U0 · U1 ···Um−1 · X and W Y · Um+1 · Um+2 ···Un. Since X · Y Um ∈ e0CKA and thus X · Y ∈ e0CKA, we find by induction , r ∈ T with ∇e0 r and X ∈ - CKA and Y ∈ r CKA. We can then choose = e- 0 · and r = r · e- 0 to find that V U0 ·U1 ···Um−1 ·X ∈ e- 0CKA ·- CKA = -CKA and W Y ·Um+1 ·Um+2 ···Un ∈ r CKA ·e- 0CKA = rCKA, and thus that V ∈ -CKA and W ∈ rCKA. Since ∇e r holds, the claim follows.

*Example 4.5.* Let U be the pomset ca and let V be bc. Furthermore, let e be the term (a · b + c) - , and note that U · V ∈ eCKA. We then find that a ∇a 1, and thus a ∇a·b 1 · b. We can now choose = (a · b + c) - · a and r = (1 · b)·(a · b + c) - to find that U ∈ -CKA and V ∈ rCKA, while ∇e r.

We know how to split a term sequentially. To resolve the second problem, we need to show that the process of splitting terms repeatedly ends somewhere. This is formalised in the notion of *right-hand remainders*, which are the terms that can appear as the right hand of a sequential splice of a term.

**Definition 4.6.** *Let* e ∈ T *. The set of* (right-hand) remainders *of* e*, written* R(e)*, is the smallest satisfying the rules*

$$\overline{e \in R(e)} \qquad \qquad \qquad \frac{f \in R(e) \qquad \ell \,\,\nabla\_f \,\, r}{r \in R(e)}$$

**Lemma 4.11.** *Let* e ∈ T *.* R(e) *is finite.*

With splitting and remainders we are in a position to define the linear system that will yield the closure of a parallel composition. Intuitively, we can think of this system as an automaton: every variable corresponds to a state, and every row of the matrix describes the "transitions" of the corresponding state, while every element of the vector describes the language "accepted" by that state without taking a single transition. Solving the system for a least fixpoint can be thought of as finding an expression that describes the language of the automaton.

**Definition 4.7.** *Let* e, f ∈ T *, and suppose that, for every* g ∈ T *such that* |g| < |e| + |f|*, there exists a closure* g↓*. We choose*

$$I\_{e,f} = \{ g \parallel h : g \in R(e), h \in R(f) \}$$

*The* Ie,f *-vector* pe,f *and* Ie,f *-matrix* Me,f *are chosen as follows.*

$$\begin{aligned} \, \_p p\_{e,f}(g \parallel h) \triangleq g \parallel f & \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \, \_{\ell\_g \nabla\_g g'} \, \_{g} \, \_{h} \odot \, \_{h} \, \_{h} \end{aligned}$$

Ie,f *is finite by Lemma 4.11. We write* Le,f *for the* Ie,f *-linear system* Me,f , pe,f *.*

We can check that Me,f is well-defined. First, the sum is finite, because ∇g and ∇h are finite by Lemma 4.8. Second, if g h ∈ I and g, rg, h, rh ∈ T such that g ∇g rg and h ∇h rh, then |g|≤|g|≤|e| and |h|≤|h|≤|f| by Corollary 4.2, and thus, if d ∈ T such that |d| < |g| + |h|, then |d| < |e| + |f|, and therefore a closure of d exists, meaning that g h exists, too.

The least solution to Le,f obtained through Lemma 3.12 is the I-vector denoted by se,f . We write e ⊗ f for se,f (e f), i.e., the least solution at e f.

Using the previous lemmas, we can then show that e ⊗ f is indeed a closure of e f, provided that we have closures for all terms of strictly lower width. The intuition of this proof is that we use the uniqueness of least fixpoints to show that e f ≡CKA e ⊗ f, and then use the properties of preclosure and the normal form of series-parallel pomsets to show that e fCKA = e ⊗ fBKA.

**Lemma 4.12.** *Let* e, f ∈ T *, and suppose that, for every* g ∈ T *with* |g| < |e| + |f|*, there exists a closure* g↓*. Then* e ⊗ f *is a closure of* e f*.*

*Proof.* We begin by showing that e f ≡CKA e ⊗ f. We can see that pe,f is a solution to Le,f , by calculating for g h ∈ Ie,f :

$$\begin{array}{ll} (p\_{e,f} + M\_{e,f} \cdot p\_{e,f})(g \parallel h) \\ = g \parallel h + \sum\_{r\_g \parallel r\_h \in I} \left( \sum\_{\substack{\ell\_g \nabla\_g r\_g \\ \ell\_h \nabla\_h r\_h \end{array}} \ell\_g \odot \ell\_h \right) \cdot (r\_g \parallel r\_h) \\ \tag{\text{def. } M\_{e,f}, p\_{e,f})} \\ = \\ \end{array}$$

$$\equiv\_{\mathsf{C\mathsf{A}}} g \parallel h + \sum\_{\substack{\ell\_{\mathsf{g}} \parallel r\_{h} \in I \\ \ell\_{h} \in \nabla\_{g} r\_{\mathcal{g}}}} \sum\_{\substack{\ell\_{\mathcal{g}} \in \nabla\_{g} r\_{\mathcal{g}} \\ \ell\_{h} \in \nabla\_{h} r\_{h}}}^{\ell\_{h} \nabla\_{h} r\_{\mathcal{g}}} (\ell\_{g} \odot \ell\_{h}) \cdot (r\_{g} \parallel r\_{h}) \tag{distributivity}$$

$$\equiv\_{\mathsf{CAK}} g \parallel h + \sum\_{\substack{r\_h \parallel r\_h \in I \\ r\_h \parallel r\_h}} \sum\_{\substack{\ell\_g \in \nabla\_g r\_g \\ \ell\_h \nabla\_h r\_h}}^{\ell\_h \text{-} \{\ell\_g\}} (\ell\_g \parallel \ell\_h) \cdot (r\_g \parallel r\_h) \tag{1.2.12}$$

$$\leq\_{\mathsf{co\\_o}} g \parallel h + \sum\_{\substack{r\_g \parallel r\_h \in I \ l\_g}} \sum\_{\substack{\ell\_g \nabla\_g r\_g \\ \ell\_h \nabla\_h r\_h}}^{\ell\_h \nabla\_h r\_h} (\ell\_g \cdot r\_g) \parallel (\ell\_h \cdot r\_h) \tag{exchange}$$

$$\leq\_{\mathsf{C@A}} g \parallel h + \sum\_{\substack{r\_g \parallel r\_h \in I \\ \ell\_h \nabla\_h r\_h}} \sum\_{g \parallel h}^{\ell\_h \nabla\_h r\_h} g \parallel h \tag{\text{Lemma 4.9}}$$

$$\begin{array}{ll} \equiv\_{\mathsf{Coka}} g \parallel h & & \text{(idempotence)}\\ = p\_{e,f}(g \parallel h) & & \text{(def. } p\_{e,f}) \end{array}$$

To see that pe,f is the *least* solution to Le,f , let qe,f be a solution to Le,f . We then know that Me,f · qe,f + pe,f -CKA qe,f ; thus, in particular, pe,f -CKA qe,f . Since the least solution to a linear system is unique up to ≡CKA, we find that se,f ≡CKA pe,f , and therefore that e ⊗ f = se,f (e f) ≡CKA pe,f (e f) = e f.

It remains to show that if U ∈ e fCKA, then U ∈ e ⊗ fBKA. To show this, we show the more general claim that if g h ∈ I and U ∈ g hCKA, then U ∈ se,f (g h)BKA. Write U = U0 · U1 ···Un−1 such that for 0 ≤ i<n, Ui is non-sequential (as in Corollary 3.1). The proof proceeds by induction on n. In the base, we have that n = 0. In this case, U = 1, and thus U ∈ g hBKA by Lemma 3.2. Since g h = pe,f (g h) -BKA se,f (g h), it follows that U ∈ se,f (g h)BKA by Lemma 3.8.

For the inductive step, assume the claim holds for n−1. We write U = U0 ·U , with U = U1 · U2 ···Un−1. Since U0 · U ∈ g hCKA, there exist W ∈ gCKA and X ∈ hCKA such that U0 · U W - X. By Lemma 3.6, we find pomsets W0, W1, X0, X1 such that W0·W1 W and X0·X1 X, as well as U0 W0 - X0 and U W1 - X1. By Lemma 4.10, we find g, rg, h, rh ∈ T with g ∇g rg and h ∇h rh, such that W0 ∈ gCKA, W1 ∈ rgCKA, X0 ∈ hCKA and X1 ∈ rhCKA.

From this, we know that U0 ∈ g hCKA and U ∈ rg rhCKA. Since U0 is non-sequential, we have that U0 ∈ g hBKA. Moreover, by induction we find that U ∈ se,f (rg rh)BKA. Since g h -BKA Me,f (g h, rg rh) by definition of Me,f , we furthermore find that

$$(\ell\_g \odot \ell\_h) \cdot s\_{e,f}(r\_g \parallel r\_h) \leq\_{\mathsf{BAK}} M\_{e,f}(g \parallel h, r\_g \parallel r\_h) \cdot s\_{e,f}(r\_g \parallel r\_h)$$

Since rg rh ∈ I, we find by definition of the solution to a linear system that

$$M\_{e,f}(g \parallel h, r\_g \parallel r\_h) \cdot s\_{e,f}(r\_g \parallel r\_h) \stackrel{\leq}{\equiv} s\_{\texttt{e\\_f}}(g \parallel h)$$

By Lemma 3.8 and the above, we conclude that U = U0 · U ∈ se,f (g h)BKA.

For a concrete example where we find a closure of a (non-trivial) parallel composition by solving a linear system, we refer to Appendix A.

With closure of parallel composition, we can construct a closure for any term and therefore conclude completeness of CKA.

**Theorem 4.1.** *Let* e ∈ T *. We can construct a closure* e↓ *of* e*.*

*Proof.* The proof proceeds by induction on |e| and the structure of e, i.e., by considering f before g if |f| < |g|, or if f is a strict subterm of g (in which case |f|≤|g| also holds). It is not hard to see that this induces a well-ordering on T .

Let e be a term of width n, and suppose that the claim holds for all terms of width at most n − 1, and for all strict subterms of e. There are three cases.

**Corollary 4.3.** *Let* e, f ∈ T *. If* eCKA = fCKA*, then* e ≡CKA f*.*

*Proof.* Follows from Theorem 4.1 and Lemma 4.1.

### **5 Discussion and Further Work**

By building a syntactic closure for each series-rational expression, we have shown that the standard axiomatisation of CKA is complete with respect to the CKAsemantics of series-rational terms. Consequently, the algebra of closed seriesrational pomset languages forms the free CKA.

Our result leads to several decision procedures for the equational theory of CKA. For instance, one can compute the closure of a term as described in the present paper, and use an existing decision procedure for BKA [3,12,20]. Note however that although this approach seems suited for theoretical developments (such as formalising the results in a proof assistant), its complexity makes it less appealing for practical use. More practically, one could leverage recent work by Brunet et al. [3], which provides an algorithm to compare closed series-rational pomset languages. Since this is the free concurrent Kleene algebra, this algorithm can now be used to decide the equational theory of CKA. We also obtain from the latter paper that this decision problem is expspace-complete.

We furthermore note that the algorithm to compute downward closure can be used to extend half of the result from [14] to a Kleene theorem that relates the CKA-semantics of expressions to the pomset automata proposed there: if e ∈ T , we can construct a pomset automaton A with a state q such that LA(q) = eCKA.

Having established pomset automata as an operational model of CKA, a further question is whether these automata are amenable to a bisimulation-based equivalence algorithm, as is the case for finite automata [10]. If this is the case, optimisations such as those in [2] might have analogues for pomset automata that can be found using the coalgebraic method [23].

While this work was in development, an unpublished draft by Laurence and Struth [19] appeared, with a first proof of completeness for CKA. The general outline of their proof is similar to our own, in that they prove that closure of pomset languages preserves series-rationality, and hence there exists a syntactic closure for every series-rational expression. However, the techniques used to establish this fact are quite different from the developments in the present paper. First, we build the closure via syntactic methods: explicit splitting relations and solutions of linear systems. Instead, their proof uses automata theoretic constructions and algebraic closure properties of regular languages; in particular, they rely on congruences of finite index and language homomorphisms. We believe that our approach leads to a substantially simpler and more transparent proof. Furthermore, even though Laurence and Struth do not seem to use any fundamentally non-constructive argument, their proof does not obviously yield an algorithm to effectively compute the closure of a given term.

A crucial ingredient in this work was the computation of least solutions of linear systems. This kind of construction has been used on several occasions for the study of Kleene algebras [1,4,18], and we provide here yet another variation of such a result. We feel that linear systems may not have yet been used to their full potential in this context, and could still lead to interesting developments.

A natural extension of the work conducted here would be to turn our attention to the signature of concurrent Kleene algebra that includes a "parallel star" operator e. The completeness result of Laurence and Struth [20] holds for BKA with the parallel star, so in principle one could hope to extend our syntactic closure construction to include this operator. Unfortunately, using the results of Laurence and Struth, we can show that this is not possible. They defined a notion of *depth* of a series-parallel pomset, intuitively corresponding to the nesting of parallel and sequential components. An important step in their development consists of proving that for every series-parallel-rational language there exists a finite upper bound on the depth of its elements. However, the language a CKA does not enjoy this property: it contains every series-parallel pomset exclusively labelled with the symbol a. Since we can build such pomsets with arbitrary depth, it follows that there does not exist a syntactic closure of the term a. New methods would thus be required to tackle the parallel star operator.

Another aspect of CKA that is not yet developed to the extent of KA is the coalgebraic perspective. We intend to investigate whether the coalgebraic tools developed for KA can be extended to CKA, which will hopefully lead to efficient bisimulation-based decision procedures [2,5].

**Acknowledgements.** We thank the anonymous reviewers for their insightful comments. This work was partially supported by the ERC Starting Grant ProFoundNet (grant code 679127).

### **A Worked Example: A Non-trivial Closure**

In this appendix, we solve an instance of a linear system as defined in Definition 4.7 for a given parallel composition. For the sake of brevity, the steps are somewhat coarse-grained; the reader is encouraged to reproduce the steps by hand.

Consider the expression e f = a∗ b. The linear system Le,f that we obtain from this expression consists of six inequations; in matrix form (with zeroes omitted), this system is summarised as follows:4

$$\begin{array}{c||c c c c c c} & 1 & 1 & 1 & & & & & & 1 \\ & 1 & \mid & b & & & & & & & & \\ a \cdot a^\* \mid & 1 & & & & & & & & & \\ a^\* \mid 1 & & & & & & & & & & \\ a \cdot a^\* \mid & b & & & & & & & & \\ a \cdot a^\* \mid & b & & & & & & & & \\ a^\* \mid & b & & & & & & & & \\ \end{array} \begin{array}{c|c|c} & 1 & & & & & & & & \\ a & & & & & & & & & \\ a \cdot a^\* \mid & b & & & & & \\ a^\* \mid & a^\* \mid & b & & & & \\ a \cdot a^\* \mid & b & & & & & \\ b & 1 & a^\* \mid & b & & & \\ \end{array} \begin{array}{c|c|c} & 1 & & & & & & \\ a \cdot a^\* \mid & b & & & & \\ a \cdot a^\* \mid & b & & & & \\ a \cdot a^\* \mid & b & & & & \\ a \cdot a^\* \mid & b & & & & \\ \end{array} \end{array}$$

Let us proceed under the assumption that x is a solution to the system; the constraint imposed on x by the first two rows is given by the inequations

$$x(1 \parallel 1) + 1 \stackrel{<}{=}\_{c \bowtie \mathsf{A}} x(1 \parallel 1) \tag{1}$$

$$a \cdot x(1 \parallel 1) + x(1 \parallel b) + b \leq\_{c \bowtie \kappa} x(1 \parallel b) \tag{2}$$

Because these inequations do not involve the other positions of the system, we can solve them in isolation, and use their solutions to find solutions for the remaining positions; it turns out that choosing x(1 - 1) = 1 and x(1 b) = b suffices here.

We carry on to fill these values into the inequations given by the third and fourth row of the linear system. After some simplification, these work out to be

$$a \cdot a^\star + a \cdot a^\star \cdot x(a^\star \parallel 1) + a^\star \cdot x(a \cdot a^\star \parallel 1) \stackrel{\le}{=}\_{\mathsf{csca}} x(a \cdot a^\star \parallel 1) \tag{3}$$

$$a^\star + a^\star \cdot a \cdot x(a^\star \parallel 1) + a^\star \cdot x(a \cdot a^\star \parallel 1) \le\_{c\star\star} x(a^\star \parallel 1)\tag{4}$$

Applying the least fixpoint axiom to (3) and simplifying, we obtain

$$a \cdot a^\star + a \cdot a^\star \cdot x(a^\star \parallel 1) \le\_{\text{c\'\'\'\text{c\'\'}}} x(a \cdot a^\star \parallel 1) \tag{5}$$

Substituting this into (4) and simplifying, we find that

$$a^\star + a \cdot a^\star \cdot x(a^\star \parallel 1) \le\_{\text{c\'\'a\'}} x(a^\star \parallel 1) \tag{6}$$

This inequation, in turn, gives us that a- -CKA x(a- - 1) by the least fixpoint axiom. Plugging this back into (3) and simplifying, we find that

$$a \cdot a^\star + a^\star \cdot x(a \cdot a^\star \parallel 1) \stackrel{\le}{=}\_{\mathsf{c}\ltimes} x(a \cdot a^\star \parallel 1)\tag{7}$$

4 Actually, the system obtained from *a*- *b* as a result of Definition 4.7 is slightly larger; it also contains rows and columns labelled by 1 · *a*- - 1 and 1 · *a*- *b*; these turn out to be redundant. We omit these rows from the example for simplicity.

Again by the least fixpoint axiom, this tells us that a · a- -CKA x(a · a- - 1). One easily checks that x(a · a- - 1) = a · a and x(a- - 1) = a are solutions to (3) and (4); by the observations above, they are also the least solutions.

It remains to find the least solutions for the final two positions. Filling in the values that we already have, we find the following for the fifth row:

$$\begin{aligned} &a \parallel b + a \cdot b + (a^\star \parallel b) \cdot a \cdot a^\star + (a \cdot a^\star \parallel b) \cdot a^\star \\ &+ a^\star \cdot x (a \cdot a^\star \parallel b) + a \cdot a^\star \cdot x (a^\star \parallel b) + a \cdot a^\star \parallel b \stackrel{\triangle}{=}\_{\mathsf{csca}} x (a \cdot a^\star \parallel b) \end{aligned} \tag{8}$$

Applying the exchange law5 to the first three terms, we find that they are contained in (a · a- b) · a-, as is the last term; (8) thus simplifies to

$$x(a \cdot a^\star \parallel b) \cdot a^\star + a^\star \cdot x(a \cdot a^\star \parallel b) + a \cdot a^\star \cdot x(a^\star \parallel b) \stackrel{\leftarrow}{=} \text{c\upharpoonright x}(a \cdot a^\star \parallel b) \tag{9}$$

By the least fixpoint axiom, we find that

$$a^\star \cdot (a \cdot a^\star \parallel b) \cdot a^\star + a \cdot a^\star \cdot x(a^\star \parallel b) \leq\_{\text{c\'\'a\'}} x(a \cdot a^\star \parallel b) \tag{10}$$

For the sixth row, we find that after filling in the solved positions, we have

$$\begin{aligned} \label{eq:SDAC-1} b &+ b + \begin{pmatrix} a^\star \parallel b \end{pmatrix} \cdot a \cdot a^\star + \begin{pmatrix} a \cdot a^\star \parallel b \end{pmatrix} \cdot a^\star \\ &+ a^\star \cdot x(a \cdot a^\star \parallel b) + a \cdot a^\star \cdot x(a^\star \parallel b) + a^\star \parallel b \stackrel{\leftharpoons}{\underset{c \in \mathbb{K}}{\rightleftharpoons}} x(a^\star \parallel b) \end{aligned} \tag{11}$$

Simplifying and applying the exchange law as before, it follows that

$$x(a^\star \parallel b) \cdot a^\star + a^\star \cdot x(a \cdot a^\star \parallel b) + a \cdot a^\star \cdot x(a^\star \parallel b) \stackrel{\le}{=} \text{c\upharpoonright} x(a^\star \parallel b) \tag{12}$$

We then subsitute (10) into (12) to find that

$$x(a^\star \parallel b) \cdot a^\star + a \cdot a^\star \cdot x(a^\star \parallel b) \leq\_{\text{C\'oA}} x(a^\star \parallel b) \tag{13}$$

which, by the least fixpoint axiom, tells us that a- · (a- b) · a- -CKA x(a- b). Plugging the latter back into (9), we find that

$$a^\star \cdot (a \cdot a^\star \parallel b) \cdot a^\star + a \cdot a^\star \cdot a^\star \cdot (a^\star \parallel b) \cdot a^\star \leq\_{\text{c\''\kappa}} x (a \cdot a^\star \parallel b) \tag{14}$$

which can, using the exchange law, be reworked into

$$a^\star \cdot (a \cdot a^\star \parallel b) \cdot a^\star \stackrel{<}{=}\_{c\kappa\kappa} x(a \cdot a^\star \parallel b) \tag{15}$$

Now, if we choose x(a · a- b) = a- ·(a · a- b)· a and x(a- b) = a- ·(a- - b) · a-, we find that these choices satisfy (9) and (12)—making them part of a solution; by construction, they are also the least solutions.

In summary, x is a solution to the linear system, and by construction it is also the least solution. The reader is encouraged to verify that our choice of x(a- b) is indeed a closure of a- b.

5 A caveat here is that applying the exchange law indiscriminately may lead to a term that is not a closure (specifically, it may violate the semantic requirement in Definition 4.1). The algorithm used to solve arbitrary linear systems in Lemma 3.12 does not make use of the exchange law to simplify terms, and thus avoids this pitfall.

### **References**

**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 chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter'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.

## Concurrency and Distribution

## **Correctness of a Concurrent Object Collector for Actor Languages**

Juliana Franco1(B) , Sylvan Clebsch2, Sophia Drossopoulou1, Jan Vitek3,4, and Tobias Wrigstad5

> Imperial College London, London, UK<EMAIL_ADDRESS>Microsoft Research Cambridge, Cambridge, UK Northeastern University, Boston, USA CVUT, Prague, Czech Republic Uppsala University, Uppsala, Sweden

**Abstract.**  Multiple actors may mutate the heap while the collector is running without any dedicated synchronisation. ORCA is applicable to any actor language whose type system prevents data races and which supports causal message delivery. We present a model of ORCA which is parametric to the host language and its type system. We describe the interplay between the host language and the collector. We give invariants preserved by ORCA, and prove its soundness and completeness.

### **1 Introduction**

Actor-based systems are massively parallel programs in which individual actors communicate by exchanging messages. In such systems it is essential to be able to manage data automatically with as little synchronisation as possible. In previous work [9,12], we introduced the ORCA protocol for garbage collection in actor-based systems. ORCA is language-agnostic, and it allows for concurrent collection of objects in actor-based programs with no additional locking or synchronisation, no copying on message passing and no stop-the-world steps. ORCA can be implemented in any actor-based system or language that has a type system which prevents data races and that supports causal message delivery. There are currently two instantiations of ORCA, one is for Pony [8,11] and the other for Encore [5]. We hypothesise that ORCA could be applied to other actor-based systems that use static types to enforce isolation [7,21,28,36]. For libraries, such as Akka, which provide actor-like facilities, pluggable type systems could be used to enforce isolation [20].

This paper develops a formal model of ORCA. More specifically, the paper contributions are:

1. Identification of the requirements that the host language must statically guarantee;

c The Author(s) 2018 A. Ahmed (Ed.): ESOP 2018, LNCS 10801, pp. 885–911, 2018. https://doi.org/10.1007/978-3-319-89884-1\_31

A formal model facilitates the understanding of how ORCA can be applied to different languages. It also allows us to explore extensions such as shared mutable state across actors [40], reduction of tracing of immutable references [12], or incorporation of borrowing [4]. Alternative implementations of ORCA that rely on deep copying (*e.g.*, to reduce type system complexity) across actors on different machines can also be explored through our formalism.

Developing a formal model of ORCA presents challenges:

The full proofs and omitted definitions are available in appendix [16].

### **2 Host Language Requirements**

ORCA makes some assumptions about its host language, we describe them here.

#### **2.1 Actors and Objects**

Actors are active entities with a thread of control, while objects are data structures. Both actors and objects may have fields and methods. Method calls on objects are synchronous, whereas method calls on actors amount to asynchronous message sends—they all called *behaviours*. Messages are stored in a FIFO queue. When idle, an actor processes the top message from its queue. At any given point of time an actor may be either idle, executing a behaviour, or collecting garbage.

**Fig. 1.** Actors and objects. Full arrows are references, grey arrows are overwritten references: references that no longer exist.

**Fig. 2.** Capabilities. Heap mutation may modify what object is reachable through a path, but not the path's capability.

Figure 1 shows actors α1 and α2, objects ω1 to ω4. In [16] we show how to create this object graph in Pony. In Fig. 1(a), actor α1 points to object ω1 through field f1 to ω2 through field f3, and object ω1 points to ω3 through field f5. In Fig. 1(b), actor α1 creates ω4 and assigns it to this.f1.f5. In Fig. 1(c), α1 has given up its reference to ω1 and sent it to act2 which stored it in field f6. Note that the process of sending sent not only ω1 but also implicitily ω4.

#### **2.2 Mutation, Transfer and Accessibility**

Message passing is the only way to share objects. This falls out of the capability system. If an actor shares an object with another actor, then either it gives up the object or neither actor has a write capability to that object. For example, after α1 sends ω1 to α2, it cannot mutate ω1. As a consequence, heap mutation only decreases accessibility, while message sends can transfer accessibility from sender to receiver. When sending immutable data the sender does not need to transfer accessibility. However, when it sends a mutable object it cannot keep the ability to read or to write the object. Thus, upon message send of a mutable object, the actor must consume, or destroy, its reference to that object.

#### **2.3 Capabilities and Accessibility**

ORCA assumes that a host language's type system assigns *access rights* to paths. A path is a sequence of field names. We call these access rights *capabilities*.

We expect the following three capabilities; read, write, tag. The first two allow reading and writing an object's fields respectively. The tag capability only allows identity comparison and sending the object in a message. The type system must ensure that actors have no read-write races. This is natural for actor languages [5, 7,11,21].

Figure 2 shows capabilities assigned to the paths in Fig. 1: α1.f1.f5 has capability write, thus α1 can read and write to the object reachable from that path. Note that capapabilities assigned to paths are immutable, while the contents of those paths may change. For example, in Fig. 1(a), α1 can write to ω3 through path f1.f5, while in Fig. 1(b) it can write to ω4 through the same path. In Fig. 1(a) and (b), α2 can use the address of ω1 but cannot read or write it, due to the tag capability, and therefore cannot access ω3 (in Fig. 1(a)) nor ω4 (in Fig. 1(b)). However, in Fig. 1(c) the situation reverses: α2, which received ω1 with write capability is now able to reach it through field f6, and therefore ω4. Notice that the existence of a path from an actor to an object does not imply that the object is accessible to the actor: In Fig. 1(a), there is a path from α2 to ω3, but α2 cannot access ω3. Capabilities protect against data races by ensuring that if an object can be mutated by an actor, then no other actor can access its fields.

### **2.4 Causality**

ORCA uses messages to deliver protocol-related information, it thus requires causal delivery. Messages must be delivered after any and all messages that caused them. Causality is the smallest transitive relation, such that if a message m is sent by some actor after it received or sent m, then m is a cause of m . Causal delivery entails that m be delivered after m.

For example, if actor α1 sends m1 to actor α2, then sends m2 to actor α3, and α3 receives m2 and sends m3 to α2, then m1 is a cause of m2, and m2 is a cause of m3. Causal delivery requires that α2 receive m1 before receiving m3. No requirements are made on the order of delivery to different actors.

### **3 Overview of** ORCA

We introduce ORCA and discuss how to localise the necessary information to guarantee safe deallocation of objects in the presence of sharing. Every actor has a local heap in which it allocates objects. An actor *owns* the objects it has allocated, and ownership is fixed for an object's life-time, but actors are free to reference objects that they do not own. Actors are obligated to collect their own objects once these are no longer needed. While collecting, an actor must be able to determine whether an object can be deallocated using only local information. This allows all other actors to make progress at any point.

### **3.1 Mutation and Collection**

ORCA relies on capabilities for actors to reference objects owned by other actors and to support concurrent mutation to parts of the heap that are not being concurrently collected. Capabilities avoid the need for barriers.

**I1** An object accessible with write capability from an actor is not accessible with read or write capability from any other actor.

This invariant ensures an actor, while executing garbage collection, can safely trace any object to which it has read or write access without the need to protect against concurrent mutation from other actors.

### **3.2 Local Collection**

An actor can collect its objects based on local information without consulting other actors. For this to be safe, the actor must know that an owned, locally inaccessible, object is also globally inaccessible (*i.e.*, inaccessible from any other actors or messages)1. Shared objects are reference counted by their owner to ensure:

**I2** An object accessible from a message queue or from a non-owning actor has reference count larger than zero in the owning actor.

Thus, a locally inaccessible object with a reference count of 0 can be collected.

### **3.3 Messages and Collection**

**I1** and **I2** are sufficient to ensure that local collection is safe. Maintaining **I2** is not trivial as accessibility is affected by message sends. Moreover, it is possible for an actor to share a read object with another actor through a message. What if that actor drops its reference to the object? The object's owner should be informed so it can decrease its reference count. What happens when an actor receives an object in a message? The object's owner should be infomed, so that it can increase its reference count. To reduce message traffic, ORCA uses *distributed, weighted, deferred* reference counts. Each actor maintains reference counts that tracks the sharing of its objects. It also maintains counts for "foreign objects", tracking references to objects owned by other actors. This reference count for non-owning actors is what allows sending/receiving objects without having to inform their owner while maintaining **I2**. For any object or actor ι, we denote with LRC(ι) the reference count for ι in ι's owner, and with FRC(ι) we denote the sum of the reference counts for ι in all other actors. The counts do not reflect the number of references, rather the existence of references:

**I3** If a non-owning actor can access an object through a path from its fields or call stack, its reference count for this object is greater than 0.

An object is globally accessible if it is accessible from any actor or from a message in some queue. Messages include reference increment or decrement messages these are ORCA-level messages and they are not visible to applications. We introduce two logical counters: AMC(ι) to account for the number of application

1 For example, in Fig. 1(c) ω4 in is locally inaccessible, but globally accessible.

**Fig. 3.** Black arrows are references, numbered in creation order. Blue solid arrows are application messages and blue dashed arrows ORCA-level message. (Color figure online)

messages with paths to ι, and OMC(ι) to account for ORCA-level messages with reference count increment and decrement requests. These counters are not present at run-time, but they will be handy for reasoning about ORCA. The owner's view of an object is described by the LRC and the OMC, while the foreign view is described by the FRC and the AMC. These two views must agree:

$$\mathbf{I\_4} \qquad \forall \ \iota \ . \quad \text{LRC}(\iota) + \text{OMC}(\iota) = \text{AMC}(\iota) + \text{FRC}(\iota)$$

**I2**, **I3** and **I4** imply that a locally inaccessible object with LRC = 0 can be reclaimed.

### **3.4 Example**

Consider actors Andy, Bart and Catalin, and steps from Fig. 3.

*Initial State.* Let ω be a newly allocated object. As it is only accessible to its owning actor, Andy, there is no entry for it in any RC.

*Sharing* ω*.* When Andy shares ω with Bart, ω is placed on Bart's message queue, meaning that AMC(ω) = 1. This is reflected by setting RCAndy(ω) to 1. This preserves **I4** and the other invariants. When Bart takes the message with ω from his queue, AMC(ω) becomes zero, and Bart sets his foreign reference count for ω to 1, that is, RCBart(ω) = 1. When Bart shares ω with Catalin, we get AMC(ω) = 1. To preserve **I4**, Bart could set RCBart(ω) to 0, but this would break **I3**. Instead, Bart sends an ORCA-level message to Andy, asking him to increment his (local) reference count by some n, and sets his own RCBart(ω) to n. 2 This preserves **I4** and the other invariants. When Catalin receives the message later on, she will behave similarly to Bart in step 2, and set RCCatalin(ω)= 1.

The general rule is that when an actor sends one of its objects, it increments the corresponding (local) RC by 1 (reflecting the increasing number of foreign references) but when it sends a non-owned object, it decrements the corresponding (foreign) RC (reflecting a transfer of some of its stake in the object). Special care needs to be taken when the sender's RC is 1.

2 This step can be understood as if Bart "borrowed" n units from Andy, added n − 1 to his own RC, and gave 1 to the AMC, to reach Catalin eventually.

Further note that if Andy, the owner of ω, received ω, he would decrease his counter for ω rather than increase it, as his reference count denotes foreign references to ω. When an actor receives one of its owned objects, it *decrements* the corresponding (local) RC by 1 but when it receives a non-owned object, it *increments* the corresponding (foreign) RC by 1.

*Dropping References to* ω*.* Subsequent to sharing ω with Catalin, Bart performs GC, and traces his heap without reaching ω (maybe because it did not store ω in a field). This means that Bart has given up his stake in ω. This is reflected by sending a message to Andy to decrease his RC for ω by n, and setting Bart's RC for ω to 0. Andy's local count of the foreign references to ω are decreased piecemeal like this, until LRC(ω) reaches zero. At this point, tracing Andy's local heap can determine if ω should be collected.

*Further Aspects.* We briefly outline further aspects which play a role in ORCA.

Finally, we reflect on the nature of reference counts: they are *distributed*, in the sense that an object's owner and every actor referencing it keep separate counts; *weighted*, in that they do not reflect the number of aliases; and *deferred*, in that they are not manipulated immediately on alias creation or destruction, and that non-local increments/decrements are handled asynchronously.

### **4 The ORCA Protocol**

We assume enumerable, disjoint sets *ActorAddr* and *ObjAddr*, for addresses of actors and objects. The union of the two is the set of addresses including null. We require a mapping C*lass* that gives the name of the class of each actor in a given configuration, and a mapping O that returns the owner of an address

> *Addr* = *ActorAddr ObjAddr* {null} C*lass* : *Config* × *ActorAddr* → *ClassId* O : *Addr* → *ActorAddr*

such that the owner of an actor is the actor itself, *i.e.*, ∀α∈*ActorAddr*. O(α) = α.

Definition 1 describes run-time configurations, C. They consist of a heap, χ, which maps addresses and field identifiers to addresses,3 and an actor map, *as*, from actor addresses to actors. Actors consist of a frame, a queue, a reference count table, a state, a working set, marks, and a program counter. Frames are either empty, or consist of the identifier for the currently executing behaviour, and a mapping from variables to addresses. Queues are sequences of messages. A message is either an *application message* of the form app(φ) denoting a highlevel language message with the frame φ, or an ORCA message, of the form orca(ι: z), denoting an in-flight request for a reference count change for ι by z. The state distinguishes whether the actor is idle, or executing some behaviour, or performing garbage collection. We discuss states, working sets, marks, and program counters in Sect. 4.3. We use naming conventions: α ∈ *ActorAddr*; ω ∈ *ObjAddr*; ι ∈ *Addr*; z ∈ Z; n ∈ N; b ∈ *BId*; x ∈ *VarId*; A ∈ *ClassId*; and ιs for a sequence of addresses ι1...ιn. We write C.heap for C's heap; and α.quC, or α.rcC, or α.frameC, or α.stC for the queue, reference count table, frame or state of actor α in configuration C, respectively.

### **Definition 1 (Runtime entities and notation)**

$$\begin{aligned} \mathcal{C} &\in \textit{Config} = \textit{Heap} \times \textit{Actors} \\ \chi &\in \textit{Heap} = (\textit{Addr} \cdot \{\text{null}\}) \times FId \to \textit{Addr} \\ as \in \textit{Actors} &= \textit{Actor} \, \textit{Addr} \to \textit{Actor} \\ a &\in \textit{Actor} = \textit{Frame} \times \textit{Queue} \times \textit{References} \times \textit{PC} \\ &\quad \times \textit{State} \times \textit{Workset} \times \textit{Marks} \times PC \\ \phi &\in \textit{Frame} = \emptyset \quad \cup \ (\textit{BId} \times \textit{LocalMap}) \\ \psi &\in \textit{LocalMap} = \textit{VarId} \to \textit{Addr} \\ q &\in \textit{Queue} = \textit{Message}^{\star} \\ m &\in \textit{Message} ::= \text{orara}(\iota : z) \quad | \quad \textsf{app}(\phi) \\ \mathbf{r} &\in \textit{Reference} \times \textit{Addr} \to \mathbb{N} \end{aligned}$$

*State, Workset, Marks, and PC described in Definition 7.*

**Example:** Figure 4 shows C0, our running example for a runtime configuration. It has three actors: α1–α3, represented by light grey boxes, and eight objects, ω1–ω8, represented by circles. We show ownership by placing the objects in square boxes, *e.g.* O(ω7) = α1. We show references through arrows, *e.g.* ω6 references ω8 through field f7, that is, C0.heap(ω6, f7) = ω8. The frame of α2 contains behaviour identifier b , and maps x to ω8. All other frames are empty. The message queue of α1 contains an application message for behaviour b and argument ω5 for x, the queue of α2 is empty, and the queue of α3 an ORCA message for ω7. The bottom part shows reference count tables: α1.rcC0 (α1) = 21,

3 Note that we omitted the class of objects. As our model is parametric with the type system, we can abstract from classes, and simplify our model.

and α1.rcC0 (ω7) = 50. Entries of owned addresses are shaded. Since α2 owns α2 and ω2, the entries for α2.rcC0 (α2) and α2.rcC0 (ω2) are shaded. Note that α1 has a non-zero entry for ω7, even though there is no path from α1 to ω7. There is no entry for ω1; no such entry is needed, because no actor except for its owner has a path to it. The 0 values indicate potentially non-existent entries in the corresponding tables; for example, the reference count table for actor α3 needs only to contain entries for α1, α3, ω3, and ω4. Ownership does not restrict access to an address: *e.g.* actor α1 does not own object ω3, yet may access it through the path this.f1.f2.f3, may read its field through this.f1.f2.f3.f4, and may mutate it, *e.g.* by this.f1.f2.f3 = this.f1.

Lookup of fields in a configuration is defined in the obvious way, *i.e.*

**Definition 2.** C(ι.f) ≡ C.heap(ι, f)*, and* C(ι.f.f ) ≡ C.heap(C(ι.f,f ))

### **4.1 Capabilities and Accessibility**

ORCA considers three capabilities:

$$\kappa \in Capacity = \{\text{read}, \text{write}, \text{tag}\},$$

where read allows reading, write allows reading and writing, and tag forbids both read and write, but allows the use of an object's address. To describe the capability at which objects are visible from actors we use the concepts of *static* and *dynamic paths*.

*Static paths* consist of the keyword this (indicating a path starting at the current actor), or the name of a behaviour, b, and a variable, x, (indicating a path starting at local variable x from a frame of b), followed by any number of fields, f.

$$sp ::= \mathbf{t}\mathbf{h}\mathbf{\dot{s}} \quad \mid \quad b.x \quad \mid \quad sp.f$$

**Fig. 4.** Configuration C0. ω1 is absent in the ref. counts, it has not been shared.

The host language must assign these capabilities to static paths. Thus, we assume it provides a static judgement of the form

$$A \vdash sp \colon \kappa \qquad \text{where } A \in ClassId$$

meaning that a static path *sp* has capability capability when "seen" from a class A. We highlight static judgments, *i.e.*, those provided by the type system in blue.

We expect the type system to guarantee that read and write access rights are "deep", meaning that all paths to a read capability must go through other read or write capabilities (**A1**), and all paths to a write capability must go through write capabilities (**A2**).

**Axiom 1** *For class identifier* A*, static path sp, field f , capability* κ*, we assume: A1* A *sp*.f : κ −→ ∃κ = tag. A *sp* : κ . *A2* A *sp*.f : write −→ A *sp* : write.

Such requirements are satisfied by many type systems with read-only references or immutability (*e.g.* [7,11,18,23,29,33,37,41]). An implication of **A1** and **A2** is that capabilities degrade with growing paths, *i.e.*, the prefix of a path has more rights than its extensions. More precisely: A *sp* : κ and A *sp*.f : κ imply that κ ≤ κ , where we define write < read < tag, and κ ≤ κ *iff* κ = κ or κ<κ .

**Example:** Table 1 shows capabilities for some paths from Fig. 4. Thus, A1 this.f1 : write, and A2 b .x : write, and A2 this.f8 : tag. The latter, together with **A1** gives that A2 this.f8.f : κ for all κ and f.

As we shall see later, the existence of a path does not imply that the path may be navigated. For example, C0(α2.f8.f4) = ω4, but actor α2 cannot access ω4 because of A2 this.f8 : tag.

Moreover, it is possible for a path to have a capability, while not being defined. For example, Table 1 shows A1 this.f1.f2 : write and it would be possible to have Ci(α1.f1) = null, for some configuration Ci that derives from C0.

**Table 1.** Capabilities for paths, where A1 = Class(α1) and A2 = Class(α2).

*Dynamic paths* (in short paths p) start at the actor's fields, or frame, or at some pending message in an actor's queue (the latter cannot be navigated yet, but will be able to be navigated later on when the message is taken off the queue). Dynamic paths may be local paths (lp) or message paths. Local paths consist of this or a variable x followed by any number of fields f. In such paths, this is the current actor, and x is a local variable from the current frame. Message paths consist of k.x followed by a sequence of fields. If k ≥ 0, then k.x indicates the local variable x from the k-th message from the queue; k = −1 indicates variables from either (a) a message that has been popped from the queue, but whose frame has not yet been pushed onto the stack, or (b) a message whose frame has been created but not yet been pushed onto the queue. Thus, k = −1 indicates that either (a) a frame will be pushed onto the stack, during message receiving, or (b) a message will be pushed onto the queue during message sending.

p ∈ *Path* ::= lp | mp lp ::= this | x | lp.f mp ::= k.x | mp.f

We define accessibility as the lookup of a path provided that the capability for this path is defined. The *partial* function A returns a pair: the address accessible from actor α following path p, and the capability of α on p. A path of the form *p*.owner returns the owner of the object accessible though *p* and capability tag.

### **Definition 3 (accessibility).** *The partial function*

A : *Config* × *ActorAddr* × *Path* → (*Addr* × *Capability*) *is defined as*

We use AC(α, p) = ι as shorthand for ∃κ. AC(α, p)=(ι, κ). The second and third case above ensure that the capability of a message path is the same as when the message has been taken off the queue and placed on the frame.

**Example:** We obtain that AC0 (α1,this.f1.f2.f3)=(ω3,write), from the fact that Fig. 4 says that C0(α1.f1.f2.f3) = ω3 and from the fact that Table 1 says that A1 this.f1.f2.f3 : write. Similarly, AC0 (α2,this.f8)=(ω3,tag), and AC0 (α2, x )=(ω8,write), and AC0 (α1, 0.x.f5.f7)=(ω8,tag).

Both AC0 (α1,this.f1.f2.f3), and AC0 (α2,this.f8) describe paths from actors' fields, while AC0 (α2, x ) describes a path from the actor's frame, and finally AC0 (α1, 0.x.f5.f7) is a path from the message queue.

Accessibility describes what may be read or written to: AC0 (α1,this.f1.f2.f3) = (ω3,write), therefore actor α1 may mutate object ω3. However, this mutation is not visible by α2, even though C0(α2.f8) = ω3, because AC0 (α2,this.f8)=(ω3,tag), which means that actor α2 has only opaque access to ω3.

Accessibility plays a role in collection: If the reference f3 were to be dropped it would be safe to collect ω4; even though there exists a path from α2 to ω4; object ω4 is not accessible to α2: the path this.f8.f4 leads to ω4 but will never be navigated (AC0 (α2,this.f8.f4) is undefined). Also, AC(α2,this.f8.owner)=(α3,tag); thus, as long as ω4 is accessible from some actor, *e.g.* through C(α2.f8) = ω4, actor α3 will not be collected.

Because the class of an actor as well as the capability attached to a static path are constant throughout program execution, the capabilities of paths starting from an actor's fields or from the same frame are also constant.

**Lemma 1.** *For actor* α*, fields* f*, behaviour b, variable x , fields f , capabilities* κ*,* κ *, configurations* C *and* C *, such that* C *reduces to* C*' in one or more steps:*

$$\begin{array}{ccccc} \mathsf{-}\mathcal{A}\_{\mathcal{C}}(\alpha,\mathsf{this}.\overline{f}) = (\mathsf{.},\mathsf{\kappa}) & \mathsf{.}\mathsf{.}\mathsf{\mathcal{A}}\_{\mathcal{C}'}(\alpha,\mathsf{this}.\overline{f}) = (\mathsf{.}',\mathsf{\kappa}') & \longrightarrow & \mathsf{\kappa}=\mathsf{\kappa}'\\\mathsf{-}\ \mathsf{-}\mathcal{A}\_{\mathcal{C}}(\alpha,x.\overline{f}) = (\mathsf{.},\mathsf{\kappa}) & \mathsf{.}\mathsf{\mathcal{A}}\_{\mathcal{C}'}(\alpha,x.\overline{f}) = (\mathsf{.}',\mathsf{\kappa}') & \wedge\\\alpha.\mathsf{frame}\_{\mathcal{C}} = (b,.) & \wedge & \alpha.\mathsf{frame}\_{\mathcal{C}'} = (b,.) & \longrightarrow & \kappa=\mathsf{\kappa}' \end{array}$$

### **4.2 Well-Formed Configurations**

We characterise data-race free configurations (-C ♦):

$$\begin{array}{llll}\textbf{Definition 4 (Data-race freeform).} & \mathbb{H}\in\mathscr{C}\diamond & \textbf{iff} \\ \forall\alpha,\alpha',p,p',\kappa,\kappa'. & \\ & \alpha\neq\alpha' & \wedge \quad \mathscr{A}\_{\mathscr{C}}(\alpha,p)=(\iota,\kappa) & \wedge \quad \mathscr{A}\_{\mathscr{C}}(\alpha',p')=(\iota,\kappa') \\ & \longrightarrow & \\ & \kappa\sim\kappa' & \\ \forall\text{ }\kappa\sim\kappa' & \\ & \kappa\sim\kappa' & \text{iff} \ [\ (\kappa=\text{write}\longrightarrow\kappa'=\text{tag})\ \wedge \ (\kappa'=\text{write}\longrightarrow\kappa=\text{tag})\ ] ] \end{array}$$

This definition captures invariant **I1**. The remaining invariants depend on the four derived counters introduced in Sect. 3. Here we define LRC and FRC, and give a preliminary definition of AMC and OMC.

#### **Definition 5 (Derived counters—preliminary for** AMC **and***ss* OMC**)**

$$\begin{aligned} \text{LRC}\_{\mathcal{C}}(\iota) & \equiv \mathcal{O}(\iota). \text{rc}\_{\mathcal{C}}(\iota) \\ \text{FRC}\_{\mathcal{C}}(\iota) & \equiv \sum\_{\alpha \neq \mathcal{O}(\iota)} \alpha. \text{rc}\_{\mathcal{C}}(\iota) \\ \text{OMC}\_{\mathcal{C}}(\iota) & \equiv \sum\_{j} \begin{cases} z & \text{if } \mathcal{O}(\iota). \text{qu}\_{\mathcal{C}}[j] = \text{cora}(\iota : z) \\ 0 & \text{otherwise} \end{cases} + \dots c.f. \text{Definition 12} \\ \text{AMC}\_{\mathcal{C}}(\iota) & \equiv \#\{\{\alpha, k\} \mid k > 0 \land \exists x. \overline{f}. \mathcal{A}\_{\mathcal{C}}(\alpha, k. x. \overline{f}) = \iota \} + \dots c.f. \text{Definition 12} \\ \text{where } \iota' \text{ denotes} \quad \iota'. \text{ Then} \end{aligned}$$

*where* # *denotes cardinality.*

For the time being, we will be reading this preliminary definition as if ... stood for 0. This works under the assumption the procedures are atomic. However Sect. 5.3, when we consider fine-grained concurrency, will refine the definition of AMC and OMC so as to also consider whether an actor is currently in the process of sending or receiving a message from which the address is accessible. For the time being, we continue with the preliminary reading.

**Example:** Assuming that in C0 none of the actors is sending or receiving, we have LRCC0 (ω3) = 160, and FRCC0 (ω3) = 160, and OMCC0 (ω3) = 0, and AMCC0 (ω3) = 0. Moreover, AMCC0 (ω6) = AMCC0 (α2) = 1: neither ω6 nor α2 are arguments in application messages, but they are indirectly reachable through the first message on α1's queue.

A well-formed configuration requires: **I1**–**I4**: introduced in Sect. 3; **I5**: the RC's are non-negative; **I6**: accessible paths are not dangling; **I7**: processing message queues will not turn RC's negative; **I8**: actors' contents is in accordance with their state. The latter two will be described in Definition 14.

**Definition 6 (Well-formed configurations—preliminary).** - C*,* iff *for all* α*,* αo*,* ι*,* ι *,* p*,* lp*, and* mp*, such that* αo = O(ι) = α*:*

**I1** - C ♦ **I2** [ AC(α, p)=ι ∨ AC(αo, mp)=ι ] −→ LRCC(ι)>0 **I3** AC(α, lp) = ι −→ α.rcC(ι) > 0 **I4** LRCC(ι) + OMCC(ι) = FRCC(ι) + AMCC(ι) **I5** α.rcC(ι ) ≥ 0 **I6** AC(α, p)=ι −→ C.heap(ι) =⊥ **I7, I8** *description in Definition 14.*

For ease of notation, we take **I5** to mean that if α.rcC(ι ) is defined, then it is positive. And we take any undefined entry of α.rcC(ι) to be 0.

### **4.3 Actor States**

We now complete the definition of runtime entities (Definition 1), and describe the states of an actor, the worksets, the marks, and program counters. (Definition 7). We distinguish the following states: idle (IDLE), collecting (COLLECT), receiving (RECEIVE), sending a message (SEND), or executing the synchronous part of a behaviour (EXECUTE). We discuss these states in more detail next.

Except for the idle state, IDLE, all states use auxiliary data structures: *worksets*, denoted by ws, which stores a set of addresses; *marks* maps, denoted by ms, from addresses to R (reachable) or U (unreachable), and program counters. Frames are relevant when in states EXECUTE, or SEND, and otherwise are assumed to be empty. Worksets are used to store all addresses traced from a message or from the actor itself, and are relevant when in states SEND, or RECEIVE, or COLLECT, and otherwise are empty. Marks are used to calculate reachability and are used in state COLLECT, and are ignored otherwise. The program counters record the instruction an actor will execute next; they range between 4 and 27 and are ghost state, *i.e.* only used in the proofs.

**Fig. 5.** State transitions diagram for an actor.

### **Definition 7 (Actor States, Working sets, and Marks)**

```
st∈State ::= IDLE | EXECUTE | SEND | RECEIVE | COLLECT
ws∈Workset = P(Addr)
 ms∈Marks = Addr → {R, U}
   pc ∈ PC = [ 4..27 ]
```
We write α.stC, or α.wsC, or α.msC, or α.pcC for the state, working set, marks, or the program counter of α in C, respectively.

Actors may transition between states. The state transitions are depicted in Fig. 5. For example, an actor in the idle state (IDLE) may receive an orca message (remaining in the same state), receive an app message (moving to the RECEIVE state), or start garbage collection (moving to the COLLECT state).

In the following sections we describe the actions an actor may perform. Following the style of [17,26,27] we describe actors' actions through pseudo-code procedures, which have the form:

procedure nameα: condition → { instructions }

We let α denote the executing actor, and the left-hand side of the arrow describes the condition that must be satisfied in order to execute the instructions on the arrow's right-hand side. Any actor may execute concurrently with other actors. To simplify notation, we assume an implicit, globally accessible configuration C. Thus, instruction α.state:=EXECUTE is short for updating the state of α in C to be EXECUTE. We elide configurations when obvious, *e.g.* α.frame = φ is short for requiring that in C the frame of α is φ, but we mention them when necessary—*e.g.* - C[ι1, f → ι2] ♦ expresses that the configuration that results from updating field f in ι1 is data-race free.

*Tracing Function.* Both garbage collection, and application message sending/receiving need to find all objects accessible from the current actor and/or from the message arguments. We define two functions: trace this finds all addresses which are accessible from the current actor, and trace frame finds all addresses which are accessible through a stack frame (but not from the current actor, this).

**Fig. 6.** Pseudo-code for garbage collection.

**Definition 8 (Tracing).** *We define the functions*

trace this : *Config*×*ActorAddr* → P(*Addr*) trace frame : *Config*×*ActorAddr*× *Frame* → P(*Addr*) *as follows* trace thisC(α) ≡{ι| ∃f. AC(α,this.f)=ι}

trace frameC(α, φ) ≡{ι| ∃x ∈ dom(φ), f. AC(α, x.f)=ι}

### **4.4 Garbage Collection**

We describe garbage collection in Fig. 6. An idle, or an executing actor (precondition on line 2) may start collecting at any time. Then, it sets its state to COLLECT (line 5), and initialises the marks, ms, to empty (line 6).

The main idea of ORCA collection is that the requirement for global unreachability of owned objects can be weakened to the local requirement to local unreachability and a LRC = 0. Therefore, the actor marks all owned objects, and all addresses with a RC > 0 as U (line 9). After that, it traces the actor's fields, and also the actor's frame if it happens not to be empty (as we shall see later, idle actors have empty frames) and marks all accessible addresses as R (line 12). Then, the actor marks all owned objects with RC > 0 as R (line 15). Thus we expect that: **(\*)** *Any* ι with ms(ι)=U *is locally unreachable, and if owned by the current actor, then its* LRC*is 0.* For each address with ms(ι) = U, if the actor owns ι, then it collects it (line 20)—this is sound because of **I2**, **I3**, **I4** and (\*). If the actor does not own ι, then it asks ι's owner to decrement its reference count by the current actor's reference count, and deletes its own reference count to it (thus becoming 0) (line 24)—this preserves **I2**, **I3** and **I4**.