# Strong Priority and Determinacy in Timed CCS

Luigi Liquori

Inria, France

Michael Mendler

University of Bamberg, Germany

## Abstract

Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called *constructive reduction* which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of *coherent* processes a confluence property for constructive reductions. We show that under some restrictions, called *pivotability*, coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner's classical confluence theory for CCS without priorities.

**2012 ACM Subject Classification** Theory of computation, Process algebras

**Keywords and phrases** Timed process algebras, determinacy, priorities, synchronous programming

Digital Object Identifier 10.4230/LIPICs...

**Funding** Luigi Liquori: Partially funded by ETSI.

Michael Mendler: Partially funded by UniCA/I3S.

## 1 Introduction

Concurrency, by expression or by implementation, is both a convenient and unavoidable feature of modern software systems. However, this does not mean that we must necessarily give up the requirement of functional determinism which is crucial for maintaining predictability and to manage design complexity by simple mathematical models [23, 8, 13]. While the pure λ-calculus is naturally deterministic by design, it cannot model shared memory. Process algebras can naturally model shared objects, but do not guarantee determinism out of the box. In this paper we use the standard mathematical formalism CCS [27] to study methods for reconciling concurrency and determinism.

### Determinacy in Process Algebra

In CCS, the interaction of concurrent processes $P \mid Q$ arises from the rendezvous synchronisation of an action $\alpha$ of $P$ and an associated co-action $\bar{\alpha}$ from $Q$, generating a silent action $\tau$, also called a reduction. A process is in normal form if cannot reduce any more and determinate if it reduces to at most one normal form, up to some notion of structural congruence. As a simplified example for the scenarios that we are interested in, consider a triple of concurrent processes $R \mid S \mid W$, where $S \stackrel{def}{=} r.S + w.r.0$ acts as a shared resource, such as a (write-once) store, while $R \stackrel{def}{=} r.0$, $W \stackrel{def}{=} w.0$ are read and write processes, respectively, sharing $S$ with each other. The store $S$ offer a read action $r$ (rendezvous) leaving the state unchanged, or a write action $w$ upon which it changes its state to $r.0$. At this point, the store only permits a single read and then becomes the inactive process $0$. The synchronisation between the actions $r$, $w$ and co-actions $\bar{r}$, $\bar{w}$ generates two sequences of reductions from $R \mid S \mid W$:

$$0 \mid \bar{r}.0 \mid 0 \stackrel{\tau}{\rightleftharpoons} 0 \mid S \mid W \stackrel{\tau}{\rightleftharpoons} R \mid S \mid W \stackrel{\tau}{\rightarrow} R \mid \bar{r}.0 \mid 0 \stackrel{\tau}{\rightarrow} 0 \mid 0 \mid 0.$$

<figure><img src="image_1.png" /></figure>

© Author: Please provide a copyright holder;

licensed under Creative Commons License CC-BY 4.0

Leibniz International Proceedings in Informatics

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## XX:2 Strong Priority and Determinacy in Timed CCS

Obviously, $R|S|W$ is not determinate. It reduces to two distinct normal forms $0|\bar{r}.0|0$ and $0|0|0$. The final store $\bar{r}.0$ on the left permits one more read, while $0$ on the right does not.

A sufficient condition for determinacy is determinism. A process $P$ is (structurally) deterministic if for all its derivatives $Q$ and action $\alpha \in Act$, if $Q \xrightarrow{\alpha} Q_1$ and $Q \xrightarrow{\alpha} Q_2$ then $Q_1 \equiv Q_2$, where $\equiv$ is a suitable structural congruence. However, determinism is too strong. For instance, the store $P \stackrel{\text{def}}{=} R_1|S|R_2$ with two readers $R_i \stackrel{\text{def}}{=} \bar{r} \cdot R'_i$ ($i=1,2$) is determinate but not deterministic, when the $R_i$ may reach structurally distinct states after reading, say, $P \xrightarrow{\tau} R'_1|S|R_2$ and $P \xrightarrow{\tau} R_1|S|R'_2$ where $R'_1|S|R_2 \not\equiv R_1|S|R'_2$. Moreover, determinism is not closed under parallel composition. In the above example, all process $R_1, R_2, S$ are deterministic, but their composition $P$ is not. An insightful solution, proposed by Milner (Chap. 11 of [27]), is to replace determinism by the notion of *confluence* which still implies determinacy but turns out to be closed under parallel composition, under natural restrictions.

**Definition 1.** $P$ is (structurally) confluent<fnref n="1" /> if for every derivative $Q$ of $P$ and reductions $Q \xrightarrow{\alpha_1} Q_1$ and $Q \xrightarrow{\alpha_2} Q_2$ with $\alpha_1 \neq \alpha_2$ or $Q_1 \neq Q_2$, there exist $Q'_1 \equiv Q'_2$ such that $Q_1 \xrightarrow{\alpha_2} Q'_1$ and $Q_2 \xrightarrow{\alpha_1} Q'_2$.

Milner shows that confluence is preserved by “confluent composition” $P|_L Q \stackrel{\text{def}}{=} (P|Q)\setminus L$, combining the parallel and restriction operators, subject to the condition that $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}\text{ and } \mathcal{L}(P) \cap \mathcal{L}(Q) = L \cup \bar{L}$, where $\mathcal{L}(R)$ is the sort of a process $R$. This is a form of *sort separation*, ensuring that every action $\alpha$ has at most one synchronisation partner $\bar{\alpha}$ either inside or outside of $(P|Q)\setminus L$. Many practical examples of determinate systems can be understood as sort-separated compositions of confluent processes. However, this still covers only a rather limited class of applications. Most seriously, memory processes such as $S$ above are intrinsically not confluent, and even if they were, confluent composition forbids direct multi-cast communication, because labels such as $r$ in $S$ could not be shared by two readers $R_1, R_2$ due to sort-separation. This means that concurrent programming languages that support shared memory and yet have determinate reduction semantics, cannot be handled.

## Determinacy in Synchronous Programming

The most prominent class of shared-memory programming languages that manage to reconcile concurrency and determinacy, is known as *Synchronous Programming (SP)*. In SP, processes interact with each other asynchronously at a *micro-step* level, yet synchronise in lock-step to advance jointly in iterative cycles of synchronous *macro-steps*. The micro-step interactions taking place during a macro-step determine the final outcome of the macro-step. This outcome is defined at the point where all subsystem pause to wait for a global logical *clock*. When this clock arrives, all subsystem proceed into the next computation cycle. Under the so-called *synchrony hypothesis*, the final outcome of a macro-step for each subsystem is fully determined from the stimulus provided by the environment of that component during the micro-step interactions. As such, the interactions inside each subsystem at macro-step level can be abstracted into a global Mealy automaton with deterministic I/O. SP started with Statecharts [17] and has generated languages such as Signal [14], Lustre [16], Esterel [5], Quartz [37], SCCharts [41], just to mention a few.

When it comes to mathematical modelling it is natural to think of a clock as a broadcast action in the spirit of Hoare's CSP [19] that acts as a synchronisation barrier for a set of concurrent processes. Used with some scheduling control, it can bundle each process' actions

<footnote n="1">¹ A variation of Milner’s “strong confluence” that includes $\tau$-actions and uses $\equiv$ not bisimulation $\sim$.</footnote>
into a sequence of macro-steps that are aligned with each other in a lock-step fashion. During each macro-step, a process executes only a temporal slice of its total behaviour, at the end of which it waits for all other processes in the same *clock scope* to reach the end of the current phase. When all processes have reached the barrier, they are released into the next round of computation. This suggests a priority-based scheduling mechanism, i.e., that the clock should fire only if the system has stabilised and no other admissible data actions are possible. This principle, called *maximal progress*, is built into timed process algebras, see e.g. [18, 11].

## Contribution

We introduce an extension of CCS, denoted CCS<sup>spt</sup>, that brings together the concepts of *priorities* [10, 36, 33] and *clocks* [15, 11, 32] that have previously been studied for CCS, but independently. We thus obtain an adequate compositional setting for SP based on standard techniques from process algebra. This is surprising since many different customised semantics (e.g., [24, 9, 5, 1]) have been developed for SP over the years, few of which fit into the classical framework of CCS. Similar ideas might be possible for other process algebras like ATP [31], TPL [18], CSP or some synchronous variants of Milner's π-calculus [2], just to mention a few. We find CCS most plausible as a point of departure since the concept of priorities is already well established and the combination of asynchronous scheduling and communication via local rendezvous synchronisation makes the problem of ensuring determinacy more prominent.

Our calculus CCS<sup>spt</sup> provides a natural setting to take a fresh look at confluence in CCS as an adequate mathematical model for SP. Moreover, we envisage that CCS<sup>spt</sup>, extended by value-passing, can be used as a playground to study compositional embeddings of concurrent λ-calculi. In particular, we have in mind those with sharing, as required for the lazy semantics of Haskell and with deterministic memory such as IVars/TVars [25] and LVars [22]. At the technical level, we make the following specific contributions in this paper:

* We use broadcast actions (clocks) as global synchronisation barriers to schedule processes using priorities in a more flexible way than any of the earlier approaches. While PMC [15] has clocks but no priorities and in CSA [11] the priorities are hardwired and expressing precedence only between the rendezvous actions and the clock, we use a fully general priority scheme as in Phillips' CCS<sup>Ph</sup> [33]. By adding clocks to CCS<sup>Ph</sup> we generalise previous CCS extensions such as Milner's SCCS [26], PMC or CSA for expressing synchronous interactions of concurrent processes. To achieve this, we must strengthen Phillips' notion of weak enabling (Def. 2) by constructive enabling (Def. 3). While all classical extensions of CCS by priorities [10, 36, 33] schedule the processes by their immediate initial actions, constructive enabling takes into account all actions potentially executable up to the next clock barrier.

* We identify a strictly larger class of processes that enjoy the Church Rosser (CR) Property (and thus reduce to unique normal forms) than the “confluence class” discussed by Milner, see e.g., Chap. 11 of [27]. Since priorities are not part of the classical confluence theory, it cannot model deterministic shared objects with conflicting choice. In this paper, exploiting priorities and clocks, we enrich Milner’s notion of confluence to “confluence up-to priorities” that we call coherence (Def. 12). We show that coherent processes are CR for constructive enabling (Thm. 14).

* We show that coherence is preserved by parallel composition under reasonable restrictions that permit sharing and memory (Thm. 24). Specifically, we construct coherent processes in a type-directed compositional fashion using the notion of *precedence policies* (Def. 16). The policy for a conformant process specifies an upper bound for its precedence-blocking behaviour (Def. 17). A policy enriches the classical sort of a process by priority information. We define the special class of *pivot policies* and call coherent processes conforming to them
XX:4 Strong Priority and Determinacy in Timed CCS

133 *pivotable processes* (Def. 48). These are not only coherent (and thus CR) but preserved by
parallel composition and other operators of the language (Thm. 24). In this fashion, we are
135 able to extend Milner’s classical results for confluent processes to cover significantly more
136 applications, specifically Esterel-style multi-cast SP with shared objects.

137 • We show that each coherent process is *clock-deterministic* (Prop. 15) and that pivotable
138 processes satisfy *maximal progress* (Prop. 23). No matter in which order we execute
139 constructively enabled reductions, when the normal form is reached, and only then, a
140 clock can tick. Since the normal form is uniquely determined, each pivotable process
141 represents a “synchronous stream”. As such, our work extends the classical non-deterministic
142 theory of timed (multi-clocked) process algebras [15, 18, 11] for applications in deterministic
143 synchronous programming.

144 For lack of space, four separate appendices will present (A) how research towards
145 determinacy for process algebras passes through those above cited papers, (B) a collection of
146 more tricky examples, and (C,D) the full proofs.

147 2 A Process Algebra with Clocks and Priorities

148 The syntax and operational semantics of our process algebra ‘SynPaTick’, denoted CCS<sup>spt</sup>, is
149 defined in this section.

150 2.1 CCS<sup>spt</sup> Syntax

151 The terms in CCS<sup>spt</sup> form a set *P* of processes. We use *P*, *Q*, *R*, *S*... to range over *P*. Let
152 *I* be a set of process names and let *A*, *B*... range over *I*. Let *A* be a countably infinite
153 set of channel names with *a*, *b*... ranging over *A*. As in CCS, the set *Ā* is a disjoint set
154 of co-names with elements denoted by *ā*, *b̄*, *c̄*... in bijection with *A*; The overbar operator
155 switches between *A* and *Ā*, i.e., *ā* = *a* for all *ā* ∈ *A*. We will refer to the names *a* ∈ *A* as
156 *input* (or *receiver*) labels while the co-names *ā* ∈ *Ā* denote *output* (or *sender*) labels. Let
157 *C* be a countably infinite set of broadcasted *clock names*, disjoint from both *A* and *Ā* and
158 let *σ* range over *C*. Every clock acts as its own co-name, *σ̄* = *σ* and so each *σ* ∈ *C* is also
159 considered as a *clock label*. Let *L* = *A* ∪ *Ā* ∪ *C* be the set of input, output and clock labels
160 and let *l* range over *L*, while *L*, *H* range over subsets of *L*. We write *L̄* for the set {*l* | *l* ∈ *L*}.
161 Let *Act* = *L* ∪ {*τ*} be the set of all *actions* obtained by adjoining the *silent action* *τ* ∉ *L* and
162 let *α* range over *Act*. Viewed as actions, the input and output labels *l* ∈ *R*<sup>def</sup> = *A* ∪ *Ā* ⊆ *Act*
163 are referred to as *rendezvous actions* to distinguish them from the *clock actions* *σ* ∈ *C* ⊆ *Act*.
164 All symbols can appear indexed. The process terms *P* are defined thus:

<table>
  <tbody>
    <tr>
      <td>P, Q, R, S</td>
      <td>::=</td>
      <td>0</td>
      <td>stop (inaction)</td>
      <td>P | Q</td>
      <td>parallel</td>
    </tr>
    <tr>
      <td></td>
      <td>|</td>
      <td>A</td>
      <td>name, A &isin; I</td>
      <td>P \ L</td>
      <td>restriction</td>
    </tr>
    <tr>
      <td></td>
      <td>|</td>
      <td>&alpha;:H.P</td>
      <td>action, &alpha; &isin; L, H &sube; L</td>
      <td>P / L</td>
      <td>hiding</td>
    </tr>
    <tr>
      <td></td>
      <td>|</td>
      <td>P + Q</td>
      <td>choice</td>
      <td></td>
      <td></td>
    </tr>
  </tbody>
</table>

167 Intuitively, 0 denotes the *inactive* process which stops all computations, including clock
168 actions. The *action prefix* α:H.P denotes a process that offers to engage in the action α
169 and then behaves as P while the *blocking set* H ⊆ L lists all actions taking precedence over
170 α. A prefix with α ∈ R denotes a CCS-style rendezvous action. In case α ∈ C, it denotes a
171 CSP-style broadcast action that can communicate with all the surrounding processes sharing
172 on the same clock only when the clock is universally *consumed*. We assume that in every
173 restriction P \ L the set L ⊆ R consists of rendezvous actions, and in every hiding P / L
174 we have L ⊆ C. These *scoping* operators act as name binders that introduce local scopes.
<figure><img src="image_2.png" /><figcaption>Figure 1 Structural Congruence, where $\star \in \{|, +\}$ and $\iota \in \{\setminus, /\}$.</figcaption></figure>

The acute reader will notice the absence of the relabelling operator $P[f]$, useful in CCS to define the well-known “standard concurrent form” ($P_1[f_1] | \cdots | P_2[f_n] \setminus L$). Because all of our examples are captured without need of relabelling, and for the sake of simplicity, relabelling will be treated in the full version of this work. A useful abbreviation is to drop the blocking sets if they are empty or drop the continuation process if it is inactive. For instance, we will typically write $a.P$ instead of $a:\{\} .P$ and $a:H$ rather than $a:H.0$. Also, it is useful to drop the braces for the blocking set if it is a singleton, writing $a:b.P$ instead of $a:\{b\} .P$. In our concrete notation using the abstract syntax of processes, we assume that the binary operator $+$ is right associative and taking higher binding strength than the binary operator $|$, i.e., writing $P + Q + R \mid S$ instead of $(P + (Q + R)) \mid S$. Also, we assume that the unary operators of prefix, restriction and hiding have higher binding strength than the binary operators. Hence, we write $P \setminus c + a.b.c.Q \mid R/\sigma$ instead of $((P \setminus c) + (a.(b.(c.Q)))) \mid (R/\sigma)$. The sub-processes of a $P$ are all sub-expressions of $P$ and (recursively) all sub-processes of $Q$ for definitions $A \stackrel{\text{def}}{=} Q$ where $A$ is a sub-expression of $P$. Sometimes it is useful to consider fragments of $\mathcal{P}$. Specifically, a process is called *unclocked* if $P$ does not contain any clock prefix $\sigma:H.Q$ as a sub-process. A process is called *sequential* or *single-threaded* if it does not contain any parallel sub-process $Q \mid R$. $P$ is *closed* if all sub-processes $\ell:H.Q$ in $P$ occur in the scope of a restriction or hiding operator that binds $\ell$. As usual, we denote by $\mathcal{L}(P) \subseteq \mathcal{L}$ the free labels, called (*syntactic*) *sort* of $P$, identify processes that differ only in the choice of bound labels.

Following Milner's presentation of the π-calculus in [28], we define a structural congruence over processes. Specifically, structural congruence $\equiv$ is the smallest congruence over $\mathcal{P}$ that satisfies the equations in Fig. 1. The idea of the structural congruence is to split interaction rules between agents from rules governing the “left-to-right” representation of expressions. It allows to use those equations in the derivation rules of the SOS making the latter simpler and easy to use, and it allows to set up formal equivalence of processes increasing for each program the number of legal SOS transitions that, otherwise, would be blocked. Milner divides CCS equations in static, dynamic and expressions laws. We choose an approach inspired by the work of Berry and Boudol [7] by adding an explicit structural rule in the operational semantics. Note that we do not include in our structural rules all of Milner’s τ-laws, i.e. the ones related to the presence of τ-actions, like e.g. $\alpha.\tau.P \equiv \alpha.P$, or $P + \tau.P \equiv \tau.P$, and we have also dropped the congruence equations related to the uniqueness of solution of recursive equations and the expansion laws related to the standard concurrent form (cf. Chap. 3, Props. 2, 4(2) and 5 of [27]). Since we do not propose notions of behavioural equivalence in this paper, we prefer to take a conservative approach and only consider a minumum set of purely structural rules that do not impinge on the dynamics of expression behaviour.
## 2.2 Operational Semantics

The operational semantics for CCS<sup>spt</sup> is given using a labelled transition relation $P \xrightarrow{\alpha} Q$
in the style of Plotkin's Structured Operational Semantics (SOS) [35, 34], where $\alpha \in Act$
is the action that labels the SOS transition. When $\alpha \in \mathcal{L}$, the transition corresponds to a
communication step, namely a rendezvous action or a broadcasted clock action. When $\alpha = \tau$
is silent, then the transition corresponds to a *reduction* or an *evaluation* step. In addition,
we decorate the nondeterministic SOS with annotations that provides sufficient information
to express a uniform and confluent reduction strategy based on scheduling precedences.
Including these annotations, our SOS judgment takes the form $P \xrightarrow{\alpha|_H} Q$ where $P, Q, R \in \mathcal{P}$
are processes, $\alpha \in Act$ is an action, and $H \subseteq Act$ a set of actions. The semantics is defined
inductively as the smallest relation closed under the rules in Fig. 2. We call each transition
derivable by Fig. 2 an *admissible* transition. We denote by $\alpha:H[R]$ a compound *c-action*
consisting of the three annotations $\alpha$, $H$, and $R$. The information provided by such a c-action
is sufficient to define our *constructive reduction* strategy for CCS<sup>spt</sup> that satisfies a refined
confluence property. Sometimes, we write $P \xrightarrow{\alpha} Q$ to state that there is a transition for some
$R$ and $H$.

The intuition behind the annotations of admissible transitions is as follows: $\alpha$ is the usual action “passed back” in the SOS. The blocking set $H$ is the set of actions that take precedence over $\alpha$, and $R$, called the concurrent context, is a process that represents the behaviour of all threads in $P$ that execute concurrently with the transition. i.e., all actions in $R$ are potentially in competition with $\alpha$. Think of $H$ as the resources that are required by the action and of $R$ as the concurrent context that potentially competes for $H$. In a parallel composition $P \mid Q$ of $P$ with another process $Q$, the context $R$ might interact with the environment $Q$ to generate actions in the blocking set $H$. If this happens, the reduction in $P$ with blocking set $H$ will be considered blocked in our scheduled semantics (see Def. 28).

In the rules of Fig. 2, the reader can observe how the annotation for the concurrent context and the blocking sets are inductively built. In a nutshell: Rule (*Act*) is the axiom annotating in the transition the action and the (empty) environment. Rules (*Restr*) and (*Hide*) deal with “local restriction” of rendezvous actions and “local hiding” of broadcasted clocks. Rules (*Par*) and (*Sum*) are almost standard and deal with parallelism and choice. Rule (*Struct*) internalises in the transition the above presented structural equivalence of processes. Rule (*Com*) constitutes the core of our SOS. It captures, in an elegant way, both the classical CCS rendezvous communication rule *and* the classical CSP broadcasting communication; it has an extra *race* test, enriching the blocking set of the conclusion by $\tau$, in case $P$ and $Q$ interfere. The presence of $\tau$ will block unconditionally. Finally, rule (*Con*) deals with process names and refers to a process whose behaviour is specified by a definitional equation $A \stackrel{def}{=} P$.

## 2.3 Constructive Scheduling

The operational semantics of Fig. 2 for rendezvous actions coincides with that of CCS and the rules for clock actions coincide with the semantics of CSP broadcast actions. The scheduling annotations $H$ and $R$ of a c-action $\alpha:H[R]$ expose extra information about blocking and concurrent context, respectively, of the underlying action $\alpha$. We can use them to implement different scheduling strategies. Prioritised process algebras [10, 36, 33] block an admissible transition $\alpha:H[R]$ when $H$ contains the silent action $\tau$ or an action that synchronises with some initial action of the concurrent context $R$. Otherwise, it is (weakly) enabled.

► **Definition 2** (Initial actions and weakly-enabled transition).

■ The set $iA(R) \subseteq Act$ of initial actions of a process $R$ is given as $iA(R) = \{\alpha \mid \exists Q. R \xrightarrow{\alpha} Q\}$.
$$ \overline{\alpha:H.P \xrightarrow{\alpha|_0} P} \text{ (Act)} \qquad \frac{P \equiv P' \quad P' \xrightarrow{\alpha|_R} H \quad Q' \equiv Q \quad R' \equiv R}{P \xrightarrow{\alpha|_R} Q} \text{ (Struct)} $$

$$ \frac{P \xrightarrow{\alpha|_R} H \quad Q \quad L' = L \cup \bar{L} \quad \alpha \notin L' \quad H' = H - L'}{P \setminus L \xrightarrow{\alpha|_{R \setminus L}} H' \quad Q \setminus L} \text{ (Restr)} \qquad \frac{P \xrightarrow{\alpha|_R} H \quad Q \quad H' = H - L}{P/L \xrightarrow{\alpha/L} H' \quad Q/L} \text{ (Hide)} $$

$$ \frac{P \xrightarrow{\alpha|_R} H' \quad \alpha \notin C}{P | Q \xrightarrow{\alpha|_{R|Q}} H' | Q} \text{ (Par)} \qquad \frac{P \xrightarrow{\alpha|_R} H' P'}{P + Q \xrightarrow{\alpha|_R} H' P'} \text{ (Sum)} $$

$$ \frac{P \xrightarrow{\ell|_{R_1}} H_1 P' \quad Q \xrightarrow{\bar{\ell}|_{R_2}} H_2 Q' \quad H = \text{race}(P,Q)}{P | Q \xrightarrow{\ell|\bar{\ell}|_{R_1|R_2}} H_1 \cup H_2 \cup H | P' | Q'} \text{ (Com)} \qquad \frac{A \stackrel{\text{def}}{=} P \quad P \xrightarrow{\alpha|_R} H' P'}{A \xrightarrow{\alpha|_R} H' P'} \text{ (Con)} $$

$$ \text{where} \qquad \alpha/L \stackrel{\text{def}}{=} \begin{cases} \tau & \text{if } \alpha \in L \\ \alpha & \text{otherwise} \end{cases} \qquad \ell/\bar{\ell} \stackrel{\text{def}}{=} \begin{cases} \tau & \text{if } \ell \in \mathcal{R} \\ \ell & \text{if } \ell \in \mathcal{C} \end{cases} \\ \text{race}(P,Q) \stackrel{\text{def}}{=} \begin{cases} \{\tau\} & \text{if } H_1 \cap \bar{iA}(Q) \notin \{\ell\} \text{ or } H_2 \cap \bar{iA}(P) \notin \{\bar{\ell}\} \\ \{\}\ & \text{otherwise} \end{cases} $$

<caption>Figure 2 The admissible transitions of CCS<sup>spt</sup> processes. See Def. 2 for the initial actions iA(P).</caption>

An transition with c-action α:H[R] is called weakly enabled if H ∩ (iA(R) ∪ {τ}) = {}.

Let us call a process *P* free if all its c-actions α:H[R] have an empty blocking set *H* = {}.
The weakly enabled transitions of (unclocked) free processes coincide with the semantics of
CCS [27]. We call *P* discrete if all its c-actions α:H[R] are self-blocking, i.e. *H* = {α}. A
process *P* is irreflexive if no action prefix α:H.Q occurring in *P* blocks itself, i.e., α ∉ H.
One can show that for (unclocked) irreflexive processes, a transition is weakly enabled iff
is derivable in the operational semantics of CCS<sup>Ph</sup> [33]<sup>2</sup>. Thus, CCS and CCS<sup>Ph</sup> correspond
to theories of free and irreflexive processes of CCS<sup>spt</sup>, respectively, under weak enabling.
Likewise the theories [10, 36] can be subsumed; specifically, the prioritised sum operator
*P* ↦ *Q* of [10] can be coded as *P* + *Q*:iA(*P*) in CCS<sup>spt</sup>. The theory [36] proposes two levels of
labels, *a*:0 and *a*:1, where 0 denotes higher priority and 1 ordinary priority. Translated into
CCS<sup>spt</sup>, the prefix *a*:0.*P* corresponds to *a*:{}.*P* while an action prefix *a*:1.*P* maps in CCS<sup>spt</sup>
to *a*:Prio.*P* if we define Prio as the set of all high-prioritised labels.

Examples 4 and 5 below in Sec. 3 demonstrate how prioritised scheduling by weak enabling (Def. 2) can indeed help to ensure determinacy in special cases. For the general case, however, weak enabling is not sufficient. In order to prevent non-determinacy (a global property) from priorities (a purely local property), we must be able to block a c-action α:H[R] not just if the initial actions iA(R) of the concurrent context R can synchronise with H, as in weak enabling, but look at the set iA*(R) of all actions that R can potentially engage in, before it reaches a clock. Example 7 in Sec. 3 illustrates this.

► **Definition 3 (Potential actions and constructive enabling).**

The set iA*(P) ⊆ L of potential actions is the smallest extension iA(P) ∩ L ⊆ iA*(P)
such that if ℓ ∈ iA*(Q) and P α Q for α ∈ R ∪ {τ}, then ℓ ∈ iA*(P).

A transition with c-action α:H[R] is called constructively enabled, or c-enabled for short,
if H ∩ (iA*(R) ∪ {τ}) = {}.

<footnote n="2">² In CCS<sup>Ph</sup> the blocking sets are written before the action, H:α.P, where we write α:H.P in CCS<sup>spt</sup>.</footnote>
XX:8 Strong Priority and Determinacy in Timed CCS

The following Sec. 3 presents some motivating examples, while Sec. 4 focuses on the
mathematical theory underlying CCS$^{spt}$.

3 Examples

The first example shows the basic mechanism of how priorities can be used to schedule
processes under weak enabling.

**Example 4 (Read Before Write).** Consider a “store” $S \stackrel{def}{=} w.r+r:w$ that offers a write action $w$ followed by a read $r$, or a read action $r$ but prefers the write over the read. The fact that $w$ takes priority over $r$ is recorded in the blocking set $\{w\}$ which contains the action $w$. If we put $S$ in parallel with a reader $R \stackrel{def}{=} \bar{r}$, the read actions $r$ and $\bar{r}$ synchronise in a reduction $S|R \xrightarrow[0]{\tau}{w} 0$. The blocking set $\{w\}$ will block $R$'s transition when a parallel writer $W \stackrel{def}{=} \bar{w}$ is added, as well. Specifically, the reduction $S|R|W \xrightarrow[\bar{w}]{\tau}{w} W$ is not weakly enabled, because $\{w\} \cap \bar{iA}(\bar{w}) = \{w\} \cap \{w\} \neq \{\}$. The only enabled reduction is that between $S$ and $W$ giving $S|R|W \xrightarrow[\bar{r}]{\tau}{w} r|R$ and only then continue with the read $r|R \xrightarrow[0]{\tau}{w} 0$. Thus, weak enabling makes the reduction determinate. Observe that $S$ is not confluent (Def. 1): We have $S \xrightarrow{w} r$ and $S \xrightarrow{r} 0$ but there is no $P_1 \equiv P_2$ such that $r \xrightarrow{r} P_1$ and $0 \xrightarrow{w} P_2$. However, $S$ is coherent (Def. 12), because the transition $S \xrightarrow[0]{r}{w} 0$ interferes (Def. 11) with the former $S \xrightarrow[0]{w}{r} w \in \{w\}$, whence coherence does not require confluence.

Processes can block each other from making progress. This happens under weak enabling if
processes offer two-way rendezvous synchronisation with contradicting precedences.

**Example 5 (Binary Blocking).** Take processes $P \stackrel{def}{=} a:b.A + b$ and $Q \stackrel{def}{=} \bar{b}:\bar{a}.B + \bar{a}$. Their composition $P|Q$ has two admissible reductions, through $a:b|\bar{a}$ to $A$ or through $b|\bar{b}:\bar{a}$ to $B$. So, disregarding the precedences, it is non-deterministic if $A \not\equiv B$. Under weak enabling, however, $P|Q$ creates a circular deadlock: $P$ offers $a$ unless synchronisation with $\bar{b}$ is possible, while $Q$ offers $\bar{b}$ provided there is no synchronisation with $a$. None of the reductions is enabled. By the “race” side-condition of (Com) the synchronisation $a:b|\bar{a}$ generates the c-action $\tau:H[0]$ with $\tau \in H$ because $\{b\} \cap i\bar{A}(Q) \not\subseteq \{a\}$. Similarly, since $\{\bar{a}\} \cap i\bar{A}(P) \not\subseteq \{\bar{b}\}$, the synchronisation $b|\bar{b}:\bar{a}$ is blocked. We note that neither $P$ nor $Q$ is confluent, but they are coherent.

**Example 6 (Reflexive Blocking).** Consider the free process $s|\bar{s}.A|\bar{s}.B$ where action $s$ can be consumed by $\bar{s}.A$ or by $\bar{s}.B$, generating non-deterministic $\tau$-transitions to $A|\bar{s}.B$ or to $\bar{s}.A|B$. However, by adding self-blocking, as in $s:s|\bar{s}.A|\bar{s}.B$, weak enabling protects the prefix $s$ from being consumed when both $\bar{s}.A$ and by $\bar{s}.B$ compete for it. If only one is present, as in $s:s|\bar{s}.A$ and $s:s|\bar{s}.B$, no blocking occurs.

Blocking under weak enabling ensures determinism in the special case where the circular
depending involves only initial actions. However, parallel threads can create dependency
chains through sequences of actions, e.g., when accessing a shared process that is acting as a
resource. This is the general case handled by c-enabling.

**Example 7 (Transitive Blocking).** Consider the process $S \stackrel{def}{=} w_0 + r_0:w_0 | w_1 + r_1:w_1$ which offers receiver actions $w_i$ and $r_i$ for $i \in \{0,1\}$ such that $w_i$ has precedence over $r_i$. Now take processes $P_0 \stackrel{def}{=} \bar{r}_0 \cdot \bar{w}_1$ and $P_1 \stackrel{def}{=} \bar{r}_1 \cdot \bar{w}_0$ which first aim to synchronise with $r_i$ and then sequentially afterwards with $w_{1-i}$. The parallel composition $P_0 | S | P_1$ has two initial $\tau$-reductions $P_0 | w_0 + r_0 : w_0 | \bar{w}_0 \stackrel{\tau}{\underset{P_0 | (w_0+r_0:w_0)}{\rightleftharpoons}} \{w_1\} P_0 | S | P_1 \stackrel{\tau}{\underset{w_1+r_1:w_1 | P_1}{\rightleftharpoons}} \{w_0\} \bar{w}_1 | w_1 + r_1 : w_1 | P_1$.
These reductions are both weakly enabled. If we continue under weak enabling then the residual process $\overline{w_1} | w_1 + r_1:w_1 | P_1$ for the first reduction must first execute the synchronisation on $w_1$ and thus proceed as $\overline{w_1} | w_1 + r_1:w_1 | P_1 \xrightarrow{\tau} P_1$ while the residual process $P_0 | w_0 + r_0:w_0 | \overline{w_0}$ can only reduce to $P_0$. Hence, the resulting final outcome of executing $P_0 | S | P_1$ is non-deterministic. Observe that none of the two reductions displayed above is actually c-enabled. For the right reduction we find that its concurrent environment $R_0 \stackrel{\text{def}}{=} w_1 + r_1:w_1 | P_1$ has a reduction sequence $R_0 \xrightarrow{\tau} \overline{w_0}$ and thus $\{w_0\} \cap i\overline{A}^*(R_0) \subseteq \{w_0\} \cap i\overline{A}^*(\overline{w_0}) = \{w_0\} \cap \{w_0\} \neq \{\}$. Symmetrically, for the concurrent environment $R_1 \stackrel{\text{def}}{=} P_0 | w_0 + r_0:w_0$ of the left reduction we have $R_1 \xrightarrow{\tau} \overline{w_1}$ and hence $\{w_1\} \cap i\overline{A}^*(R_1) \neq \{\}$. The parallel composition $P_0 | S | P_1$ is deterministic under c-enabling. We note again, $S$ is not confluent but coherent (Def. 12).

The next example generalises Ex. 4 to a full memory cell.

**▶ Example 8 (Read/Write Memory).** Let $w_0, w_1, r_0, r_1$ the labels of writing/reading a boolean value 0 or 1, respectively. A memory would be modelled by two mutually recursive processes

$$wAND_0 \stackrel{\text{def}}{=} w_1.wAND_1 + w_0:w_1.wAND_0 + r_0:\{w_0, w_1\}.wAND_0$$

$$wAND_1 \stackrel{\text{def}}{=} w_1.wAND_1 + w_0:w_1.wAND_0 + r_1:\{w_0, w_1\}.wAND_1$$

The process $wAND_v$ represents the memory cell in a state where it has stored the value $v \in \{0, 1\}$. In either state, it offers to synchronise with a write action $w_u$ to change its state to $wAND_u$, and also with a read action $r_v$ to transmit its stored value $v$ to a reader. The write actions $w_u$ do not only change the state of the memory, they also block the read actions since they appear in their blocking sets $r_v:\{w_0, w_1\}$.

<figure><img src="image_3.png" /></figure>

Between the write actions, the blocking sets implement a precedence of $w_1$ over $w_0$. In the picture on the right the process state transitions are visualised with the blocking sets as red dashed arrows.

**▶ Example 9 (Esterel Signals).** Concurrent Esterel threads communicate via signals [6, 38]. A (pure, temporary) signal can have two statuses, present and absent. At the beginning of a synchronous macro-step, each signal is initialised to be absent, by default. The signal becomes present as soon as some thread emits it. It remains present thereafter for throughout the current macro-step, i.e., until the next clock cycle is started. The clock is a global synchronisation, taken by all threads simultaneously. The value of the signal is broadcast to all concurrent threads which can test it and branch their control-flow according to the signal's status. To maintain coherency of data-flow and deterministic behaviour, the signal status can only be read when no writing is possible any more. Esterel compilers conduct a causality analysis on the program and obtain a suitable static schedule when they generate imperative code. In Esterel hardware compilers, the scheduling is achieved dynamically by propagating signal statuses. Programs that cannot be scheduled to satisfy the emit-before-test protocol, or hardware that does not stabilise are called non-constructive and rejected by the compiler. A pure, temporary signal is modelled by the following recursive behaviour:

$$S_0 \stackrel{\text{def}}{=} \text{abs:emit}.S_0 + \text{emit}.S_1 + \sigma:\{\text{abs, emit}\}.S_0$$

$$S_1 \stackrel{\text{def}}{=} \text{pres}.S_1 + \text{emit}.S_1 + \sigma:\{\text{pres, emit}\}.S_0$$

which is depicted on the right and structurally coherent according to Def. 12.

<figure><img src="image_4.png" /></figure>
XX:10 Strong Priority and Determinacy in Timed CCS

$$
\mathbf{ABRO} \stackrel{\text{def}}{=} \sigma.(A|B|R|O|T) \setminus \{s,t\}
$$

$$
A \stackrel{\text{def}}{=} k_a:k_a.0 + a:\{k_a, a\}.\bar{s}:\bar{s}.0 + \sigma:\{k_a, a\}.A
$$

$$
B \stackrel{\text{def}}{=} k_b:k_b.0 + b:\{k_b, b\}.\bar{s}:\bar{s}.0 + \sigma:\{k_b, b\}.B
$$

$$
R \stackrel{\text{def}}{=} r:r.\bar{k}_a:\bar{k}_a.\bar{k}_b:\bar{k}_b.\bar{k}_s:\bar{k}_s.\bar{k}_t:\bar{k}_t.ABRO + \tau:r.\sigma.R
$$

$$
O \stackrel{\text{def}}{=} k_t:k_t.0 + t:\{k_t, t\}.\bar{o}:\bar{o}.0 + \sigma:\{k_t, t\}.O
$$

$$
T \stackrel{\text{def}}{=} k_s:k_s.0 + s:\{k_s\}.T + \bar{t}:\{k_s, \bar{t}, s\}.0 + \sigma:\{k_s, \bar{t}, s\}.T
$$

<figure><img src="image_5.png" /><figcaption>Figure 3 ABRO as a CCS<sup>spt</sup> process, Mealy machine and SyncChart.</figcaption></figure>

► **Example 10 (ABRO).** The *hello world* in synchronous languages, see [6], ABRO has the following behaviour: *Emit the output o as soon as both inputs a and b have been received. Reset this behaviour each time the input r occurs, without emitting o in the reset cycle.* [38]

The behaviour of ABRO is expressed as a Mealy machine and a SyncChart, displayed in Fig. 3 on the right. The synchronous behaviour of Esterel lies in the assumption that each transition of the Mealy machine summarises a single *macro-step* interaction of the machine with its environment. The transitions of parallel machines synchronise so that state changes proceed in lock-step. The simultaneous execution of these transitions that make up a macro-step consists of the sending and receiving of signals. The propagation of individual signals between machines is modeled in the *micro-step* operational semantics of Esterel.

**module ABRO:**
*input A, B, R;*
*output O;*
*loop*
*    await A || await B;*
*    emit O*
*    each R*
*end module*

In CCS<sup>spt</sup> we represent the micro-steps as sequences of τ-transitions, i.e., rendez-vous synchronisations, whereas the macro-step is captured as a global clock synchronisation. Unfortunately, the Mealy machine formalism is not scalable because the number of states can grow exponentially as the number of signals grow, while in Esterel can be expressed in a linear number of code lines as seen on the right.

The *loop P each R* construct of Esterel executes the behaviour of program P for an unbounded number of clock cycles, but restarts its body P when the signal R becomes present. The reset R takes priority over the behaviour of P which is preempted at the moment that the reset occurs. Note that in Esterel each signal appears exactly once, as in the specification and unlike in the Mealy machine. Other parts of Esterel also naturally arise from precedence-based scheduling. Esterel's *loop P each R* mechanism, for instance, can be coded using the static parallel composition operator that combines the process P to be aborted and reset with a "watchdog" process R. The latter waits for the reset signal from the environment in each clock cycle. The choice between the reset and continuing inside P is resolved by giving R higher priority. When the reset occurs, the watchdog sends "kill" signals to all threads running in P and waits for these to terminate. Only then the watchdog R restarts P from scratch. This is a form of precedence that can be expressed in the blocking sets of CCS<sup>spt</sup>. As such, Fig. 3 on the left translates the Esterel code of ABRO compositionally in CCS<sup>spt</sup>. ABRO is obtained as a parallel composition $(R|ABO) \setminus \{s,t\}$ combining a watchdog R with the behaviour $ABO \stackrel{\text{def}}{=} A|B|O|T$. The R is responsible to implement the reset loop at the superstate called ABO, as in the state charts. The ABO is the behaviour of the interior of this superstate, which corresponds to the statement $(await A || await B); emit O$ in Esterel: it is the parallel composition of $A|B$ making up the behaviour of the region called AB with code `await A || await B`. The processes $T|O$ implement the synchronisation that waits for termination of AB to start the output process O. We assume that the channels *a*, *b*, *r*, *o* modelling interface signals A, B, R, O all have a unique sender and receiver. This is seen
in our coding from the fact that the prefixes for these channels are self-blocking.

# 4 Coherence and Determinacy for CCS<sup>spt</sup>

This section presents the core elements of our scheduling theory under constructive enabling: coherence, policies, and policy-conformant processes. *Coherence* (Def. 12) corresponds to Milner’s notion of confluence, but refined “up-to” priorities. It requires structural confluence for c-enabled and diverging c-actions only if they do not interfere with each other considering their blocking sets and concurrent environments.

**Definition 11 (Transition Interference).** Two c-enabled transitions with c-actions $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are interference-free if $\alpha_1 = \alpha_2$ or $\alpha_i \notin H_{3-i}$ for all $i \in \{1, 2\}$.

Observe that for free processes (i.e., with empty blocking sets) all c-actions are interference-free and they are c-enabled iff they are admissible. Confluence of interference-free c-actions is formulated using an auxiliary form of *residual transition* $P \stackrel{\alpha}{\rightsquigarrow} Q$. This is a transition from $P$ to $Q$ with an action that is a “factor” of $\alpha$. Formally, we define $P \rightsquigarrow \alpha Q$ if $(i) \alpha \in \mathcal{L}$ with $P \stackrel{\alpha}{\Rightarrow} Q$ or $P \equiv Q$, or $(ii) \alpha = \tau$ with $P \stackrel{\tau}{\Rightarrow} Q$ or $P \stackrel{\ell}{\Rightarrow} Q$ or $P \stackrel{\bar{\ell}}{\Rightarrow} Q$ for some $\ell \in \mathcal{R}$.

**Definition 12 (Process Coherence).** A process $P$ is (structurally) coherent if for all its derivatives $Q$ the following holds: Given two c-enabled and interference-free transitions $Q \xrightarrow{\alpha_1} H_1 Q_1$ and $Q \xrightarrow{\alpha_2} H_2 Q_2$ such that $\alpha_1 \neq \alpha_2$ or $Q_1 \neq Q_2$ or both $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$. Then, there exist transitions $Q_1 \xrightarrow{\alpha_2} H'_2 Q'$ and $Q_2 \xrightarrow{\alpha_1} H'_1 Q'$ with $H'_i \subseteq H_i$ and $E_1 \rightsquigarrow \alpha_2 E'_1$ and $E_2 \rightsquigarrow \alpha_1 E'_2$.

For free processes, coherence implies confluence (Def. 1), but is strictly stronger.

**Example 13.** For instance, $Q \stackrel{\text{def}}{=} a:\{\}$.0 is confluent but not coherent. Since the prefix not self-blocking, coherence ensures that the label must *consumable* by arbitrarily many concurrent processes. Technically, since $Q \xrightarrow{a} Q_1$ and $Q \xrightarrow{a} Q_2$ for $Q_1 \equiv 0 \equiv Q_2$, there should be a transition $Q_i \xrightarrow{a} Q'$ which is not the case. However, for discrete processes, coherence is identical with confluence: With self-blocking, $Q \stackrel{\text{def}}{=} a:\{a\}$.0 is both confluent and coherent. It is important to note that all examples in Sec. 3 are coherent but not confluent.

**Theorem 14 (Coherence implies Determinacy).** Every coherent process is determinate under c-enabled reductions.

A coherent process cannot simultaneously offer both a clock and another distinct action without putting them in precedence order. Moreover, whenever a clock is enabled, then every further reduction of the process is blocked by the clock. Thm. 14 concerns the $\tau$-transitions of a coherent process. For clock transitions we have an even stronger result.

**Proposition 15 (Clock Determinism).** Every coherent process $P$ is structurally clock deterministic, i.e., if $P \stackrel{\sigma}{\Rightarrow} P_1$ and $P \stackrel{\sigma}{\Rightarrow} P_2$ then $P_1 \equiv P_2$.

The question is now how we can obtain coherent processes by composition. In view of Milner’s classical result for confluence, we expect to have to impose some form of “sort-separation” for parallel processes. It turns out that we can express such a condition and even avoid the restriction operator (thereby permit sharing) if we enrich the sorts $\mathcal{L}(P)$, $\mathcal{L}(Q)$ by priority information. We call the resulting enriched sorts $\pi(P)$, $\pi(Q)$ precedence policies.
XX:12 Strong Priority and Determinacy in Timed CCS

429

430

431

**► Definition 16 (Precedence Policy).** A precedence policy is a pair $\pi = (L, ---)$ where $L \subseteq \mathcal{L}$ is a subset of visible actions, called the alphabet of $\pi$ and $--- \subseteq L \times L$ a binary relation on $L$, called the precedence relation.

432

433

434

435

We will write $\ell \in \pi$ to state that $\ell$ is in the alphabet of $\pi$ and we write $\ell_1 \dashrightarrow \ell_2 \in \pi$ to express that the pair $(\ell_1, \ell_2)$ is in the precedence relation of the policy. Further, if $\ell_1, \ell_2 \in \pi$ and both $\ell_1 \dashrightarrow \ell_2 \notin \pi$ as well as $\ell_2 \dashrightarrow \ell_1 \notin \pi$, we say that $\ell_1$ and $\ell_2$ are concurrently independent under $\pi$, written (by abuse of the set-notation) $\ell_1 \diamond \ell_2 \in \pi$.

436

437

438

For any policy $\pi = (L, ---)$ and set of labels $K \subseteq \mathcal{L}$ we denote by $\pi \setminus K$ the policy $\pi$ restricted to the alphabet $L - (K \cup \bar{K})$ in the standard way. There is also the normal inclusion ordering $\pi_1 \subseteq \pi_2$ between policies defined by $L_1 \subseteq L_2$ and $---_1 \subseteq ---_2$.

439

440

The next Def. 17 on conformance captures how policies statically specify the externally observable scheduling behaviour of a process.

441

442

**► Definition 17 (Conformance).** $P$ conforms to a policy $\pi$ if for each derivative $Q$ of $P$: If $Q \xrightarrow{\ell/R} H$ $Q'$ with $\ell \in \mathcal{L}$, then $\ell \in \pi$ and for all $\ell' \in H \cap \mathcal{L}$, then $\ell' \dashrightarrow \ell \in \pi$.

443

444

445

446

447

448

449

For a process $P$ and policy $\pi$, let us write$^3 P \Vdash \pi$ to express that $P$ is coherent and conforms to policy $\pi$. We will say that $P$ is coherent for $\pi$. If $P \Vdash \pi$ then the alphabet of $\pi$ corresponds to the sort $\mathcal{L}(P)$ in CCS. It gives an upper bound on the labels that can be used by the process, and the precedence relation in $\pi$ provides a static over-approximation of the blocking, i.e., which labels can be in a choice conflict with each other. As a notational shortcut we will write $P \Vdash \ell_1 \dashrightarrow \ell_2$ to say that there is a policy $\pi$ with $P \Vdash \pi$ and $\ell_1 \dashrightarrow \ell_2 \in \pi$. Analogously, we write $P \Vdash \ell_1 \diamond \ell_2$ if there is a policy $\pi$ with $\ell_1 \diamond \ell_2 \in \pi$ and $P \Vdash \pi$.

450

451

452

453

454

455

456

**► Example 18.** The most permissive policy for a given sort $L \subseteq \mathcal{L}$, written $\pi_{max}(L)$, contains all labels from $L$ as its alphabet but no precedences, i.e., $\ell_1 \diamond \ell_2 \in \pi_{max}(L)$ for all $\ell_1, \ell_2 \in L$. If $P \Vdash \pi_{max}$ then $P$ has sort $L$ and will permit arbitrarily many concurrent processes to consume its labels $L$ under c-enabling. The most restrictive policy, denoted $\pi_{min}(L)$, also has alphabet $L$, but full precedences, i.e., $\ell_1 \dashrightarrow \ell_2 \in \pi_{min}$ for all $\ell_1, \ell_2 \in L$. If $P \Vdash \pi_{min}(L)$, then $P$ has sort $L$ but does not permit any concurrency; it can only communicate with a single sequential thread.

457

458

459

460

461

462

463

**► Example 19.** Reflexive precedences $\ell \dashrightarrow \ell \in \pi$ play a special role in our theory. They permit a conformant $P \Vdash \pi$ and its derivatives to execute $\ell$ only with a single partner. For instance, ABRO from Ex. 10 satisfies ABRO $\not\Vdash r \diamond r$ and so ABRO $| \sigma.\bar{r} $ reduces but ABRO $| \sigma.\bar{r} | \sigma.\bar{r} $ will block after the initial clock transition. In contrast, if the policy specifies $\ell \diamond \ell \in \pi$, then in a process $P \Vdash \pi$ any $\ell$-transition is consumable arbitrarily often. For instance, the Esterel signal from Ex. 9 has $S_1 \Vdash \mathit{pres} \diamond \mathit{pres}$ and so $S_1 | \overline{\mathit{pres}} | \mathit{pres}$ will not block.

464

Here we are interested in processes that conform to policies with special properties.

465

466

467

468

**► Definition 20 (Pivot and precedence-closed policy).** A policy $\pi$ is called
- *pivotable* if $\overline{L} \subseteq L$ and for all $\ell_1, \ell_2 \in L$ with $\ell_1 \neq \ell_2$ we have $\ell_1 \diamond \ell_2 \in \pi$ or $\overline{\ell_1} \diamond \overline{\ell_2} \in \pi$.
- *precedence-closed* for $L \subseteq \mathcal{L}$ if $\ell_1 \in L$ and $\ell_1 \dashrightarrow \ell_2 \in \pi$ implies $\ell_2 \in L$.
A process is *pivotable/precedence-closed* if $P$ conforms to *pivot/precedence-closed policy*.

<footnote n="3">³ In Milner’s notation we would write $P : \pi$, but we already use the colon ‘:’ for blocking sets as in CCS<sup>Ph</sup>.</footnote>
**Example 21.** An Esterel signal (Ex. 9) has the alphabet $\{emit, pres, abs\} = \mathcal{L}(S_i)$ ($i \in \{1,2\}$) and for simplicity we ignore the clock $\sigma$) and is conformant to the policy psig with $emit \rightarrow abs \in psig$. A typical program $R$ accessing the signal has alphabet $\{pres, abs\} \subseteq \mathcal{L}(S_i)$ and is of form $R = \overline{pres:pres.R_1 + abs:\{abs, pres\}.R_0}$. If the signal is present then $R_1$ is executed, if it is absent then $R_0$ is executed. Such $R$ conforms to a policy prg with $pres \rightarrow abs \in prg$ and $\ell \rightarrow \ell \in prg$ for $\ell \in \{pres, abs\}$. Both psig and prg as well as their union psig $\cup$ prg are pivot policies, so that $R \mid S_i$ is pivotable. In a pivotable process, conflicting choices are resolved by the precedences in a single thread, acting as the “pivot”. In $R \mid S_i$ the pivot is the signal $S_i$ on reading, resolving the choice $pres + abs$ in $R$, and it is the program $R$ on writing, resolving the choice $abs + emit$ in $S_i$.

Non-pivotable processes, in general, may block because of two threads entering into a circular precedence deadlock with each other.

**Example 22.** For example, recall the processes $P \stackrel{def}{=} a:b.A + b$ and $Q \stackrel{def}{=} \bar{b}:\bar{a}.B + \bar{a}$ from Example 5. Their parallel composition $P \mid Q$ creates a deadlock under (even weak) enabling because of the contradicting precedences in the two possible interactions $a:b \mid \bar{a}$ and $b \mid \bar{b}:\bar{a}$. The deadlock is reflected in the policy $\pi$ of $P$ satisfying $b \rightarrow a \in \pi$ and $\bar{a} \rightarrow \bar{b} \in \pi$ which is not a pivot policy that would instead require $a \diamond b \in \pi$ or $\bar{a} \diamond \bar{b} \in \pi$.

Reductions of pivotable processes never block because of two threads entering into a circular precedence deadlock with each other. One can show that for pivotable processes of at most two threads, the three operational semantics of CCS (admissible), of CCS$^\text{Ph}$ (weak enabling) and our CCS$^\text{spt}$ (c-enabling) all coincide. This is a consequence of the fact (cf. Lem. 51 and 52) that the race test in the rule (Com) is never introducing the silent action $\tau$ into the blocking sets. In general, pivotable processes may consist of three or more interacting threads, and blocking may occur and the semantics of CCS, CCS$^\text{Ph}$ and CCS$^\text{spt}$ are different. However, one can show that the blocking of a synchronisation is always due to the external environment. In other words, the computation of race($P, Q$) in rule (Com) becomes redundant. Two single-threaded pivotable processes never block each other.

Pivotable process cannot offer a clock action and exhibit reduction at the same time. This means that in this class of processes, clocks and reductions are sequentially scheduled.

**Proposition 23 (Clock Maximal Progress).** Suppose $P$ is coherent and pivotable. If $\sigma \in iA(P)$ then $P$ is in normal form, i.e., there is no reduction $P \xrightarrow{\tau} P'$.

Prop. 23 can be seen as saying that in pivotable processes all clocks take lowest precedence. As a result, clock transitions satisfy maximal progress, i.e., a clock is only enabled on normal forms, i.e., if there is no reduction possible. Thus clocks behave like time steps in the standard timed process algebras [18, 11]. More importantly (Thm. 12), all reductions are confluent. So, a pivotable process, no matter in which order the reductions are executed, when it terminates, it computes a unique normal form. At this point it either stops if there is no clock possible, or it offers a clock step (pausing) to a continuation process from which a new normal form is produced. In this way, coherent pivotable processes correspond to synchronous streams.

It remains to be seen how we can obtain coherent processes systematically by construction. The following Thm. 24 identifies a set of closure operators for coherent processes based on policy-conformance. This is our main theorem that summarises Propositions 60–66 (Appendix), which provide in CCS$^\text{spt}$ a generalisation of Milner’s Confluence Class, Prop. 15-17 in [27].
XX:14 Strong Priority and Determinacy in Timed CCS

► **Theorem 24** (Milner's Confluence Class Generalised).

(1) (Idling) $0 \Vdash \pi$ for all policies $\pi$.

(2) (Rendezvous Prefix) If $Q \Vdash \pi$, then for every $\ell \in \mathbb{R}$ we have $\ell:H.Q \Vdash \pi$ if $\ell \in H \subseteq \{\ell' | \ell' \rightarrow \ell \in \pi\}$.

(3) (Clock Prefix) If $Q \Vdash \pi$ and clock $\sigma \in \mathcal{C}$, then $\sigma:H.Q \Vdash \pi$ if $H \subseteq \{\beta | \beta \rightarrow \sigma \in \pi\}$.

(4) (Choice) If $P_1 \Vdash \pi_1$ and $P_2 \Vdash \pi_2$ and for all pairs of initial transitions $P \xrightarrow[\bar{F}_1]{\alpha_1} H_1$, $P_1$ and $P \xrightarrow[\bar{F}_2]{\alpha_2} H_2$, $P_2$ such that $\alpha_1 \neq \alpha_2$ as well as $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$. Then $P_1 + P_2 \Vdash \pi$ if $\pi_1 \subseteq \pi$ and $\pi_2 \subseteq \pi$.

(5) (Parallel) If $Q \Vdash \pi$ and $R \Vdash \pi$ where $\pi \setminus \mathcal{R}$ is a pivot policy, then $(Q|R) \Vdash \pi$.

(6) (Hiding) If $Q \Vdash \pi$ and $\sigma \rightarrow \ell \in \pi$ for all $\sigma \in L$ and $\ell \in \pi$, then $Q/L \Vdash \pi$.

(7) (Restriction) If $Q \Vdash \pi$ and $\pi$ precedence-closed for $L \cup \bar{L}$, then $(Q \setminus L) \Vdash \pi \setminus L$.

The theorem is the main result of the paper, namely that under a suitable “policy decoration”, a process can be run deterministically in the scheduled SOS semantics of CCS$^{spt}$.

► **Example 25.** To give a concrete example of the property stated by the above theorem, let's revisit Ex. 10: the processes A, B, R, O, T are all coherent and conform to the pivot policy $\pi_{ABRO}$ with precedences (ignoring the clock, so $\pi \setminus \mathcal{R} = \pi$) $k_s \rightarrow \bar{t}$, $s \rightarrow \bar{t}$, $k_x \rightarrow \{k_x, x\}$ for $x \in \{a, b, s, t\}$ and $\ell \rightarrow \ell$ for $\ell \in \{r, a, b, \bar{s}, t, \bar{t}, \bar{\sigma}\}$. Thus, by Thm. 24(5), their composition satisfies $A|B|R|O|T \Vdash \pi_{ABRO}$. Since the policy is also precedence-closed for $\{s, t, \bar{s}, \bar{t}\}$, we have $ABRO \Vdash \pi'_{ABRO}$ by Thm. 24(3,7), where $\pi'_{ABRO} = \pi_{ABRO} \setminus \{s, t\}$.

Note that, specifically, Thm. 24(5) is our replacement of Milner's notion of confluent composition $(P|Q) \setminus L$. Finally, to highlight our claim that we extend the classical result, we offer the following definition and conjecture to catch Milner's setting of CCS in CCS$^{spt}$.

► **Definition 26** (Milner's Confluence Class). Milner's confluence class CCS$^{cc} \subseteq P$ is the set of processes $P$ such that for all derivatives $Q$ of $P$, if $Q \xrightarrow[\bar{E}]{\alpha} H Q'$, the following holds:

■ If $\alpha \neq \tau$ then $H = \{\alpha\}$ and $\alpha \notin i\bar{A}^*(E)$.

■ If $\alpha = \ell | \bar{\ell}$ then $H = \{\ell\}$ and $\{\ell, \bar{\ell}\} \cap i\bar{A}^*(E) = \{\ell\}$.

► **Conjecture 1** (Milner's Confluence Class is Coherent). For all $P, Q \in \text{CCS}^{cc}$:

■ *P is coherent iff P is confluent.*

■ *A transition of P is c-enabled iff it is admissible.*

■ If $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}$ and $\overline{\mathcal{L}(P)} \cap \overline{\mathcal{L}(Q)} = L \cup \bar{L}$, then $(P|Q) \setminus L \in \text{CCS}^{cc}$.

5 Further work

We list in spare order some possible future works:

■ We plan to study the interaction of our notion of coherence with forms of congruence (static, dynamic and interaction laws in Milner's jargon) and notions of bisimulation.

■ We plan to generalise the interaction model of CCS$^{spt}$ to synchronisation algebras permitting action fusion in the spirit of Milner's ASCCS and Austry and Boudol's Meije (see [26, 3]).

■ Thm. 24 suggests using policies as types. Among possible type disciplines we just mention: behavioural type systems, including session-types to capture rendezvous interactions; intersection-types, including non-idempotent ones to characterise termination and resources awareness, and linear-types to model consuming resources.
- C-actions are somewhat related with continuation passing style, and, in some sense they are more powerful because they permit a “forecast” analysis of all possible future actions: studying this relation, possibly in relation with abstract interpretation techniques, would be worth of study.

- Clocks are unordered in $CCS^{spt}$: introducing a partial order could be an interesting, although economic and fine grained, way to reason about time and time priorities.
References

1 J. Aguado, M. Mendler, R. v. Hanxleden, and I. Fuhrmann. Grounding synchronous deterministic concurrency in sequential programming. In Proceedings of the 23rd European Symposium on Programming (ESOP'14), LNCS 8410, pages 229-248, Grenoble, France, April 2014. Springer.

2 R. M. Amadio. A synchronous pi-calculus. Inf. Comput., 205(9):1470-1490, 2007. URL: https://doi.org/10.1016/j.ic.2007.02.002, doi:10.1016/J.IC.2007.02.002.

3 D. Austry and G. Boudol. Algèbre de processus et synchronisation. Theor. Comput. Sci., 30:91-131, 1984.

4 G. Barrett. The semantics of priority and fairness in OCCAM. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proc. MFPS'89, 1989.

5 G. Berry. The Constructive Semantics of Pure Esterel. Draft Book, 1999. ftp://ftp-sop.inria.fr/esterel/pub/papers/constructiveness3.ps.

6 G. Berry. The Foundations of Esterel. In Proof, Language and Interaction: Essays in Honour of Robin Milner, pages 425-454. MIT Press, 2000.

7 G. Berry and G. Boudol. The chemical abstract machine. Theor. Comput. Sci., 96(1):217-248, 1992. URL: https://doi.org/10.1016/0304-3975(92)90185-I, doi:10.1016/0304-3975(92)90185-I.

8 R. Bocchino, V. Adve, S. Adve, and M. Snir. Parallel programming must be deterministic by default. In Proceedings of the First USENIX conference on Hot topics in parallelism, pages 4-4, 2009.

9 F. Boussinot and R. De Simone. The SL synchronous language. IEEE Transactions on Software Engineering, 22(4):256-266, 1996.

10 J. Camilleri and G. Winskel. CCS with priority choice. Information and Computation, 116(1):26-37, 1995.

11 R. Cleaveland, G. Lüttgen, and M. Mendler. An algebraic theory of multiple clocks. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the International Conference on Concurrency Theory CONCUR'97, pages 166-180. Springer, 1997. LNCS 1243.

12 V. Dieckert and G. Rozenberg, editors. The Book of Traces. World Scientific, 1995.

13 S. A. Edwards. On determinism. In M. Lohstroh et. al., editor, Lee Festschrift, pages 240-253. Springer, 2018.

14 P. Le Guernic, T. Goutier, M. Le Borgne, and C. Le Maire. Programming real time applications with SIGNAL. In Proceedings of the IEEE, volume 79, pages 1321-1336. IEEE Press, September 1991.

15 M. Mendler H. R. Andersen. An asynchronous process algebra with multiple clocks. In D. Sannella, editor, In Proc. ESOP'94, pages 58-73, 1994.

16 N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305-1320, September 1991.

17 D. Harel, A. Pnueli, J. Pruzan-Schmidt, and R. Sherman. On the formal semantics of Statecharts. In Logic in Computer Science (LICS'87), pages 54-64. IEEE Press, 1987.

18 M. Hennessy and T. Regan. A process algebra for timed system. Information and Computation, 117:221-239, 1995.

19 C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. 256 pages.

20 C. D. Kloos and P. Breuer, editors. Formal Semantics for VHDL. Kluwer, 1995.

21 J. W. Klop. Combinatory reduction systems. PhD thesis, Univ. Utrecht, 1980.

22 L. Kuper and R. Newton. Lvars: lattice-based data structures for deterministic parallelism. In Functional High-Performance Computing, page 71-84, New York, NY, USA, 2013. ACM.

23 E. A. Lee. The problem with threads. Computer, 39(5):33-42, 2006.

24 G. Lüttgen, M. von der Beeck, and R. Cleaveland. Statecharts via process algebra. In CONCUR '99: Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 399-414. Springer, 1999.
25 S. Marlow. Parallel and concurrent programming in haskell. In *CEFP 2011*, pages 339–401, 2012.

612

613

26 R. Milner. Calculi for synchrony and asynchrony. *Theor. Comput. Sci.*, 25:267–310, 1983. URL: https://doi.org/10.1016/0304-3975(83)90114-7, doi:10.1016/0304-3975(83)90114-7.

614

615

27 R. Milner. *Communication and Concurrency*. Prentice Hall, 1989.

616

28 R. Milner. *Communicating and mobile systems - the Pi-calculus*. Cambridge University Press, 1999.

617

618

29 R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I. *Inf. Comput.*, 100(1):1–40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4, doi:10.1016/0890-5401(92)90008-4.

619

620

621

30 R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, II. *Inf. Comput.*, 100(1):41–77, 1992. URL: https://doi.org/10.1016/0890-5401(92)90009-5, doi:10.1016/0890-5401(92)90009-5.

622

623

624

31 X. Nicollin and J. Sifakis. The algebra of timed processes, ATP: theory and application. *Inf. Comput.*, 114(1):131–178, 1994. URL: https://doi.org/10.1006/inco.1994.1083, doi: 10.1006/INCO.1994.1083.

625

626

627

32 B. Norton, G. Luettgen, and M. Mendler. A compositional semantic theory for component-based synchronous design. In R. Amadio and D. Lugiez, editors, *Int’l Conf. on Concurrency Theory (CONCUR’2003)*, pages 461–476, Marseille, September 2003. Springer LNCS 2761.

628

629

630

33 I. Phillips. CCS with priority guards. In K. G. Larsen and M. Nielsen, editors, *Proc. Concur 2001*, pages 305–320, 2001.

631

632

34 G. D. Plotkin. The origins of structural operational semantics. *J. Log. Algebraic Methods Program.*, 60-61:3–15, 2004. URL: https://doi.org/10.1016/j.jlap.2004.03.009, doi: 10.1016/J.JLAP.2004.03.009.

633

634

635

35 G. D. Plotkin. A structural approach to operational semantics. *J. Log. Algebraic Methods Program.*, 60-61:17–139, 2004.

636

637

36 V. Natarajan R. Cleaveland, G. Lüettgen. *Handbook of Process Algebra*, chapter Priority in Process Algebra. Elsevier, 2001.

638

639

37 K. Schneider. The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, December 2009.

640

641

642

38 Esterel Technologies. The Esterel v7 reference manual version v7_30 – initial IEEE standardization proposal. Technical report, Esterel Technologies, 679 av. Dr. J. Lefebvre, 06270 Villeneuve-Loubet, France, November 2005.

643

644

645

39 S.H. Unger. Asynchronous sequential switching circuits with unrestricted input changes. *IEEE Transactions on Computers*, C-20(12):1437–1444, 1971. doi:10.1109/T-C.1971.223155.

646

647

40 L. G. Valiant. A bridging model for parallel computation. *Commun. ACM*, 33(8):103–111, 1990. URL: https://doi.org/10.1145/79173.79181, doi:10.1145/79173.79181.

648

649

41 R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, and O. O’Brien. SCCharts: Sequentially Constructive Statecharts for safety-critical applications. In *Proc. PLDI’14*, Edinburgh, UK, June 2014. ACM.

650

651

652

A From Asynchronous Priorities to Synchronous ones, via Clocks

653

This rather informal section gives to the curious reader a nice view of our personal pilgrimage of previous work looking at reaching more control and determinism in asynchronous process algebra. This trip lead us to consider adding clocks to the previous literature and reach confluence in a synchronous setting.

654

655

656

657
<figure><img src="image_6.png" /><figcaption>■ **Figure 4** Symmetric Choice. The final outcome, in states ③ and ④, is non-determinate because it depends on the order of read and write. The continuations states are $S' \stackrel{\text{def}}{=} r.S'$ and $S'' \stackrel{\text{def}}{=} r.S'' + e.S''$. For confluence, the error state ③ should permit a (delayed) read to move forward and (eventually) meet with state ④, indicated by the dashed red arrow. However, this is not in general guaranteed.</figcaption></figure>

## A.1 CCS with (Weak) Priorities

Let us look in more detail on how a precedence mechanism such as “write-before-read” might be derived from the classical priorities studied for CCS. As a simple example, suppose $S$ is a (synchronous write, asynchronous read) memory cell that can be read at any time offering the read action $r$, but only be written once with the write action $w$. Ignoring data values, the cell would be modelled in plain CCS by the equations $S \stackrel{\text{def}}{=} w.S' + r.S''$ where $S' \stackrel{\text{def}}{=} r.S'$ and $S'' \stackrel{\text{def}}{=} r.S'' + e.S''$. Initially, memory cell $S$ is empty and offers a choice between a read action $r$ and a write action $w$. If the write action is performed, the cell receives a value and changes to state $S'$. In this filled state $S'$, only read actions are admissible to access the stored value, the state does not change. When the read action is executed on the empty cell $S$, however, the continuation state is $S''$ which represents an error state. In the error state $S''$ only a read or an error action $e$ is possible, but no write and the cell remains in error. Observe that only the read action is always admissible in both states $S$ and $S'$, while the write is admissible only in state $S$. If $S$ is put in parallel with a reader offering $\bar{r}$ and a writer offering $\bar{w}$, then the final state of $S$ depends on the order between the $\bar{r}$ and $\bar{w}$ actions. If we synchronise with the external sequence $\bar{r}.\bar{w}$ on $S$ where the read action is first, the writer gets blocked on the error state $S''$, while if we exercise $\bar{w}.\bar{r}$ where the write action is first, both can proceed and we obtain filled state $S'$. In term rewriting system jargon [21] this is called “critical pairs”.

Formally, let $R \stackrel{\text{def}}{=} \bar{r}.0$ be a reader process with a single read and $W \stackrel{\text{def}}{=} \bar{w}.0$ the writer with a single write, both terminating in the empty behaviour $0$. Then, according to the operational semantics of CCS, we have the two execution sequences $R \mid S \mid W \xrightarrow{\tau} 0 \mid S'' \mid W$ and $R \mid S \mid W \xrightarrow{\tau} R \mid S' \mid 0 \xrightarrow{\tau} 0 \mid S' \mid 0$, where both configurations $0 \mid S'' \mid W$ and $0 \mid S'' \mid 0$ are distinct normal forms, in the sense that no reductions are possible anymore. This is pictorially illustrated in Fig. 4. Observe that the behaviour is not only *non-deterministic* in the sense that there is more than one scheduling sequence. It is also non-determinate as the final outcome depends on the scheduling decisions.

Among many CCS extension with priorities, we looked the one of Camilleri and Winskell [10], named CCS$^{CW}$ in the sequel. CCS$^{CW}$ provides a *prioritised choice* operator $Q \stackrel{\text{def}}{=} \alpha_1.Q_1 \vdash \alpha_2.Q_2$ called “prisum” that gives the action $\alpha_1$ priority over $\alpha_2$ and blocks the second prefix $\alpha_2$ in case $\alpha_1 = \alpha_2$. Such priorities help us resolve the issue. The problem with non-determinism originates from the preemptive behaviour of the write-read choice $w.S' + r.S''$. It permits the read and the write actions to compete with each other for the next state of the process
S. In data-flow and functional programming, we resolve the conflict by making the write action take precedence over the read one. First, the data-flow variable must be written by the producer process, then it can be read by the consumers, if any. This “write-before-read” scheduling policy is a prioritised choice, represented in CCS<sup>CW</sup> as $S \stackrel{\text{def}}{=} w.S' \vdash r.S''$ in which the prisum $\vdash$ operator enforces a precedence from left to right. The store S is willing to engage in a read action r (to the right of $\vdash$) only if the environment does not offer a write w (on the left of $\vdash$) at the same time, concurrently.

Another important study in the endeavour of adding priorities to CCS is the work of Phillips [33]. In Phillips’ extension of CCS with priority guards, referred to as CCS<sup>Ph</sup>, the previous behavior is expressed by $S \stackrel{\text{def}}{=} \{ }:w.S' + \{w\}:r.S''$, where each action is pre-annotated by a set of actions that take priority. Process S will synchronise with the reader process R to move to the error state $S''$ with guarded action $\{w\}:r$. The priority guard $\{w\}$ states that this can only happen if the environment does not offer a write w. Otherwise, the only action available is $\{ }:w$ which makes the cell move into state $S'$. The write action has an empty guard and so cannot be blocked. If both $\overline{w}$ and $\overline{r}$ are offered concurrently, then only the higher-prioritised write action $\overline{w}$ will go ahead.

The standard way to implement this scheduling in prioritised CCS is via a transition relation that keeps track of blocking information. In line with the approaches of [10, 33, 36], let us write $P \xrightarrow{\alpha} H P'$ to denote that process P can engage in an action $\alpha$ to continue as $P'$, provided the concurrent environment does not offer any action from H. We will call H the blocking set of the transition. In Plotkin’s SOS, the (selected) rules for prefix and choice in CCS<sup>CW</sup> are the following<sup>4</sup>:

$$ \frac{\frac{P \xrightarrow{\alpha} H P'}{\alpha.P \xrightarrow{\alpha} \{\}} P} {P \vdash Q \xrightarrow{\alpha} L P'} (PriSum_1) \qquad \frac{\frac{Q \xrightarrow{\alpha} H Q'}{P \vdash Q \xrightarrow{\alpha} H \cup iA(P) Q'} \tau, \alpha \notin iA(P)} {PriSum_2} $$

where $iA(P)$ (defined formally later) informally represents the set of initial actions of P that are offered by P in some environment and $\vdash$ is the priority sum defined by CCS<sup>CW</sup>. From rule (Act), individual prefixes generate transitions without any blocking constraints. Rules (PriSum<sub>1</sub>) and (PriSum<sub>2</sub>) describe how the transitions of a choice $P \vdash Q$ are obtained from the transitions of P and of Q: more in details, rule (PriSum<sub>1</sub>) lets all transitions of the higher-prioritised process P pass through to form a transition of the choice $P \vdash Q$ without restriction. This is different for Q, where, according to rule (PriSum<sub>2</sub>), an action of the lower-prioritised process Q can only be executed, and thus P preempted by it, if P does not have an initial silent action and if it does not offer the same action $\alpha$, already. All initial actions of P are added to the blocking set Q’s transition. This will ensure that these get blocked in concurrent contexts in which P has a communication partner. The blocking sets take effect in the rules for parallel composition displayed below:

$$ \frac{\frac{P_1 \xrightarrow{\alpha_1} H_1 P'_1 \quad H_1 \cap \overline{iA}(P_2) = \{\}}{P_1 | P_2 \xrightarrow{\alpha_1} H_1 P'_1 | P_2} (Par_1)} {P_2 \xrightarrow{\alpha_2} H_2 P'_2 \quad H_2 \cap \overline{iA}(P_1) = \{\}} (Par_2) $$

<footnote n="4">⁴ For the fragment of CCS<sup>CW</sup> that we are considering, the precise connection is the following: $\vdash_R P \xrightarrow{\alpha} P'$ in CCS<sup>CW</sup> iff R is a subset of out-actions and there is a subset L of in-actions such that $P \xrightarrow{\alpha} H P'$ and either $\alpha$ is an out-action and $H = \{\}$ or $\alpha$ is an in-action with $\overline{\alpha} \in R$ and $R \cap \overline{H} = \{\}$.</footnote>
<figure><img src="image_7.png" /><figcaption>■ **Figure 5** Prioritised Choice. The read-write data race on memory cell *S* resolved by scheduling priority. The write takes precedence over the read, indicated by the dashed arrow. This removes the top left transition labelled τ: {w}. Since there is only one execution path, the system is deterministic. The continuations states *S'*<sub>def</sub> = r.S' and *S''*<sub>def</sub> = r.S'' + e.S'' of the cell are the same as in Fig. 4.</figcaption></figure>

$$
\frac{
  \begin{array}{ccccc}
    P_1 \xrightarrow{\alpha_1} H_1 & P'_1 & P_2 \xrightarrow{\alpha_2} H_2 & P'_2 & \alpha_1 = \overline{\alpha}_2 & H_1 \cap \overline{\mathrm{iA}}(P_2) = \{\} & H_2 \cap \overline{\mathrm{iA}}(P_1) = \{\}
  \end{array}
}{
  P_1 \mid P_2 \xrightarrow{\tau} H_1 \cup H_2 \mid P'_1 \mid P'_2
} \quad (\mathrm{Par}_3)
$$

More in details, rules (Parᵢ) for *i* ∈ {1, 2} define an action αᵢ by P₁ | P₂ offered in one of the sub-processes Pᵢ. Such is enabled if the competing concurrent process P₃₋ᵢ has no initial action that is in the blocking set Hᵢ of action αᵢ, i.e. when the condition Hᵢ ∩ iA(P₃₋ᵢ) = {} is satisfied. Rule (Par₃) implements the synchronisation between an action α₁ in P₁ and the associated matching action α₂ = α₁, originating from P₂. The side-condition is the same: each process Pᵢ only accepts the matching action call from P₃₋ᵢ if it does not offer any action that blocks action αᵢ. Let us see how this blocking semantics works for our running example of a write-once memory cell, where we now enforce a write-before-read priority on the empty cell S: S<sub>def</sub> = w.S' ⊲ r.S'' and S'<sub>def</sub> = r.S' and S''<sub>def</sub> = r.S'' + e.S''. The cell S has two potential transitions that can be fired, namely

$$
\frac{
  \frac{
    \overline{w.S' \xrightarrow{w} \{\} S'} \quad (\text{Act})
  }{
    S \xrightarrow{w} \{\} S' \quad (\text{PriSum}_1)
  }
  \quad \text{or}
  \quad
  \frac{
    \overline{r.S'' \xrightarrow{r} \{\} S''} \quad (\text{Act})
  }{
    S \xrightarrow{r} \{w\} S'' \quad (\text{PriSum}_2)
  }
}{
  \tau, r \notin iA(w.S')
} \quad (\text{PriSum}_2)
$$

considering that iA(w.S') = {w}. The latter transition synchronises with the reader process' 
$\bar{r}$ transition to give $R | S \xrightarrow{\tau} \{w\} 0 | S''$ as verified by the derivation

$$
\frac{
  \overline{R \xrightarrow{\tau} \{0\} 0} (\text{Act})
  \quad
  \overline{S \xrightarrow{r} \{w\} S''} (\text{Act})
  \quad
  \{\} \cap \overline{i\mathcal{A}}(S) = \{\}
  \quad
  \{w\} \cap \overline{i\mathcal{A}}(R) = \{\}
}{
  R | S \xrightarrow{\tau} \{w\} 0 | S''
} \quad (\text{Par}_3)
$$

in which the side-conditions {w} ∩ iA(R) = {w} ∩ {r} = {} and {} ∩ iA(S) = {} of rule (Par₃)
are satisfied. This is fine since a single reader should be able to access the store, as long as
there is no conflicting write. Note that the resulting silent transition is guarded by the write
action w to record this constraint. Now if we add the writer process, too, then we get stuck.
The writer's initial action w̄ ∈ iA(W) conflicts with the silent transition. The execution in
the context E = [·] | W is blocked by rule (Par₁), because {w} ∩ iA(W) = {w} ∩ {w} ≠ {}.
The derivation tree 749

$$ \begin{array}{c} \overline{R \xrightarrow{\tau \rightarrow \{w\}} 0} (\text{Act}) \qquad \overline{\overline{r.S'' \xrightarrow{\tau \rightarrow \{w\}} S''}} (\text{Act}) \\ \qquad \overline{S \xrightarrow{\tau \rightarrow \{w\}} S''} (\text{PriSum}_2) \\ \hline \overline{R | S \xrightarrow{\tau \rightarrow \{w\}} 0 | S''} (\text{Par}_3) \qquad \begin{array}{l} \{w\} \cap \text{iA}(W) \neq \{w\} \end{array} \\ \hline \overline{R | S | W \xrightarrow{\tau \rightarrow \{w\}} 0 | S'' | W} (\text{Par}_1) \end{array} $$

where the side-conditions of (PriSum₂) and of (Par₃) are satisfied, blocks at side-condition of rule (Par₁) in red. On the other hand, the writing of S by W followed by the reading of S' by R can be derived, i.e., we have $R | S | W \xrightarrow{\tau \rightarrow \{w\}} R | S' | 0$ and $R | S' | 0 \xrightarrow{\tau \rightarrow \{w\}} 0 | S' | 0$. The derivation trees in the SOS are as follows 751 752 753 754

$$ \begin{array}{c} \overline{w.S' \xrightarrow{w \rightarrow \{w\}} S'} (\text{Act}) \\ \overline{S \xrightarrow{w \rightarrow \{w\}} S'} (\text{PriSum}_1) \\ \hline \overline{R | S \xrightarrow{w \rightarrow \{w\}} R | S'} (\text{Par}_2) \qquad \overline{W \xrightarrow{w \rightarrow \{w\}} 0} (\text{Act}) \\ \hline \overline{R | S | W \xrightarrow{\tau \rightarrow \{w\}} R | S' | 0} (\text{Par}_3) \qquad \overline{R \xrightarrow{\tau \rightarrow \{w\}} 0} (\text{Act}) \qquad \overline{S' \xrightarrow{\tau \rightarrow \{w\}} S'} (\text{Act}) \\ \hline \overline{R | S' | 0 \xrightarrow{\tau \rightarrow \{w\}} 0 | S' | 0} (\text{Par}_1) \\ \hline \overline{R | S' | 0 \xrightarrow{\tau \rightarrow \{w\}} 0 | S' | 0} (\text{Par}_3) \end{array} $$

where the blocking side-conditions of (Par₁), (Par₂) and (Par₃) are all trivially satisfied. The scheduling which resolves the non-determinism is depicted in Fig. 5. 756 757

## A.2 Asynchronous CCS with (Strong) Priorities is Confluent

Our example from the previous section shows how (weak) priority-based scheduling helps us to exercise control over the execution order in an asynchronous process calculus with rendez-vous communication. The surprising observation is that very little needs to be changed in the traditional notion of priority for CCS to achieve confluence. For this we need to look how to “tune” of the classical weak priorities for our purposes. Our fix will make the difference between (weak) priority-based and (strong) priority-based scheduling (see Def. 3). What we want is that every process using only strong priority satisfies the following weak local confluence property [21]. Suppose P admits two transitions to different states $P_1 \neq P_2$ that do not block each other, i.e., $P \xrightarrow{\alpha_1} H_1$ $P_1$ and $P \xrightarrow{\alpha_2} H_2$ $P_2$ such that $\alpha_1 \notin H_2$ and $\alpha_2 \notin H_1$. Then, each action $\alpha_i$ (for $i \in \{1, 2\}$) is still admissible in $P_{3-i}$, and there exist $P'$ and $H'_i \subseteq H_i$ such that $P_i \xrightarrow{\alpha_3 - i} H'_i$ $P'$. The assumption $\alpha_i \notin H_{3-i}$ uses the blocking sets to express non-interference between transitions. Then, our weak<fnref n="5" /> local confluence expresses a weak “diamond property” stating that every diverging choice of non-interfering transitions immediately reconverges. The subset inclusions $H'_i \subseteq H_i$ ensure that delaying an admissible action does not introduce more chances of interference. 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773

### A.2.1 Fix 1

The standard notion of priority for CCS, as implemented in CCS<sup>CW</sup> or CCS<sup>Ph</sup>, of course was not designed to restrict CCS for determinism but to extend it conservatively to be able to

<footnote n="5">⁵ In the pure λ-calculus the diamond property holds for β-reduction without any assumptions. We use the term “weak” confluence, because of the side-condition of non-interference.</footnote>
express scheduling control. Even in the fragment of CCS<sup>CW</sup> where all choices are prioritised, weak confluence fails. For instance, although our memory cell S behaves deterministically for a single reader R and a single writer W, in the context $E \stackrel{\text{def}}{=} W_1 | [\cdot] | W_2$ of two writers $W_i \stackrel{\text{def}}{=} \bar{w}.W'_i$, it creates a race. The two writers compete for the single write action on S and only one can win. Using the operational semantics of CCS<sup>CW</sup> we can derive the (non-interfering) transitions $W_1 | S | W_2 \xrightarrow{\tau} \{\} W'_1 | S' | W_2$ and $W_1 | S | W_2 \xrightarrow{\tau} \{\} W_1 | S' | W'_2$. Still, the two outcomes of the divergence are a critical pair that have no reason to reconverge $W'_1 | S' | W_2 \to P'$ and $W_1 | S' | W'_2 \to P'$ if $W'_i$ are arbitrary behaviours. To preserve confluence we must block the environment from consuming the single prefix $w.S'$ twice. The problem is that the synchronisations $W_1 | S \xrightarrow{\tau} H_1 W'_1 | S'$ and $S | W_2 \xrightarrow{\tau} H_2 S | W'_2$ have empty blocking sets $H_i = \{\}$ which does not prevent the second writer $W_{3-i}$ to be added in parallel. If $w \in H_i$, then the rules $(\text{Par}_{3-i})$ would automatically prevent the second reader. Now, suppose we extend the action rule (Act) to expose the singleton nature of a prefix, like by $(\text{Act}^+)$, $\alpha.P \xrightarrow{\alpha} \{\alpha\} P$ we would not only prevent a second concurrent writer but already a single writer. The transitions $W_1 \xrightarrow{\bar{w}} \{\bar{w}\} W'_1$ and $S \xrightarrow{w} \{w\} S'$ would not be able to communicate, violating both side-condition $\{\bar{w}\} \cap \bar{iA}(S) = \{\}$ and $\{w\} \cap \bar{iA}(W_1) = \{\}$ of $(\text{Par}_3)$. The issue is that in the setting of CCS<sup>CW</sup> (and CCS<sup>Ph</sup>, indeed) the blocking set $H$ of a transition $P \xrightarrow{\alpha} H P'$ expresses a priority rather than an interference. An action cannot take priority over itself without blocking itself. Therefore, in CCS<sup>CW</sup> (and CCS<sup>Ph</sup>) we always have $\alpha \notin H$. Here, we need to apply a weaker interpretation. The actions in $H$ only prevent $\alpha$ from synchronising with a matching $\bar{\alpha}$ in the environment, if they are executed in a *different* (and thus competing) prefix from the one that executes $\bar{\alpha}$. Actions in $H$ interfere with $\alpha$ in the sense that they are intial actions of $P$ sharing the same control thread in which $\alpha$ is offered. Thus, we want to avoid a situation in which the environment synchronises with $\bar{\alpha}$ in the presence of *another distinct* communication on some $\beta \in H$. For then we would have a race for the behaviour of the thread shared by $\alpha$ and $\beta$ in $P$.

To fix this, we need to refine the side-conditions $H_i \cap \bar{iA}(P_{3-i})$ in $(\text{Par}_3)$ to check not all initial actions $\bar{iA}(P_{3-i})$ but only those initial actions of $P_{3-i}$ that are competing with the matching transitions $P_1 \xrightarrow{\alpha_1} H_1 P'_1$ and $P_2 \xrightarrow{\alpha_2} H_2 P'_2$ with $\alpha_1 = \bar{\alpha}_2$, involved in the communication $P_1 | P_2 \xrightarrow{\tau} H_1 \cup H_2 P'_1 | P'_2$ that we want to protect. We fix this by refining the information exposed by a transition. More specifically, we extend each transition $P \xrightarrow{\alpha} H P'$ by the set $K$ of initial actions that are offered in competing prefixes of the same thread as $\alpha$ or by threads concurrent to the thread from which $\alpha$ is taken. Then, the set of all initial actions is simply $iA(P) = K \cup \{\alpha\}$. Let us call $K$ the *initial environment* of the transition. From the description, we expect the invariant that $H \subseteq K$.

**Remark 27.** Note that we cannot simply define $K \stackrel{\text{def}}{=} iA(P) - \{\alpha\}$, because $\alpha$ could be contained in $K$. For example, take $P \stackrel{\text{def}}{=} \alpha.0 | \alpha.0$, where $P \xrightarrow{\alpha} \{\alpha\} \alpha.0$. The blocking set is $H = \{\alpha\}$ since the prefix is volatile and must be protected from a competing consumptions. Also, we need $\alpha$ to be in the initial environment $K = \{\alpha\}$, because the transition's action $\alpha$ is offered a second time in a concurrent thread. This is different from the set $iA(P) - \{\alpha\} = \{\alpha\} - \{\alpha\} = \{\}$. This shows that we must compute the initial environment explicitly as an extra label with each transition.

Now we can reformulate the parallel rule as

$$ \frac{P_i \xrightarrow{\alpha_i} H_i P'_i \quad \alpha_1 = \bar{\alpha}_2 \quad H_i \cap \bar{K}_{3-i} = \{\} \quad \text{for } i \in \{1, 2\}}{P_1 | P_2 \xrightarrow{\tau} H_1 \cup H_2 P'_1 | P'_2} (\text{Par}_3^+) $$
<figure><img src="image_8.png" /><figcaption>Figure 6 The store $S$ in composition with a reader $\bar{r}.0$ and a delayed writer $d.0|\bar{d}.\bar{w}.0$. The behaviour has two incongruent final outcomes, a store $S''$ with error in state ⑤ and an error-free store $S$ in state ⑥. The transition system is not confluent. The reason is that transition labelled $\tau:\{w\}$ is admissible in state ④ but not anymore in state ②. A solution is to block the reading already in state ④. In other words, the priority blocking (write-before-read) that kicks in at state ② needs to be detected already at state ①. Again, all transitons are silent with labels omitted.</figcaption></figure>

and achieve the same as before but can accommodate the action rule ($Act^+$) that introduces a "reflexive precedence".

### A.2.2 Fix 2

In the previous subsection we have seen how priorities can be beneficial to approaching to a deterministic scheduling in an intrinsic non-deterministic process algebra. The priority blocking eliminates the competition between mutually pre-empting actions and the remaining independent actions naturally commute. Now another question naturally arises: "does this mean that if we replace the non-deterministic choice $P+Q$ by a prioritised choice, denoted by $P \nearrow Q$, do we obtain a determinate process algebra?" Indeed, we can show that in the "asynchronous" fragment of CCS, i.e. where all prefixes $\alpha.P$ are of form $\alpha.0$, confluence can be granted: On the contrary, in the "synchronous" fragment of CCS, where actions sequentially guard new actions, we run into a problem of non-monotonicity. A communication between prefixes may trigger new actions that block another communication that was enabled before. In other words, it is not guaranteed that independent actions remain admissible. As an example, in the above reader-writer scenario, the actions $a_i$ ($i \in \{1,2\}$) may become blocked in processes $P_3-i$. Now, consider a parallel composition $R|S^*|W^*$ in which a modified store $S^* \stackrel{\text{def}}{=} S|d.0$ offers another concurrent method action $d$ on the side in parallel. Let the writer $W^*$ be delayed by a synchronisation with this concurrent action $d$, i.e., $W^* \stackrel{\text{def}}{=} \bar{d}.W \stackrel{\text{def}}{=} \bar{d}.\bar{w}.0$. The scheduling sequences are depicted in Fig. 6. We can still derive $S|d.0 \xrightarrow{r|\{w,d\}} \{r,w\} S''|d.0$ but also $S|d.0 \xrightarrow{d|\{r,w\}} \{d\} S$. The reading synchronisation $R|S|d.0 \xrightarrow{\tau|\{w,d\}} \{\bar{r},r,w\} S''|d.0$ can now take place by ($Par_3$) before the write to give the following reduction sequence: $R|S|d.0|W^* \xrightarrow{\tau|\{w,d,\bar{d}\}} \{\bar{r},r,w\} S''|d.0|W^* \xrightarrow{\tau|\{r,e\}} \{d\} S''|W$. The first reduction is justified by rule ($Par_1$), because the side-condition $\{w\} \cap \bar{A}(W) = \{w\} \cap \{d\} = \{\}$ is satisfied. The blocking side-condition which only looks at the moment when the read is happening does not see the write action $\bar{w}$ by $W^*$ hidden behind its initial action $\bar{d}$. It lets process $R$ access and read the store $S$. As before, however, the following reduction sequence is allowed, too: $R|S|d.0|W^* \xrightarrow{\tau|\{\bar{r},r,w\}} \{d\} R|S|W \xrightarrow{\tau|\{\bar{r},r\}} \{w,\bar{w}\} R|S' \xrightarrow{\tau|\{w\}} \{\bar{r},r,w\} S'$ in which the
write action happens before the read action. This creates two diverging reduction sequences (incoherent schedules) in which the final store is $S'$ or $S''$, non-deterministically.

Our insight is that the blocking side-conditions of the standard Camilleri-Winskell theory [10], described above, are too weak in scheduling control for our purposes and to guaranteeing a weak Church-Rosser property [21]. The problem is that in the side-condition of rule $Par_2$ we are only looking at the initial actions of $Q$. This is why the read action is blocked out of state ② in Fig. 6 but not out of state ①. In state ① there is no pending initial write. The write action $\bar{w}$ only becomes initial when the parallel processes $\bar{d}.0 | d.\bar{w}.0$ have interacted on action $d$ and advanced together with a silent action $\tau$, i.e. $\bar{d}.0 | d.\bar{w}.0 \xrightarrow{\tau} 0 | \bar{w}.0$. In order to see that the read action $r$ blocked by $\{w\}$ out of state ① should not be enabled, we must follow all sequences of interactions that can possibly happen concurrently to the read. The read is to be blocked, because after one silent $\tau$-step, in the reachable configuration of state ②, the write action $w$ in the blocking set $\{w\}$ of a silent action, meets a matching initial partner $\bar{w}$.

This suggests a strategy to fix up the standard theory. We accumulate, along with the upper blocking set $H$ of a transition the following: a lower blocking set $L$ and the context of all concurrent processes $E$ that run in competition with the transition. From these we can find out what blocking actions might be generated after any number of silent actions. The initial environment $K$ of a transition then is $H \cup L \cup iA(E)$. This finally gives a transition relation of the form $P \xrightarrow{a/E} H \cup L P'$. The label $E$, called the reduction context, is accumulated in the parallel compositions of $P$. The rules (Act) and (PriSum$_i$) are the one presented above. Further, let $iA^\tau(E)$ be informally the set of all actions that can become initial along $\tau$-sequences from $E$, which obviously includes $iA(E)$ (formally defined later on). We will call the set $iA^\tau(E)$ the set of weak initial actions of $E$. The rules $(Par_1^*)$ and $(Par_2^*)$ need to be reformulated. Rule $(Par_1^*)$, propagating an action in a parallel composition, is as follows:

$$ \frac{P \xrightarrow{a/E} H \cup L P' \qquad E' = E \mid Q \qquad H \cap \overline{iA^\tau}(E') = \{\}}{P \mid Q \xrightarrow{a/E} H \cup L P' \mid Q} (Par_1^*) $$

Rule $(Par_2^*)$ is symmetric to $(Par_1^*)$. Rule $(Par_3)$, for the synchronisation of an action $\alpha$ and its co-action $\bar{\alpha}$ using these weak initial sets, is reformulated as follows:

$$ \frac{P \xrightarrow{a/E_1} H_1 \cup L_1 P' \qquad Q \xrightarrow{\bar{\alpha}/E_2} H_2 \cup L_2 Q' \qquad E = E_1 \mid E_2 \qquad \forall i. H_i \cap (\overline{iA^\tau}(E) \cup L_{3-i}) = \{\}}{P \mid Q \xrightarrow{\tau/E} H_1 \cup H_2 \cup L_1 \cup L_2 P' \mid Q'} (Par_3^*) $$

We are now ready to revisit our running example. By $(Par_2^*)$, since

$$ R \xrightarrow{\bar{r}/0} \{r\} \cup \{\} R' \text{ and } S \mid d.0 \xrightarrow{r/d.0} \{w,r\} \cup \{\} S'', \text{ we get } R \mid S \mid d.0 \xrightarrow{\tau/d.0} \{w,r\} \cup \{\} S'' \mid d.0. $$

The side-condition of $(Par_3^*)$ is satisfied since the “weak” initial action set (where $\tau$ actions are dropped) $iA^\tau(d.0) = \{d\}$. Thus, both $\{r\} \cap \overline{iA^\tau}(d.0) = \{\}$ as well as $\{w,r\} \cap \overline{iA^\tau}(d.0) = \{\}$. If now want to shunt this past the writer process $W^*$ using rule $(Par_1^*)$, then we get stuck. Since $d.0 | W^* \xrightarrow{\tau/0} \{d,\bar{d}\} \cup \{\} W$ and $\bar{w} \in iA(W)$, we find $\bar{w} \in iA^\tau(d.0 | W^*)$ and thus $\{w\} \cap \overline{iA^\tau}(d.0 | W^*) \neq \{\}$. Therefore, the side-condition of $(Par_1^*)$ is violated and the reading interaction of $R \mid S \mid d.0$ cannot be composed with $W^*$. This is what we want. The transition from state ② to state ③ in Fig. 6 is now blocked. On the other hand, the reduction $R \mid S \mid d.0 \xrightarrow{d/R} \{d\} \cup \{\} R \mid S$ can be composed with $W^* \xrightarrow{\bar{d}/0} \{\bar{d}\} \cup \{\} W$ via $(Par_3^*)$ to make a reduction $R \mid S \mid d.0 | W^* \xrightarrow{\tau/R} \{d,\bar{d}\} \cup \{\} R \mid S | W$. Regarding the side-condition, we
notice that the weak initial action set $i\mathbf{A}^{\tau}(R|S)$ of the reduction context is irrelevant, because it does not contain $d$ or $\bar{d}$. In configuration $R|S|W$ (state ② in Fig. 6), the reader $R$ cannot interact with $S$. The associated reduction $R|S|W \xrightarrow[\mathbf{W}]{\tau} \{r,w\} \cup \{\} S''|W$ is blocked by the reduction environment, because $w \in \overline{i\mathbf{A}^{\tau}(\bar{w}.W')}$. For our further discussion, let us call the proposed change in the side-conditions leading to $(Par_i^*)$ from $(Par_i^*)$ a process algebra with strong priorities<fnref n="6" /> and let's call the traditional process algebra with priorities, introduced by [10, 36], as process algebra with weak priorities.

As an intermediate step to implement our precedence-based scheduling, the previous example suggests we look at the weak initial actions for a process, given in the following definition.

**Definition 28 (Weak Initial Actions & Strong Enabling).** The set $i\mathbf{A}^{\tau}(P)$ of weak initial transitions is the smallest extension $i\mathbf{A}(P) \subseteq i\mathbf{A}^{\tau}(P)$ such that if $\alpha \in i\mathbf{A}^{\tau}(Q)$ and $P \xrightarrow{\tau} Q$ then $\alpha \in i\mathbf{A}^{\tau}(P)$. Let $\overline{i\mathbf{A}^{\tau}(P)} = \overline{i\mathbf{A}^{\tau}(P)}$. A transition $P \xrightarrow{\alpha} H$ is called strongly enabled if $H \cap (\overline{i\mathbf{A}^{\tau}(R)} \cup \{\tau\}) = \{\}$.

It is easy to see that $i\mathbf{A}(P) \subseteq i\mathbf{A}^{\tau}(P)$, so every strongly enabled transition is weakly enabled: as such, for free processes, the notions of weak and strong enabling coincide. Note also that enabling as a scheduling constraint is not monotonic under parallel composition. The enabledness property of a transition is not, in general, preserved when the process is placed into a concurrent context. If a reduction $P \xrightarrow[\mathbf{R}]{\tau} H$ $P'$ is enabled, then we know that $H \cap \overline{i\mathbf{A}(R)} = \{\}$ or $H \cap \overline{i\mathbf{A}^{\tau}(R)} = \{\}$, depending on what scheduling we choose. This means that the context $R$ cannot (weakly) generate a synchronisation with a blocking initial action. This does not mean that an extension $R|Q$ may not perhaps have $H \cap \overline{i\mathbf{A}(R|Q)} \neq \{\}$ or $H \cap \overline{i\mathbf{A}^{\tau}(R|Q)} \neq \{\}$. This happens if blocking actions come from $Q$ or, in the case of strong enabling, become reachable though the interactions of $R$ and $Q$. Then the parallel extension $P|Q$ does not permit a reduction $P|Q \xrightarrow[\mathbf{R}]{\tau} H$ $P'|Q$. As indicated by the examples of Sec. 3, strong enabling generates confluent reductions in the reflexive case, where rendez-vous actions have a unique sender and a unique receiver process. For multi-cast communication, i.e., non-irreflexive self-blocking c-actions, we need the even stronger notion of constructive enabling based on $\overline{i\mathbf{A}^*(R)}$ instead of $\overline{i\mathbf{A}^{\tau}(R)}$.

### A.2.3 Digression: Strong Priorities lead to Impredicativity Issues

On the face of it, strong priorities may seem rather a natural modification to make. However, they amount to a significant change of the game compared to the standard weak priorities presented in the literature. For they break the standard method of defining the transition relation inductively as the least relation closed under a finite set of production rules. The key problem is the logical cycle in the structural definition of the operational semantics: the rules to generate the transitions ensure $H \cap \overline{i\mathbf{A}^{\tau}(E)} = \{\}$, i.e., that none of the blocking actions $H$ matches with the transitively reachable initial actions of the reduction context $E$ which itself is extracted as a part of $P$.

Obviously, to compute $i\mathbf{A}^{\tau}(E)$ we need to know the full transition relation for $E$. In other words, the existence of a transition of a process $P$ depends on the absence of certain transitions of a certain part of process $P$. If $P$ is defined recursively or via repetition then

<footnote n="6">⁶ The terminology is suggested by the fact that strong priorities use weak initial sets as rule premises while weak priorities are based on strong initial sets. Rules are implications, so weakening the antecedent makes a rule logically stronger.</footnote>
the behaviour of a part of *P* might depend on the behaviour of *P* itself. Does such a self-referential semantical definition make sense at all? How do we ensure the absence of a Russell-paradox style relation, by defining a process *rec* *p*. *P* to have a transition to *P'* if it does not have a transition to *P'* for a suitable *P'*? Such would be plainly inconsistent at the meta-level, because it would not only define simply an empty transition relation<sup>7</sup>, but it would not define a unique semantic relation at all.

In the standard theory of weakly prioritised process algebra as described in the cited references of CCS with priorities, the problem does not exist, because the set of (strong) initial actions $i\mathcal{A}(E)$ can be determined by structural recursion on $E$ without any reference to the transition relation. Unfortunately, for strong prioritized process algebra as defined in this paper, this is not possible anymore. So, how do we make sense of transition-generating rules $(Par_i^*)$ that depend on negative premises? One option is to treat the negation in the side-condition $H \cap \overline{i\mathcal{A}^\tau}(E) = \{\}$ constructively rather than classically, say like negation in normal logic programming. This would amount to building a second independent (inductive) rule system to generate constructive judgements about the absence of weakly reachable transitions. Trouble is that there is no canonical semantics of constructive negation, even in logic programming<sup>8</sup>.

Some progress has been made for unifying the proposals in a game-theoretic and intuitionistic setting which works well for special situations like the constructive semantics of Esterel [5] or StateCharts [17]. However, playing with constructive negation at the meta-level will give a variety of semantics whose adequacy might be difficult to judge in practical application contexts.

A more perspicuous attack is to keep the classical set-theoretic interpretation but use an over-approximation $L \cap \overline{fi\mathcal{A}^*}(E) = \{\}$ where $fi\mathcal{A}^*(E) \supset i\mathcal{A}^\tau(E)$ is intuitively a superset of weakly reachable initial sender actions obtained from a relaxed transition relation, formally defined later in this paper. A natural over-approximation that can be defined independently is the “free speculative” scheduling that ignores all priorities. The stronger side-condition $L \cap \overline{fi\mathcal{A}^*}(E) = \{\}$ forces the absence of a blocking sender action under the worst-case assumption of priority-free scheduling. Obviously, this is sound but will have the effect that some programs block that could make progress under a tighter approximation of the sets $i\mathcal{A}^\tau(E)$. Between $fi\mathcal{A}^*(E)$ and $i\mathcal{A}^\tau(E)$ there be a whole range of different semantics that may or may not be equivalent to specific constructive semantics of negation. Exploring the range of options systematically will certainly be a worthwhile research exercise likely to cover much new ground in the theory of process algebras with priorities.

## A.3 Synchronous CCS with (Strong) Priorities and Clocks is Confluent

We argue that the use of priorities for determinacy calls for a combination of strong priorities with a second important concept that has been investigated in the literature before, but independently. This is the well-known notion of a *clock*, from Timed Process Algebras, like e.g. TPL [18] and PMC [15]. Intuitively, a clock $\sigma$ is a “broadcast action” in the spirit of Hoare’s CSP [19] that acts as a synchronisation barrier for a set of concurrent processes. It bundles each processes’ actions into a sequence of *macro-steps* that are aligned with each other in a lock-step fashion. During each macro-step, a process executes only a temporal slice of its total behaviour, at the end of which it waits for all other processes in the same *clock*

<footnote n="7">⁷ As an example consider the unguarded process *rec* *p*. *p* in the standard inductive theory. Its behaviour is well-defined as the empty transition relation.</footnote>

<footnote n="8">⁸ Different well-known semantics are negation-by-failure, stable semantics, supported model semantics.</footnote>
<figure><img src="image_9.png" /><figcaption>Figure 7 Strong priorities introduce confluence in scheduling.</figcaption></figure>

scope to reach the end of the current phase. When all processes have reached the barrier, they are released into the next round of computation.

This scheduling principle is well-known from computer hardware like sequential circuits [39] and VHDL [20], or synchronous languages like Esterel [5], Lustre [16], SCCharts [41], BSP [40], just to mention a few. For our purposes, clocks are the universal trick to break causality cycles in priority scheduling, when processes need to communicate with each other in iterated cycles (so-called *ticks* or *macro-steps*) while maintaining determinacy.

To get this off the ground we introduce a clock broadcast action $\sigma$ to separate each round of communication. We define the recursive processes $W \stackrel{\text{def}}{=} d.0 | \bar{d}.\bar{w}.\sigma.W$ and $R \stackrel{\text{def}}{=} \bar{r}.\sigma.R$ for one write and one read per macro-step. Assuming the content of the memory variable is reset for every tick, we can define $S$ as follows $S \stackrel{\text{def}}{=} w.S' + r:\{w\}.S'' + \sigma:\{w,r\}.S$ with $S' \stackrel{\text{def}}{=} r.S'' + \sigma:\{r\}.S'$ and $S'' \stackrel{\text{def}}{=} wCamera$. The clock always takes lowest priority among all other rendez-vous actions out of a state. The idea is that the clock should fire only if the system has stabilised and no other admissible data actions are possible. This is called maximal progress and it is a standard assumption in timed process algebras [18, 11]. The fairly standard rules for clock actions, inspired by timed process algebras are then:

$$ \frac{P \xrightarrow{\sigma}{R_1} L_1 P' \quad P \xrightarrow{\sigma}{R_2} L_2 P' \quad (L_1 \cup L_2) \cap \text{iA}^{\tau}(R_1 | R_2) = \{\}}}{\sigma.P \xrightarrow{\sigma}{0} \{\} P} \quad (\text{Clk}_1) \quad \frac{P | Q \xrightarrow{\sigma}{R_1 | R_2} L_1 \cup L_2 P' | Q'}{\text{Clk}_2} \quad (\text{Clk}_2) $$

Those two rules enforces global synchronisation and make the clock deterministic. As such, the evaluation of $R|S|W$ “prunes” all reductions that could lead to non confluent reductions. Fig. 7 shows how higher priorities can introduce determinism in scheduling. The importance of the clock $\sigma$ is that its associated synchronisation rule (Clk₂) enforces, in a quite natural way, the barrier explicitly in the SOS rather than making it an artefact of a specific synchronisation process, as such obliging the programmer to an extra effort. The fact that the broadcasting clock is hard-wired into the rules can now be exploited for the computation of the weak initial action sets, defined formally $\text{iA}^{\tau}(R)$. More precisely, we only need to predict the behaviour of $R$ for the current macro-step, i.e., up to the next synchronization of $\sigma$ by $R$. For a transition $P \xrightarrow{a} R' P'$ we know that all actions taking place after $\sigma$ in $R$ are definitely observed to happen in the next macro step and thus not in competition with the current action $a$ under blocking set $L$. In this fashion, the clock acts as a stopper sentinel for
prediction and evaluation of the blocking set $L$ relative to the reduction environment $R$. If every recursion is instantaneous, then the search space becomes finite.

As a final remark, for the purposes of this paper, adding synchrony and determinism in process algebras, we are not (and indeed we do not need to be) interested in higher-order calculi, like e.g. the π-calculus [29, 30], where processes are first-class objects, i.e. sent and received as a values, as in a!P.Q and a?x.(x|Q). In the next sections, we present the syntax, the structural operational semantics à la Plotkin, we set up all the definitions and the metatheory necessary to formally prove the claimed informal properties.

**B Examples, new and reloaded**

This section contains a number of reloaded and new examples in view of the definitions and results presented in the previous section.

**Note on Conservativity**

The weakly-enabled transitions of unclocked, free processes coincide with the semantics of genuine Milner's CCS [27], as stated in the following easy exercise.

► **Exercise 29** (On Def. 2). If P is unclocked and free, then a transition $P \xrightarrow{\alpha} H_Q$ is weakly enabled iff $P \xrightarrow{\alpha} Q$ is admissible, i.e., iff it is derivable in Milner's original SOS for CCS.

In fact, one can show that the semantics of weak enabling generates the theory of CCS$^{Ph}$ [33]. To be more precise, let us call a process $P$ *irreflexive* if no action prefix $\alpha:H.Q$ occurring in $P$ has $\alpha \in H$, i.e., blocks itself. In the semantics of CCS$^{Ph}$, such *self-blocking* prefixes do not contribute any transitions. Thus, CCS$^{Ph}$ captures a theory of irreflexive processes. We leave as a less easy exercise that all weakly enabled transitions between irreflexive processes are precisely the ones allowed in CCS$^{Ph}$.

► **Exercise 30** (On Def. 2). If P is unclocked and irreflexive, then a transition $P \xrightarrow{\alpha} H_Q$ is weakly enabled iff $P \xrightarrow{\alpha} P'$ is derivable in the operational semantics of CCS$^{Ph}$.

Thus, from the point of view of CCS$^{Spt}$, theories of CCS and CCS$^{Ph}$ correspond to theories of free and irreflexive processes, respectively, under weak enabling. Here we suggest two extension to this classical work. Firstly, we apply a stronger scheduling restrictions, called *strong enabling* (Def. 28 below) and *constructive enabling* (Def. 3 above) to achieve confluence and secondly we make use of self-loops to control sharing.

**Priorities and Scheduling**

► **Example 31** (On Def. 12). If $A \not\equiv B$ then $a.A + a.B$ is not coherent while $a:a.A|a:a.B$ is coherent. Conflicting choices on the same label in a single thread cannot be externally observed and thus cannot be deterministically scheduled via their externally observable properties. In coherent processes such choices are assumed to be resolved internally by each thread itself, rather than through the precedence relation. Note that the process $a:a.A+a:a.B$ in which the two action prefixes are self-blocking, is not coherent either. The reason is that the two identical (self-blocking) transitions lead to structurally distinct states $A \not\equiv B$. Thus, the confluence condition expressed in Def. 12 applies and $A$ and $B$ should be reconvergent with transitions $A \xrightarrow{a} Q'$ and $B \xrightarrow{a} Q'$. But this is not guaranteed for arbitrary $A$ and $B$. On
the other hand, a single self-blocking prefix $a:a.A$ is coherent. Without the self-blocking, $a.A$ is only coherent if process $A$ permits infinite repetition of $a$ as in $A \stackrel{\text{def}}{=} a.A$ or $A \stackrel{\text{def}}{=} a | A$.

The precedence relation cannot resolve the choice of a prefix with itself. The precedence relation can resolve the choice between distinct actions prefixes. For instance, if $a \neq b$ then $a.A+b.B$ is not coherent, for any $A$ and $B$. However, both $a:a.A | b:b.B$ and $a:a.A+b:\{a,b\}.B$ are coherent. In the former case, the actions are concurrently independent and so confluence occurs naturally. In the latter case, the choice is resolved by precedence: No reconvergence is required by coherence Def. 12 as the actions are interfering with each other. ◀

**Example 32 (On Normal form).** For the process $P_1 \stackrel{\text{def}}{=} (a.c | b.d | \bar{a} | \bar{b}) \setminus \{a,b\}$ we have $(a.c | d | \bar{a}) \setminus \{a,b\} \stackrel{\tau}{\leftarrow} P_1 \stackrel{\tau}{\rightarrow} (c | b.d | \bar{b}) \setminus \{a,b\}$ where the continuation processes $(c | b.d | \bar{b}) \setminus \{a,b\}$ and $(a.c | d | \bar{a}) \setminus \{a,b\}$ are not structurally equivalent. They are not even behaviourally equivalent. However, both reductions are concurrently independent and commute with each other. We can execute both rendezvous synchronisations $\tau = a | \bar{a}$ and $\tau = b | \bar{b}$ in any order, the process $P$ converges to a unique final outcome $(c | d) \setminus \{a,b\}$. Similarly, in the multi-cast process $P_2 \stackrel{\text{def}}{=} (a.c | a.d | \bar{a} | \bar{a}) \setminus \{a\}$ the reduction behaviour is not structurally deterministic but nevertheless generates a unique normal form. ◀

**Example 33 (On Sequentiality à la Esterel in CCS<sup>spt</sup>).** Like CCS, our calculus CCS<sup>spt</sup> does not have a generic operator for sequential composition as in Esterel. This is not necessary, because sequential composition can be coded in CCS by action prefixing and parallel composition. More precisely, a sequential composition $P;Q$ is obtained as a parallel composition $([P]|_t|t:Q) \setminus \{t\}$ where $[P]|_t$ is the process $P$, modified so when it terminates, then the termination signal $\bar{t}$ is sent. The signal $t$ will then trigger the sequentially downstream process $Q$. The operation $[P]|_t$ can be implemented by a simple (linear) syntactic transformation of $P$. In the same way we can detect termination of a parallel composition $P = P_1 | P_2$. Since a parallel terminates if both threads terminate, we can define $[P]|_t$ as follows

$$[P_1 | P_2]|_t \stackrel{\text{def}}{=} ([P_1]|_{s_1} | [P_2]|_{s_2} | s_1:s_1.s_2:s_2.\bar{t}) \setminus \{s_1, s_2\}$$

where $s_1$ and $s_2$ are fresh “local” termination signals. The “termination detector” $T_{seq} \stackrel{\text{def}}{=} s_1:s_1.s_2:s_2.\bar{t}$ first waits for $P_1$ to terminate and then for $P_2$, before it sends the signal $\bar{t}$ indicating the termination of the parallel composition. We could equally first wait for $P_2$ and then for $P_1$, if the difference is not observable from the outside. In cases where the termination detector needs to permit both processes $P_1$ and $P_2$ to terminate in any order, however, we need a different solution. We need to “wait concurrently” for $s_1$ or $s_1$, not sequentially as in $T_{seq}$. The obvious idea would be to use a confluent sum

$$T_{csum} \stackrel{\text{def}}{=} s_1:s_1.s_2:s_2.\bar{t} + s_2:s_2.s_1:s_1.\bar{t}$$

as discussed in Milner [27] (Chap. 11.4). This does not work, because the sum must explicitly unfold all possible orders in which the termination signals can arrive and thus again creates an exponential descriptive complexity. Interestingly, in CCS<sup>spt</sup> we can exploit precedence scheduling to obtain a robust and compositional solution. Consider the process $T_{par} \stackrel{\text{def}}{=} s.T_{par} + \bar{t}:\{s,\bar{t}\}$. It engages in an unbounded number of receptions on channel $s$ without changing its state. At the same time, it offers to send the termination signal $\bar{t}$, but only if the action $s$ is not possible. Under the weak enabling strategy, the composition $\bar{s} | \bar{s} | T$ will consume the two senders $\bar{s}$ and only then engage in $t$. In this way, we can use $T_{par}$ to detect the absence of $s$ which corresponds to the termination of the two environment processes $\bar{s} | \bar{s}$, in any order. The signal $s$ could be the shared termination signal of each
process $P_1$ and $P_2$ that is sent and consumed by $T_{par}$ if and when the process terminates. If we execute the parallel composition $P_1 | P_2 | T_{par}$ under constructive enabling, the termination signal $\bar{t}$ will not be sent until such time that both $P_1$ and $P_2$ have been able to send $s$ to $T$. From the scheduling point of view, the composition $P_1 | P_2$ acts like a counter that is initialised to 2, representing the number of potential offerings of $s$ initially in $P_1 | P_2$. It gets decremented each time one of $P_1$ or $P_2$ terminates. For instance, $0 | P_2$ and $P_1 | 0$ have one potential offering left, while $0 | 0$ has no more potential to send $s$. At this moment, the counter has reached 0 and $0 | 0 | T_{par}$ can take the $\bar{t}$ action and thereby send termination. In sum, there are two important observations here: First, we find that precedences with constructive enabling permits us to code sequential composition of Esterel in a compositional fashion. Second, the coding of Milner's confluent sum $T_{csum}$ is possible in CCS$^{pt}$ with linear descriptive complexity. ◀

The next example illustrates that the closure property for coherence of hiding (Thm. 14(6), see also Prop. 65) needs to require that the hidden clock must not take precedence over rendezvous actions.

► **Example 34 (On Clock-hiding).** The process $P \stackrel{def}{=} \sigma.A + a:\sigma.B | \sigma$ offers a choice of two transitions $P \xrightarrow{\sigma} \{\} A$ and $P \xrightarrow{a} \{\sigma\} B | \sigma$. These transitions interfere with each other so that the $\sigma$-transition blocks the $a$-transition under weak enabling, given that $\{\sigma\} \cap \overline{iA}(\sigma) = \{\sigma\} \neq \{\}$. Thus, $P$ is coherent. Note that any policy with $P \parallel \pi$ must have $\sigma \dashrightarrow a \in \pi$. This does not satisfy the side condition of Thm. 24(6). So we cannot conclude that $P/\sigma$ is coherent. Let us see what happens when the clock is hidden and thus generates a silent step. Indeed, hiding the clock, we obtain from rule *Hide* the two transitions

where the blocking set of the $a$-transition turns into $\{\sigma\} - \{\sigma\} = \{\}$. Now, because $\sigma$ is removed from the blocking set, the $a$-transition is even constructively enabled. Moreover, both the $\tau$-transition and the $a$-transition are interference-free. However, in general, there is no chance that we can find recovergent transitions $A/\sigma \xrightarrow{a} Q_1$ and $(B|\sigma)/\sigma \xrightarrow{\tau} Q_2$ with $Q_1 \equiv Q_2$. Thus, $P/\sigma$ is not coherent any more. ◀

The problem is this: One the one hand, the *Hide* rule closes the scope of a clock but one the other hand, it does not actually implement any blocking that comes from this clock inside the scope. Such can be implemented by a refined hiding rule that, like (*Com*), implements a “race test” and introduces a $\tau$ into the blocking set whenever there is a conflict:

$$ \frac{P \xrightarrow{\sigma} H Q \quad H' = H - \{\sigma\} \cup \{\tau \mid \sigma \in \overline{iA^*}(R) \cap H\}}{P/\sigma \xrightarrow{\sigma/\tau} H' Q/\sigma} \quad (Hide^*) $$

In this manner, the enabling check for the conclusion transition verifies that $\tau \notin H'$ and thus that $\sigma \notin \overline{iA^*}(R) \cap H$. In other words, if the local clock $\sigma$ is in $H$ (blocking the visible action $\alpha$) then the concurrent context $R$ inside the clock scope must not conflict with $\sigma$. Not surprisingly, *mutatis mutandis*, a similar refinement could be made to the restriction rule giving

$$ \frac{P \xrightarrow{\sigma} H Q \quad \alpha \notin \{\ell, \bar{\ell}\} \quad H' = H - \{\ell, \bar{\ell}\} \cup \{\tau \mid \ell \in \overline{iA^*}(R) \cap H\}}{P \setminus \ell \xrightarrow{\sigma} H' Q \setminus \ell} \quad (Restr^*) $$
In this paper we stick to the simpler versions (Hide) and (Restr) but conjecture that the side conditions on the policy in Thm. 24(6,7) can be lifted to show that for (Hide*) and (Restr*) the operations of hiding and restriction preserve coherence.

**Example 35 (Clock-hiding with built-in Scheduling Test).** Consider the process $P \stackrel{\text{def}}{=} \sigma.A + a:\sigma.B | b.\sigma$ where the local clock $\sigma$ also blocks the action $a$ by priority. But now the clock is guarded in $b.\sigma$ and so to become active for $P$, it needs the synchronisation with an external action $\bar{b}$. As in the previous example $P/\sigma$ would not be coherent. The extended hiding rule (Hide*) would generate the a-transition

$$P/\sigma \xrightarrow{\frac{a}{(b.\sigma)/\sigma}} \{\tau\} (B | b.\sigma) / \sigma \text{ from } P \xrightarrow{\frac{a}{b.\sigma}} \{\sigma\} A | b.\sigma.$$

The $\tau$ enters into the blocking set because of the race test which discovers that $\sigma \in \overline{iA}^*(b.\sigma) \cap \{\sigma\}$, where $\{\sigma\}$ is the blocking set of the a-transition in $P$. Hence, the a-transition of $P/\sigma$ is not (constructively) enabled anymore, which saves coherence. There is no requirement to exhibit any reconvergence for it. ◀

## Policies

**Example 36 (On coherence and pivotable processes).** The process $P_1 \stackrel{\text{def}}{=} a | \bar{b} | \overline{a:b} + b$ is coherent and pivotable with a policy $\pi$ such that $\pi \Vdash \bar{b} \dashv\vdash \overline{a}$ and $\pi \Vdash \bar{b} \diamond a$. The rendezvous synchronisation $\tau = a | \overline{a}$ is blocked by the presence of the offering $\bar{b}$ from a third thread. We have $P_1 \xrightarrow{\tau} \{b\} \bar{b}$, which is not weakly enabled, because $\{b\} \cap \overline{iA}(\bar{b}) \neq \{\}$. The blocking is due to the concurrent context $\bar{b}$ of the transition. For contrast, the process $P_2 \stackrel{\text{def}}{=} (a + \bar{b}) | (\overline{a:b} + b)$ is pivotable but not coherent. In our semantics, the synchronisation of $a$ and $\overline{a:b}$ in $P_2$ is blocked by the race test of rule (Com) which introduces $\tau$ into the blocking set $P_2 \xrightarrow{\tau} \{b, \tau\} 0$ because $\{b\} \cap \overline{iA}(a + \bar{b}) \notin \{\overline{a}\}$. This transition therefore is not weakly enabled, because of $\{b, \tau\} \cap (\overline{iA}(0) \cup \{\tau\}) \neq \{\}$. We can make the pivotable $P_1$ also coherent by forcing a sequential ordering between $a$ and $\bar{b}$ in the first thread, say $P_3 \stackrel{\text{def}}{=} a.\bar{b} | (\overline{a:b} + b)$, then the synchronisation is even strongly enabled $P_3 \xrightarrow{\tau} \{b\} \bar{b}$. If we introduce a precedence into the first thread, say $P_4 \stackrel{\text{def}}{=} (a:b + \bar{b}) | (\overline{a:b} + b)$, then we are also coherent but no longer pivotable. Like for $P_2$, the synchronisation $\tau = a | \overline{a}$ is blocked and not weakly enabled, because of the introduction of $\tau$ into the blocking set by the race condition of (Com). ◀

**Example 37 (On Coherent and Pivotable Processes).** The process $P_1 \stackrel{\text{def}}{=} \sigma + a:\sigma | \overline{a}$ is coherent and pivotable, with policy $\sigma \dashv\vdash a \in \pi$ and $\sigma \diamond \overline{a} \in \pi$. It has both $a, \overline{a} \in iA(P)$ but $\sigma \notin iA(P)$ since the clock is not offered by the parallel process $\overline{a}$. The synchronisation $\tau = a | \overline{a}$ can go ahead. On the other hand, the process $P_2 \stackrel{\text{def}}{=} \sigma + a:\sigma | \overline{a} + \sigma:\overline{a}$ has all three actions $\sigma, a, \overline{a} \in iA(P_2)$ initial. It is coherent but not pivotable. Since both $a$ and $\overline{a}$ are in a precedence relationship with $\sigma$, $P_2$ does not satisfy concurrent independence of $\sigma$ with neither $a$ nor $\overline{a}$. Formally, any policy $\pi$ for $P_2$ must have $\sigma \dashv\vdash a \in \pi$ and $\overline{a} \dashv\vdash \sigma \in \pi$ violating the pivot requirement that if $\sigma \dashv\vdash a \in \pi$, then $\sigma \diamond \overline{a} \in \pi$. The same is true of the process $P_3 \stackrel{\text{def}}{=} \sigma + (a:\sigma | \overline{a})$ which can perform both $\sigma$ and a (silent) reduction $\tau = \alpha | \overline{\alpha}$ that has $\sigma$ in its blocking set. ◀

An interesting special class of pivot policies are input-scheduled policies.

**Definition 38 (Input-scheduled Processes).** A policy $\pi$ is called input-scheduled if $\pi \subseteq \pi_{is}$ where $\pi_{is} = (L_{is}, \dashv\vdash_{is})$ given by alphabet $L_{is} = \mathcal{L}$ and precedence relation $\ell_1 \dashv\vdash \ell_2 \in \pi_{is}$ iff $\ell_1 = \ell_2$ or $\ell_1, \ell_2 \in \mathcal{A} \cup \mathcal{C}$. A process is input-scheduled if $P$ conforms to an input-scheduled policy.
<figure><img src="image_10.png" /><figcaption>(a) A Boolean Read-Write Memory with coherent states wAND₀ : mem and wAND₁ : mem.</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>(b) The mem ∪ prg Pivot Policy.</figcaption></figure>

Figure 8 A boolean memory process.

► **Example 39 (On Pivotable but not Input-scheduled Processes).** The process $a + b:c | \bar{a} + \bar{b}:\bar{a}$ is pivotable. It conforms to $\pi$ with precedences $c \dashv\vdash b \in \pi$ and $\bar{a} \dashv\vdash \bar{b} \in \pi$, while at the same time $\bar{c} \diamond \bar{b} \in \pi$ and $a \diamond b \in \pi$. However, assuming $a \neq b$, the process is not input-scheduled, because it has $\bar{a} \dashv\vdash \bar{b} \in \pi$ while $\bar{a} \diamond \bar{b} \in \pi_{is}$. The same is true of the process in Ex. 5. ◀

► **Example 40 (On Read/Write Process, reloaded).** Fig. 8 shows that the processes wAND_v conform to a policy mem with $w_i \dashv\vdash r_j \in \text{mem}$ for $i \neq j$ and $w_1 \dashv\vdash w_0 \in \text{mem}$. Obviously, mem is a pivot policy. The processes wAND_v are also coherent. One verifies by simple case analysis that for any derivative Q of wAND_v, if $Q \stackrel{\ell}{\rightarrow}_H Q'$ and $\ell \notin H$ then there is a repetition $Q' \stackrel{\ell}{\rightarrow}_H Q''$ with $H' = H$. This yields Def. 12. Secondly, suppose $Q \stackrel{\ell_1}{\rightarrow}_H Q_1$ and $Q \stackrel{\ell_2}{\rightarrow}_H Q_2$. Then, obviously, if $\ell_1 \neq \ell_2$, the two transitions are never interference-free, because of the choice of blocking sets which orders all summation prefixes in a linear precedence order. If $Q_1 \not\equiv Q_2$ then necessarily $\ell_1 \neq \ell_2$. Thus, Def. 12 is satisfied, too, for trivial reasons. So, the memory, which satisfies wAND_v $\Vdash$ mem, is pivotable.

Note that wAND_v is not a reflexive process, since none of its actions is self-blocking. We can put the memory in parallel with arbitrarily many writers and readers. Consider a parallel composition wAND_v | P where P is any single-threaded process that synchronises via w&#773;i for writing and r&#773;i for reading. Each writing action of P is a self-blocking prefix w&#773;i:w&#773;i.Q and each reading is a choice r&#773;1:r&#773;1.R&#773;1 + r&#773;0:r&#773;0.{r&#773;0, r&#773;1}.R&#773;0 where the continuation processes R&#773;0 and R&#773;1 are selected according to the content of the memory, by matching with the r&#773;0 action of wAND_0 or the r&#773;1 action of wAND_1. If the memory would offer both a synchronisation on r&#773;0 and r&#773;1 (which it does not), the reader would take the match on r&#773;1, because of the precedences. If Q, R&#773;0 and R&#773;1 follow the same principle, such a sequential program is a discrete process P that is coherent and conformant to the policy prg with r&#773;1 ---&rarr; r&#773;i &isin; prg and r&#773;0 ---&rarr; r&#773;0 &isin; prg. Now we observe that the union mem &cup; prg of policies is a pivot policy. Since wAND_v $\Vdash$ mem and P $\Vdash$ prg we have wAND_v $\Vdash$ mem &cup; prg as well as P $\Vdash$ mem &cup; prg. Then, by Prop. 64 we get

$$wAND_v | P \Vdash \mathrm{mem} \cup \mathrm{prg}$$

i.e., the composition is coherent and pivotable. In fact, we can put the memory in parallel with arbitrarily many sequential programs coherent for prg and the composition wAND_v | P_1 | P_2 | ... | P_n will be coherent for mem &cup; prg. In particular, all reductions will be
confluent under strong enabling. Technically, what happens is that first all writers of value 1, synchronising as $w_1 | \overline{w_1}$, will go ahead. Then all writers of 0, synchronising as $w_0 | \overline{w_0}$ become enabled. Only then the readers will be able to retrieve the final value via $r_0 | \overline{r_0}$ or $r_1 | \overline{r_1}$ rendezvous synchronisations. ◀

Observe that the pivot policy mem $\cup$ prg of Ex. 40 permits a choice (and precedence) between both the receiver actions $w_0$, $w_1$ but also between the sender actions $\overline{r_0}$, $\overline{r_1}$. As a result, the combined memory and program, which is coherent for mem $\cup$ prg, is not an input-scheduled process in the sense of Def. 38. This breaks the assumption on which the theory of classical prioritised process algebras like [10] or [36] are based. In reference to the former, Phillips writes:

> They [Camilleri and Winskel] decide to sidestep this question by breaking the symmetry in CCS between inputs and outputs, and only allowing prioritised choice on input actions. We feel that this complicates the syntax and operational semantics, and should not be necessary. [33]

Our example and analysis indeed highlights the usefulness of the more general setting suggested by Phillips. In order to explain the theory of deterministic shared memory we need a larger class of processes than those considered in CCS$^{CW}$.

Note that all the examples of Sec. 3 have the “input-scheduled” property that (non-trivial, i.e. non-self-blocking) precedences only exist between receiver actions $A$, while sender actions $\overline{A}$ never appear in any choice contexts. These are the processes covered by [10] which restrict prioritised choice to receiver actions (“input-guarded, prioritised choice”) in the same way as the programming language Occam [4] with its “PRIALT” construct does (cf. [10]).

**► Example 41.** The memory cell schedules readers after the writers and among the writers prefers to engage first with those that set the value to 0, in the prioritised sum. This implements an Esterel-style resolution function for multi-writer convergecast, multi-reader broadcast of boolean signals. All concurrent readers receive the same value, which is the combined-AND of all values written by any concurrent writer. If any process writes a boolean 1 it will win the competition. This is also known as a “wired-AND”. Likewise, we can implement a memory cell that models a “wired-OR” if we swap the roles of $w_0$ and $w_1$ in the prioritised choices of wAND$_w$.

Note that the wired-AND behaviour only applies to concurrent threads. A single thread can use the wAND cell as a local memory and destructively update it sequentially as it wishes. Consider the difference: Both concurrent writers $\overline{w_1}:\overline{w_1} | \overline{w_0}:\overline{w_0}$ and $w_0: w_0 | \overline{w_1}:\overline{w_1}$ will necessarily make the reader $R \stackrel{\text{def}}{=} r_0: r_1.A + r_1:\{r_0, r_1\}.B$ detect a value $r_0$ and therefore end in state $A$ (wired-AND of $w_0$ and $w_1$). The two single-threaded sequential writings $\overline{w_1}:\overline{w_1}.w_0:\overline{w_0}$ and $w_0: w_0.\overline{w_1}:\overline{w_1}$ will generate two different readings by $R$: The first is the reading $r_0$, leading to $A$. The second is the reading $r_1$, leading to $B$. ◀

## Strong Enabling vs Constructive Enabling

As an intermediate step to implement our precedence-based scheduling, the previous example suggests we look at the weak initial actions for a process. The next example shows why strong enabling, based on $i\overline{A}^*(R)$, is not sufficient and why we need the stronger notion of c-enabling (Def. 3), based on $i\overline{A}^*(R)$.
1182

1183

1184

1185

1186

1187

1188

1189

1190

1191

1192

1193

1194

1195

1196

1197

1198

1199

1200

1201

1202

1203

1204

1205

1206

1207

1208

1209

1210

1211

1212

1213

1214

1215

1216

1217

1218

1219

1220

1221

1222

1223

1224

1225

1226

1227

**► Example 42 (On Multi-Cast and Constructive Enabling).** Suppose $S_0 \stackrel{\text{def}}{=} a:e.S_0 + e.S_1 + \sigma:\{a,e\}.S_0$ is an Esterel Signal (Sec. 9) in its absent state, with abbreviations $e = \text{emit}$, $a = \text{abs}$ and $p = \text{pres}$. Its initial action $S_0 \xrightarrow{a} \{e\} S_0$ to communicate absence does not block itself to permit multi-reader scenarios. A typical reader is of form $R \stackrel{\text{def}}{=} \bar{p}:\bar{p}.R_1 + \bar{a}:\{\bar{a},\bar{p}\}.R_0$. This is a choice: if the signal is present we execute $R_1$, otherwise if it is absent we execute $R_0$. The two sender actions $\bar{p}$ and $\bar{a}$ are self-blocking, because these prefixes can only be consumed once. In essence, what we want is that there can be many senders of the value labels $\bar{p}$, $\bar{a}$ (readers) but at most one receiver for $p$, $a$ (signal).

Consider a reader $C \stackrel{\text{def}}{=} \bar{a}:\bar{a}.\bar{e}:\bar{e}.C_1$ that wants to emit the signal when it finds it absent. The composition $S_0|C$ is deterministic under strong enabling. $S_0|C \xrightarrow{\tau}|_0 \{e,\bar{a}\} S_0|\bar{e}:\bar{e}.C_1$. The blocking set contains two labels:

(1) First, $e \in \{e, \bar{a}\}$ indicates priority, i.e., that we do not want another concurrent thread sending $\bar{e}$, because the synchronisation for absence is based on the assumption that there is no emission. Specifically, $S_0|C|\bar{e} \xrightarrow{\tau}|_0 \{e, \bar{a}\} S_0|\bar{e}:\bar{e}.C_1|\bar{e}$ will block because $\{e, \bar{a}\} \cap i\bar{A}^\tau(0|0|\bar{e}) \neq \{\}$. Instead, the transition $S_0|C|\bar{e} \xrightarrow{\tau}|_0 \{\bar{e}\} S_1|C|0$ which emits the signal can proceed.

(2) Second, $\bar{a} \in \{e, \bar{a}\}$ indicates that the sending prefix $\bar{a}:\bar{a}$ of the reader $C$ (which has entered into the synchronisation $\tau = a|\bar{a}$) must not be consumed by another competing receiver. Specifically, $S_0|C|a \xrightarrow{\tau}|_0 \{e, \bar{a}\} S_0|\bar{e}:\bar{e}.C_1|a$ will block.

Now, take $S_0|C|D$ where the signal $S_0$ is connected with two readers, where $C$ is as above and $D \stackrel{\text{def}}{=} \bar{a}:\bar{a}.\bar{e}:\bar{e}.D_1$ analogous. Both readers can go ahead and synchronise in reactions $(\tau = a|\bar{a}) S_0|C|D \xrightarrow{\tau}|_0 \{e, \bar{a}\} S_0|\bar{e}:\bar{e}.C_1|D$ and $S_0|C|D \xrightarrow{\tau}|_0 \{e, \bar{a}\} S_0|C|\bar{e}:\bar{e}.D_1$ which are both strongly enabled since $i\bar{A}^\tau(0|0|D) = \{a\} = i\bar{A}^\tau(0|C|0)$ which is disjoint from the blocking set $\{e, \bar{a}\}$. This may seem ok, as we wanted to have multiple readers access the signal on the same port $a$. However, now the emission of $\bar{e}$ by the process that advanced first will block the reading of absence by the other which stayed behind. In each case symmetrically, there is only one (strongly enabled) transition left, viz. $S_0|\bar{e}:\bar{e}.C_1|D \xrightarrow{\tau}|_0 \{\bar{e}\} S_1|C|D$ and $S_0|C|\bar{e}:\bar{e}.D_1 \xrightarrow{\tau}|_0 \{\bar{e}\} S_1|C|D_1$ where the final states $C_1|D$ and $C|D_1$ of the readers are behaviourally different. Thus, we have non-determinism while the confluence is lost.

The core of the problem is that the concurrent contexts $0|0|D$ and $0|C|0$, respectively, of the above rendezvous synchronisations and do not account for the fact that the signal $S_0$ can be simultaneously reused by the other reader that is not involved in the transition. We could account for this reuse by adding $S_0$ into the concurrent context as in $S_0|C|D \xrightarrow{\tau}|_0 \{e, \bar{a}\} S_0|\bar{e}:\bar{e}.C_1|D$. Now $D$ can interact with $S_0$ in the concurrent context $S_0|0|D$. The above transition depends on the assumption that no other thread will send $\bar{e}$. This is not true, because now $e \in i\bar{A}^\tau(S_0|0|D)$. Thus, putting the shared signal $S_0$ into the concurrent environment is enforcing determinism by blocking the strong enabling properties of the above transitions. Unfortunately, the fix is too strong. The presence of $S_0$ in the concurrent context would block even the single reader in $S_0|\bar{a}:\bar{a}$. Specifically, the reduction $S_0|\bar{a}:\bar{a} \xrightarrow{\tau}|_0 \{e, a\} S_0|0$ would block, because $\bar{a} \in i\bar{A}(S_0) \subseteq i\bar{A}^\tau(S_0|0)$, and so the reduction is not strongly enabled any more. Thus, our fix would not permit any reading of the signal $S_0$, whatsoever.

The solution is to tighten up the notion of strong enabling and close it under arbitrary non-clock transitions in the concurrent environment rather than just the silent steps. Technically, we define a larger set $i\bar{A}^*(E) \supset i\bar{A}^\tau(E)$ of potential labels (Def. 3) that closes under all non-clock actions of $E$. In this case, we do find $e \in \{e, \bar{a}\} \cap i\bar{A}^*(0|0|D) \neq \{\}$. In this way, diverging reductions are no longer enabled. On the other hand, the reduction $S_0|C \xrightarrow{\tau}|_0 \{e, a\} S_0|\bar{e}:\bar{e}.C_1$
$$
\begin{align*}
\text{ABRO} &\stackrel{\text{def}}{=} \sigma.(A|B|R|O) \setminus \{s,t\} \\
A &\stackrel{\text{def}}{=} k:k.0 + a:\{k,a\}.\bar{s}:\bar{s}.0 + \sigma:\{k,a\}.A \\
B &\stackrel{\text{def}}{=} k:k.0 + b:\{k,b\}.\bar{s}:\bar{s}.0 + \sigma:\{k,b\}.B \\
R &\stackrel{\text{def}}{=} r:r.R' + \tau:r.\sigma.R \\
R' &\stackrel{\text{def}}{=} \bar{k}.R' + \tau:\bar{k}.\text{ABRO} \\
O &\stackrel{\text{def}}{=} k:k.0 + s:k.O + t:\{k,t,s\}.\bar{o}:\bar{o}.0 + \sigma:\{k,s,t\}.O.
\end{align*}
$$

<caption>Figure 9 Simplified version of ABRO.</caption>

remains enabled, because $\overline{iA^*}(0|0) = \{\}$. In general, single readers $S_0|C$ where $C$ is an arbitrary sequential process, or multiple readers $S_0|C|D$ where at most one of $C$ or $D$ is writing, i.e., sending $\bar{c}$, remain enabled.

**► Example 43 (On Fully Multi-Cast ABRO).** To model full multi-cast ABRO in CCS<sup>spt</sup>, we could use sharable (i.e., non-self-blocking) prefixes on internal actions to show how they are useful to model the control-flow of Esterel programs, specifically termination and reset. Consider the process ABRO from Ex. 10 again:

- The reset watchdog R can receive a reset signal r or silently move to state σ.R where it synchronises on the clock σ to repeat in the next macro-step. When a reset r is received by the environment, then R executes the sequence $r:r.\bar{k}_1:\bar{k}_1.\bar{k}_2:\bar{k}_2.\bar{k}_3:\bar{k}_3.\bar{k}_4:\bar{k}_4$.ABRO whereby it sends a “kill” signal $\bar{k}_i$ to each of the four threads A, B, T and O, in some arbitrary but fixed order. When all kills have been delivered, the watchdog R will restart ABRO. Until such time, there is no clock possible. The second transition $R \xrightarrow{\tau} \{r\} \sigma.R$ preempts this reset choice but has lower priority as it is blocked by r. It is only taken when there is no reset possible, i.e., when the reset signal r is absent. Note that with the preemption of the kill signals $\bar{k}_i$ are removed from the potential, because $\overline{iA^*}(\sigma.R) = \{\}$, i.e., we do not look past the clock prefix.

- The A and B processes are analogous to each other with the role of a and b swapped. Looking at A, we see that it has a choice of three actions, viz to receive a kill signal $k_1$, an input signal a or perform the clock action σ to start the next macro step. The kill $k_1$ has highest priority, action a second and the clock can only go ahead if there is neither a $k_1$ nor an a signal to be received. When there is no kill but an a signal, then the process A sends an $\bar{s}$ signal to indicate its termination. When the kill $k_1$ occurs, it enters into the halt state 0 where it is inactive but permits any number of clock ticks. Since this is the neutral element for parallel composition, A essentially drops out of the picture. Note that we cannot use the inactive 0 here, because then the terminated process A would block the clock for all other threads. Finally, when there is neither a kill $k_1$ nor signal a, the A process can synchronise on σ and repeat as A in the next macro-step. In this fashion, A will patiently wait for a clock tick in which $k_1$ or a occur. If both occur, the kill takes priority: For instance, the transition $A|\bar{k}_1.0|\bar{a}.0 \xrightarrow{\tau} \{k_1\} 0|0|\bar{a}.0$ is constructively enabled while $A|\bar{k}_1.0|\bar{a}.0 \xrightarrow[0|\bar{k}_1.0|0]{\tau} \{k_1,a\} 0|\bar{k}_1.0|0$ is not enabled.

- The process T is the termination detector implementing the principle discussed above. It forms a clock-patient, killable counter that waits for any possible reception of signal s before it sends termination $\bar{t}$ to process O. Note that T itself does not need to know how many possible termination signals there are. It waits for the termination count
XX:36 Strong Priority and Determinacy in Timed CCS

(implemented by iA*) to reach zero.

1263

When process O receives the termination signal $t$ it sends the output signal $\bar{o}$ to the environment and then halts. Alternatively, with highest priority, it can be killed by reception of $k_5$ or engage in the clock $\sigma$ if neither a kill $k_5$ nor a termination $t$ is present. The reduction $\tau = \bar{t}:\{k_3, \bar{t}, s\} | t:\{k_4, t\}$ between T and O will be blocked by precedence, for as long as at least one of the processes A or B has a choice term that sends $\bar{s}$, i.e., as long as $s \in iA^*(A|B)$. Only when both prefix sequences $a:\{a, k_1\}$.\bar{s}:\bar{s}.0$ and $b:\{b, k_2\}$.\bar{s}:\bar{s}.0$ have been eliminated by reductions, then the termination can occur.

1264

1265

1266

1267

1268

1269

1270

1271

1272

1273

1274

1275

1276

Using multi-cast, we can improve on this as seen in Fig. 9: We can integrate the termination test into the output process O if we let O loop on consumption of s rather than T. Similarly, we can use only a single (multi-cast) kill signal k shared between A, B, O: The reset process R keeps sending $\bar{k}$ unboundedly often, until all target processes have received a copy and all receptions k have been consumed. At that point, it takes a clock step to repeat ABRO from the start.

1277 One can verify that ABRO is coherent and pivotable using Thm. 24.

The choices in each of the threads A, B, R, O are fully resolved by the blocking sets, i.e., every pair of actions in the summations are distinct and in precedence relationships. Every rendezvous prefix is self-blocking unless the action can be repeated with the same blocking in the continuation process. This happens for channels s and k in the recursions $O \stackrel{def}{=} \dots + s:k.O + \dots$ and $R' \stackrel{def}{=} \bar{k}.R' + \dots$. Thus, the threads A, B, R, O themselves are coherent.

1278

1279

1280

1281

1282

1283

A suitable policy $\pi$, for which the threads A, B, R, O are coherent, enforces the precedences
* $k \dashrightarrow \ell \in \pi$ for $\ell \in \{k, a, b, s, t, \sigma\}$
* $\ell \dashrightarrow \ell \in \pi$ for $\ell \in \{r, k, a, b, \bar{s}, t, \bar{o}\}$
* $s \dashrightarrow t \in \pi$
* $\ell \dashrightarrow \sigma \in \pi$ for $\ell \in \{a, b, s, t\}$.

1284

1285

1286

1287

1288

The dual matching pairs for these precedences, however, are all concurrently independent. More precisely, we look at distinct labels, $\bar{k} \diamond \bar{\ell} \in \pi$ for all $\ell \in \{r, o, a, b, s, t, \sigma\}$, $\bar{s} \diamond \bar{t} \in \pi$ and $\bar{\ell} \diamond \sigma \in \pi$ for $\ell \in \{r, o, a, b, s, t\}$.

1289

1290

1291

Thus, the policy $\pi$ (and thus $\pi \setminus \mathcal{R}$) is a pivot policy and so the parallel composition $A|B|R|O$ is coherent for $\pi$. Further, $\pi$ is precedence-closed for $\{s,t\}$ which means that $(A|B|R|O) \setminus \{s,t\}$ is coherent for $\pi \setminus \{s,t\}$. Finally, since $\{\ell \mid \ell \dashrightarrow \sigma \in \pi \setminus \{s,t\}\} = \{a,b\}$, the process ABRO (which starts with a prefix $\sigma:H$ where $H = \{\}$) is coherent for $\pi \setminus \{s,t\}$.

1292

1293

1294

1295

1296

◀

C Auxiliary Results

1297

In the following we list some simple observation on the properties of iA($P$), iA$^{\tau}$(P) and iA*($P$) that will be used in the proofs.

1298

1299

► Lemma 44. Let P, Q be processes:

1300

(1) $P \xrightarrow{\sigma}^H Q$ implies $R \equiv 0$.

1301

(2) $\alpha \in iA(P)$ iff $P \xrightarrow{\alpha} Q$.

1302

(3) $iA(P) \cap \mathcal{R} \subseteq iA(P|Q)$.

1303

(4) If P is single-threaded, then $P \xrightarrow{\alpha}^H Q$ implies $\alpha \in \mathcal{L}$, $R \equiv 0$ and $\tau \notin H$.

1304

(5) If $P \xrightarrow{\alpha}^H Q$ then $iA(R) \subseteq iA(P)$.

1305
**Proof.** (2) is by definition. The other points follow by an inspection of the SOS rules, using the definition of $iA(P)$.

Lem. 44(1) means that clock actions always run in an empty concurrent environment. Observe that Lem. 44(2) means that the set $iA(P)$ corresponds to the initial actions of $P$. The presence of $\tau$ in the blocking set of a transition provides information about the set of initial actions of a process. Specifically, in rule (Com) the presence of $\tau$ in the set $H = race(P|Q)$ indicates a blocking situation arising from the priorities in $P$ or $Q$ conflicting with the rendevous actions $\ell$ or $\bar{\ell}$. Thus, the condition $\tau \notin H$ can be used to implement priority-based scheduling. Lem. 44(4) implies that single-threaded processes are never blocked.

**Lemma 45.** Let $P$ be an arbitrary process:

(1) $iA(P) \cap \mathcal{L} \subseteq iA^T(P) \subseteq iA^*(P)$.

(2) If $P \equiv Q$ then $iA^*(P) = iA^*(Q)$.

(3) If $P \xrightarrow{\alpha} Q$ for $\alpha \in \mathcal{R} \cup \{\tau\}$, then $iA^*(Q) \subseteq iA^*(P)$.

**Proof.** All points follow by an inspection of the SOS rules, using the definition of $iA^T(P)$ and $iA^*(P)$.

## On Interference

**Proposition 46.** Suppose $\alpha_1:H_1[E_1|R]$ and $\alpha_2:H_2[E_2|R]$ are interference-free. Then, $\alpha_1:H'_1[E_1]$ and $\alpha_2:H'_2[E_2]$ are interference-free for arbitrary subsets $H'_1 \subseteq H_1$ and $H'_2 \subseteq H_2$.

As a special case, choosing $R=0$, Proposition 46 implies non-interference of $\alpha_i:H'_i[E_i]$ for $i \in \{1,2\}$ from non-interference of $\alpha_i:H_i[E_i]$ for any $H'_i \subseteq H_i$.

**Proof.** First, non-interference of $\alpha_i:H_i[E_i|R]$ means $\alpha_i \notin H_{3-i}$ by assumption. Since $H'_i \subseteq H_i$, this implies also $\alpha_i \notin H'_{3-i}$. Second, suppose that $\alpha_{3-i} = \tau$ for some $i \in \{1,2\}$. Then, non-interference of $\alpha_1:H_1[E_1|R]$ and $\alpha_2\bar{H}_2[E_2|R]$ gives $\tau \notin H_i$ and $H_i \cap i\bar{A}^*(E_i|R) = \{\}$. Since by Lem. 44, $i\bar{A}^*(E_i) \subseteq i\bar{A}^*(E_i|R)$, the inclusions $H'_i \subseteq H_i$ preserve this property, i.e., $\tau \notin H'_i$ and $H'_i \cap i\bar{A}^*(E_i) \subseteq H_i \cap i\bar{A}^*(E_i|R) = \{\}$.

## On Policies

We obtain a partial ordering $\pi_1 \le \pi_2$ on precedence policies by subset inclusion. Specifically, we have $(L_1, \dashv\dashv_1) \le (L_2, \dashv\dashv_2)$ if $L_1 \subseteq L_2$ such that for all $\ell_1, \ell_2 \in L_1$, if $\ell_1 \dashv\dashv_2 \ell_2$ then $\ell_1 \dashv\dashv_1 \ell_2$. Intuitively, if $\pi_1 \le \pi_2$ then $\pi_2$ is a tightening of $\pi_1$ in the sense that it exports more labels (resources) subject to possibly fewer precedences (causality constraints) than $\pi_1$. By way of this ordering, we can use policies to measure the degree of concurrency exhibited by a process. The alphabet of the $\le$-maximal policy $\pi_{max}$ contains all labels $\mathcal{L}$ and its precedence relation $\dashv\dashv_{max}$ is empty. It is the largest policy in the $\le$ ordering. The $\le$-minimal policy $\pi_{min}$ has empty alphabet and empty precedences. It is self-dual, i.e., $\bar{\pi}_{min} = \pi_{min}$.

There is also the normal inclusion ordering $\pi_1 \subseteq \pi_2$ between policies defined by $L_1 \subseteq L_2$ and $\dashv\dashv_1 \subseteq \dashv\dashv_2$. It differs from $\le$ in the inclusion direction of the precedence alphabets.

For any policy $\pi$ on alphabet $L$ we define its *dual* as a policy $\bar{\pi}$ on the set of labels $\bar{L}$ where for all $\bar{\ell}_1, \bar{\ell}_2 \in \bar{L}$ we stipulate $\bar{\ell}_1 \dashv\dashv \bar{\ell}_2 \in \bar{\pi}$ iff $\ell_1 = \ell_2$ or $\ell_1 \diamond \ell_2 \in \pi$, i.e., both $\ell_1 \dashv\dashv \ell_2 \notin \pi$ and $\ell_2 \dashv\dashv \ell_1 \notin \pi$. Intuitively, the dual policy $\bar{\pi}$ consists of matching copies $\bar{\ell}$ of all labels $\ell$ from $\pi$ and puts them in a precedence relation precisely if their original copies
are identical or do not stand in precedence to each other, in any direction. This generates a form of “negation” $\bar{\pi}$ from $\pi$, which is reflexive and symmetric. Note that $\bar{\pi}$ need not be identical to $\pi$ but contains more precedences. In general, we have $\bar{\pi} \le \pi$ and $\bar{\pi} = \pi$ if $\pi$ is symmetric. The policy $\bar{\pi}$ captures the independences between actions of $\pi$ and is called the associated *independence alphabet*, in the sense of trace theory [12]. Analogously, $\bar{\pi}$ expresses the dependencies of actions in $\pi$, called the associated *dependence alphabet*.

1347

1348

1349

1350

1351

1352

1353

1354

1355

1356

1357

1358

1359

1360

1361

1362

1363

1364

1365

**Example 47.** Suppose $P \Vdash \ell_1 \diamond \ell_2$ then all transitions with labels $\ell_1$ and $\ell_2$ of $P$ must be from concurrent threads and thus cannot block each other. For instance, both $\ell_1 | \ell_2$ and $\ell_1 + \ell_2$ conform to $\ell_1 \diamond \ell_2$. However, the choice $\ell_1 + \ell_2$ is not coherent. It becomes coherent if we add a precedence $\ell_1 + \ell_2:\ell_1$ but then it is not longer conformant to $\ell_1 \diamond \ell_2$. Instead, we now have $\ell_1 + \ell_2:\ell_1 \Vdash \ell_1 \dashv\dashv \ell_2$, where the policy expresses the precedence coded in the blocking sets of the prefixes. Suppose $P \Vdash \ell_1 \diamond \ell_2$ then all transitions with labels $\ell_1$ and $\ell_2$ of $P$ must be from concurrent threads and thus cannot block each other. For instance, both $\ell_1 | \ell_2$ and $\ell_1 + \ell_2$ conform to $\ell_1 \diamond \ell_2$. However, the choice $\ell_1 + \ell_2$ is not coherent. It becomes coherent if we add a precedence $\ell_1 + \ell_2:\ell_1$ but then it is no longer conformant to $\ell_1 \diamond \ell_2$. Instead, we now have $\ell_1 + \ell_2:\ell_1 \Vdash \ell_1 \dashv\dashv \ell_2$, where the policy expresses the precedence coded in the blocking sets of the prefixes. More generally, if $\ell_1 \dashv\dashv \ell_2 \in \pi$ and $\ell_1 \neq \ell_2$ are distinct, then $P \Vdash \pi$ may take $\ell_1$ and $\ell_2$ transitions to completely different states from the same thread.

1366

1367

**Definition 48 (Pivot Policy).** A policy $\pi$ is called a pivot policy if $\bar{\pi} \le \pi$. We call a process $P$ pivotable if $P$ conforms to a pivot policy.

1368

1369

**Proposition 49.** A policy $\pi = (L, \dots)$ is a pivot policy if $\bar{L} \subseteq L$ and for all $\ell_1, \ell_2 \in L$ with $\ell_1 \neq \ell_2$ we have $\ell_1 \diamond \ell_2 \in \pi$ or $\bar{\ell}_1 \diamond \bar{\ell}_2 \in \pi$.

1370

1371

1372

1373

1374

1375

1376

**Proof.** Let $\pi$ be a pivot policy. Since the alphabet of $\bar{\pi}$ is $\bar{L}$ and the alphabet of $\pi$ is $L$ the assumption $\bar{\pi} \le \pi$ implies $\bar{L} \subseteq L$ by definition of $\le$. Given labels $\ell_1, \ell_2 \in L$ with $\ell_1 \neq \ell_2$ suppose $\ell_1 \diamond \ell_2 \notin \pi$. Hence $\ell_1 \dashv\dashv \ell_2 \in \pi$ or $\ell_2 \dashv\dashv \ell_2 \in \pi$. Consider the first case, i.e., $\ell_1 \dashv\dashv \ell_2 \in \pi$. Since $\bar{L} \subseteq L$ and $L = \bar{\bar{L}}$ it follows that also $L \subseteq \bar{L}$, i.e., the labels $\ell_i$ are also in the alphabet of $\bar{\pi}$. But then by definition of the ordering and the fact that $\ell_i = \bar{\ell}_i$, the assumption $\bar{\pi} \le \pi$ implies that $\bar{\bar{\ell}}_1 \dashv\dashv \bar{\bar{\ell}}_2 \in \bar{\pi}$. Now, the definition of the dual policy means that $\bar{\bar{\ell}}_1 \dashv\dashv \bar{\bar{\ell}}_2 \notin \pi$ and $\bar{\bar{\ell}}_2 \dashv\dashv \bar{\bar{\ell}}_1 \notin \pi$. This is the same as $\bar{\bar{\ell}}_1 \diamond \bar{\bar{\ell}}_2 \in \pi$ as desired.

1377

1378

1379

1380

1381

Suppose the properties (1) and (2) of the proposition hold for a policy $\pi$. We claim that $\bar{\pi} \le \pi$. The inclusion of alphabets is by assumption (1). Then, suppose $\bar{\bar{\ell}}_1 \dashv\dashv \bar{\bar{\ell}}_2 \in \pi$ which implies $\bar{\bar{\ell}}_1 \diamond \bar{\bar{\ell}}_2 \notin \pi$. If $\ell_1 = \ell_2$ we have $\bar{\bar{\ell}}_1 \dashv\dashv \bar{\bar{\ell}}_2 \in \bar{\pi}$ directly by definition. So, let $\ell_1 \neq \ell_2$. Because of $\bar{L} \subseteq L$ and (2) this gives us $\ell_1 \diamond \ell_2 \in \pi$ considering again that $\ell_i = \bar{\ell}_i$. But $\ell_1 \diamond \ell_2 \in \pi$ is the same as $\bar{\bar{\ell}}_1 \dashv\dashv \bar{\bar{\ell}}_2 \in \bar{\pi}$ by definition. ◀

1382

**Proposition 50.** Suppose $P$ is input-scheduled $\pi_{is}$ and $P \xrightarrow{\alpha} H$ $Q$ for some $\alpha$, $H$, $R$, $Q$. Then:

1383

1. If $\alpha \in \bar{\mathcal{A}}$ then $H \subseteq \{\alpha, \tau\}$.

1384

2. If $\alpha \in \mathcal{A} \cup \mathcal{C} \cup \{\tau\}$ then $H \subseteq \mathcal{A} \cup \mathcal{C} \cup \{\tau\}$.

1385

**Proof.** Obvious by definition of conformance and the construction of $\pi_{is}$. ◀

<figure><img src="image_12.png" /></figure>

1386

1387

1388

The next crucial Lemma implies that two coherent threads cannot block each other if they are conformant to the same pivot policy. The blocking of a reduction $\ell | \bar{\ell}$ must always arise from a thread in the concurrent context that is not involved in the synchronisation.

1389

1390

**Lemma 51.** Let $P_1 \Vdash \pi$ and $P_2 \Vdash \pi$ be coherent for the same pivot policy $\pi$ and $\ell \in \mathcal{L}$ such that $P_1 \xrightarrow{\ell} H_1 P'_1$ and $P_2 \xrightarrow{\bar{\ell}} H_2 P'_2$. Then, $H_2 \cap \bar{iA}(R_1) = \{\}\}$ implies $H_2 \cap \bar{iA}(P_1) \subseteq \{\bar{\ell}\}$.
**Proof.** Let $\ell \in \mathcal{L}$ and the transitions be given as in the statement of the Lemma. Suppose $\alpha \in H_2$ and $\alpha \in \overline{iA}(P_1)$. We claim that $\alpha = \overline{\ell}$, whence $H_2 \cap \overline{iA}(P_1) \subseteq \{\overline{\ell}\}$. By contraposition let us assume that $\alpha \neq \overline{\ell}$, or equivalently $\bar{\alpha} \neq \ell$. Further, since $iA(P_1) \subseteq \mathcal{L}$ we also have $\alpha \neq \tau$. The assumption $\alpha \in H_2$ means $\alpha \dashrightarrow \overline{\ell} \in \pi$ by Def. 12(1) applied to $P_2$. Since $\pi$ is pivot we must thus have $\bar{\alpha} \diamond \ell \in \pi$, specifically $\bar{\alpha} \dashrightarrow \ell \notin \pi$, i.e., $\bar{\alpha} \notin H_1$, again by Def. 12(1), now applied to $P_1$. But since $\bar{\alpha} \in iA(P_1)$, by Lem. 44, there is a transition $P_1 \xrightarrow{\bar{\alpha}/E} H Q$. Since also $\ell \dashrightarrow \bar{\alpha} \notin \pi$, by pivot property, it follows $\ell \notin H$ by Def. 12(1) again for $P_1$. Now both $\bar{\alpha} \notin H_1$ and $\ell \notin H$ mean that the c-actions $\ell:H_1[R_1]$ and $\bar{\alpha}:H[E]$ are interference-free (Def. 53). Since $\ell \neq \bar{\alpha}$ there must exist a reconvergent process $R$ and transitions

$$P_1 \xrightarrow{\bar{\alpha}/E} H' R \text{ and } Q \xrightarrow{\ell/R_1} H'_1 R \text{ with } R_1 \xrightarrow{\bar{\alpha}} R'_1 \text{ and } E \xrightarrow{\ell} E'$$

The latter transitions are strengthenings of the residuals $R_1 \rightsquigarrow R'_1$ and $E \rightsquigarrow E'$ that must exist according to the statement of Coherence, because of $\{\ell, \bar{\alpha}\} \subseteq \mathcal{R}$ and $\ell \neq \bar{\alpha}$. However, the transition $R_1 \xrightarrow{\bar{\alpha}} R'_1$ implies $\bar{\alpha} \in iA(R_1)$ which is impossible, because then $\alpha \in H_2 \cap \overline{iA}(R_1)$ while $H_2 \cap \overline{iA}(R_1) = \{\}$ by assumption.

We can show that pivotable processes do not have internal races.

**Lemma 52.** Let $P \models \pi$ be coherent for a pivot policy $\pi$. Then, for every reduction $P \xrightarrow{\tau/E} H P'$, if $H \cap \overline{iA}(E) = \{\}$ then $\tau \notin H$.

**Proof.** Let $P$ be coherent for pivotable $\pi$ and a reduction $P \xrightarrow{\tau/E} H P'$ such that $H \cap \overline{iA}(E) = \{\}$ be given. Suppose, by contraposition, $\tau \in H$. Since there are no action prefixes $\tau.P'$ in CCS$^{\text{spt}}$, the reduction must arise from a synchronisation of two threads $P_1$ and $P_2$ inside $P$, via rule (Com), i.e.,

$$\frac{P_1 \xrightarrow{\ell/R_1} H_1 P'_1 \quad P_2 \xrightarrow{\overline{\ell}/R_2} H_2 P'_2 \quad B = \{\ell | \overline{\ell} | H_2 \cap \overline{iA}(P_1) \not\subseteq \{\overline{\ell}\} \text{ or } H_1 \cap \overline{iA}(P_2) \not\subseteq \{\overline{\ell}\}}}{P_1 | P_2 \xrightarrow{\ell/\overline{\ell}|/R_1|R_2} H_1 \cup H_2 \cup B P'_1 | P'_2} \quad (\text{Com})$$

for some $\ell \in \mathcal{L}$. The assumption $H \cap \overline{iA}(E) = \{\}$ for the top-level reduction implies that $(H_1 \cup H_2) \cap \overline{iA}(R_1 | R_2) = \{\}$ at the point of (Com). Here we may assume, by induction on the depth of the derivation, that $\tau \notin H_1 \cup H_2$. We must show that the synchronisation action $\tau$ cannot enter into the blocking set by (Com), i.e., $\tau = \ell | \overline{\ell} \notin B$, i.e., which is the same as $H_2 \cap \overline{iA}(P_1) \subseteq \{\overline{\ell}\}$ and $H_1 \cap \overline{iA}(P_2) \subseteq \{\ell\}$. The sub-expressions $P_1 \models \pi'$ and $P_2 \models \pi'$ are also coherent for a common pivot policy $\pi'$. This policy may contain local labels that are restricted or hidden in the outer process $P$. Since by assumption we have $H_1 \cap \overline{iA}(R_1) \subseteq (H_1 \cup H_2) \cap \overline{iA}(R_1 | R_2) = \{\}$ and likewise $H_2 \cap \overline{iA}(R_2) = \{\}$, we can apply Lem. 51 to show $H_2 \cap \overline{iA}(P_1) \subseteq \{\overline{\ell}\}$ and $H_1 \cap \overline{iA}(P_2) \subseteq \{\ell\}$. This means $B = \{\}$ and we are done.

## The Role of Pivotability

Let us give an example to show that the requirement of pivotability cannot be removed in the closure statement for parallel compositions of Thm. 14. For compactness of notation let us write $\ell:H$ for $\ell:(H \cup \{\ell\})$ to create reflexive prefixes. Let

$$Q = \underline{b} | \underline{c}:a \text{ and } R = \overline{b}:\overline{a}.R_1 + \overline{c}:\overline{a}.R_2 \text{ with } R_1 = \underline{a} + \overline{c}:\overline{a} \text{ and } R_2 = \underline{a} + \overline{b}:\overline{a}.$$

First, we observe that both $Q$ and $R$ are coherent:
XX:40 Strong Priority and Determinacy in Timed CCS

Process $Q$ has two admissible transitions

$$Q \xrightarrow{b \atop 0} \{b\} 0 \text{ and } Q \xrightarrow{c \atop 0} \{c,a\} 0$$

which both are self-interfering. Thus, reconvergence is required only between the two transitions which is guaranteed, because they are from concurrent threads. This can also be obtained from Thm. 24 and the pivot policy with $b \dasharrow b \in \pi$, $c \dasharrow c \in \pi$ and $a \dasharrow c \in \pi$.

Process $R$ has two admissible transitions, the c-action $R \xrightarrow{\bar{b} \atop 0} \{\bar{a}\} R_1$ and $R \xrightarrow{\bar{c} \atop 0} \{\bar{a}\} R_2$. Each interferes with itself but not with the other. Thus, coherence implies that $R_1$ and $R_2$ reconverge. This is indeed the case, since we have $R_1 \xrightarrow{\bar{c} \atop 0} \{\bar{a}\} 0$ and $R_2 \xrightarrow{\bar{b} \atop 0} \{\bar{a}\} 0$, with commuting actions. The concurrent contexts are residual since $0 \rightsquigarrow 0$ and $0 \rightsquigarrow 0$. Since all admissible transitions of $R_1$ (and $R_2$) are reflexive and interfere with each other, $R_1$ (and $R_2$) are coherent, too.

Next we show that the parallel composition $Q|R$ is not coherent. We have admissible c-actions

$$Q|R \xrightarrow{b|\bar{b} \atop c:a} \{b,\bar{b},\bar{a}\} c:a|R_1 \text{ and } Q|R \xrightarrow{c|\bar{c} \atop \bar{b}} \{c,\bar{c},a,\bar{a}\} \bar{b}|R_2.$$

which are in fact c-enabled. However, the continuation process $c:a|R_1 = c:a|\bar{a} + \bar{c}:\bar{a}$ on the left is binary blocked by a race condition. We find

$$c:a|R_1 \xrightarrow{c|\bar{c} \atop 0} \{c,\bar{c},\bar{a},\tau\} 0$$

where the silent $\tau$ enters the blocking set, because $\{a\} \cap i\bar{A}(\bar{a} + \bar{c}:\bar{a}) \not\subseteq \{c\}$. This is a race computed in rule (Com). Thus, the reduction $c|\bar{c}$ of the original state $Q|R$ is not longer c-enabled in the state $c:a|R_1$. This breaks coherence.

Finally, we notice that $Q|R$ is not pivotable. A common policy $\pi$ for $Q|R$ must obviously include the precedences $\bar{a} \dasharrow \bar{c} \in \pi$, as well as $a \dasharrow c \in \pi$. This is not pivot according to Def. 48.

1427 On Milner's Confluence Class

As we have noted above, CCS corresponds to the unclocked and (blocking) free processes of CCS<sup>spt</sup> (Prop. 29). For these processes, admissible transitions and strongly enabled transitions coincide. The key result of Milner [27] (Chap. 11, Prop. 19) is that confluence is preserved by inaction 0, prefixing $\ell.P$ and confluent composition defined as $P|_L Q = (P|Q) \setminus L$ where $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}$ and $\overline{\mathcal{L}(P)} \cap \mathcal{L}(Q) \subseteq L \cup \overline{L}$. We will show how confluence for this fragment of CCS processes follows from our more general results on coherence. From now on, for the rest of this section, we assume that all processes are unclocked, i.e., each prefix $\ell:H.Q$ has $H \cup \{\ell\} \subseteq A \cup \overline{A}$.

Let us call a process $P$ discrete if all prefixes occurring in $P$ are of form $\ell:\{\ell\}.Q$, i.e., they are self-blocking. Under strong enabling, a discrete process behaves like a CCS process with the restriction that each action $\ell$ only synchronises if there is a matching partner $\overline{\ell}$ in a unique other parallel thread. If the matching partner is not unique, then the scheduling blocks. For instance, $\ell:\ell|\overline{\ell}|\overline{\ell}|\overline{\ell}$ blocks because there are two concurrent senders $\overline{\ell}$ matching the receiver $\ell$. Now consider the fragment CCS<sup>cc</sup> of discrete processes built from inaction 0, self-blocking prefixes $\ell:\{\ell\}.Q$ and confluent composition. Milner's result says that the processes in CCS<sup>cc</sup> are confluent under admissible scheduling.
To emulate Milner's result in our setting, we consider the sort $\mathcal{L}(P)$ of a process $P$ as the admissible actions of a discrete policy $\pi_P$ with only reflexive precedences. In other words, $\ell_1 \dashv\vdash \ell_2 \in \pi_P$ iff $\ell_1 = \ell_2$. It is easy to see that a discrete process always conforms to $\pi_P$. Also, discrete policies are always pivot policies (Def. 48) and dependency-closed for all label sets (Def. 48), as one shows easily. Thus, discrete processes, which are coherent for discrete policies, fullfill all conditions of the preservation laws for inaction 0 (Prop. 60), self-blocking action prefix $\ell:\mathcal{H}[E]$ (Prop. 61), parallel composition $P|Q$ (Prop. 64) and restriction $P\setminus L$ (Prop. 66). As a consequence and in particular, all processes in $\mathbf{CCS}^{\mathbf{cc}}$ are coherent under strong enabling by our results.

Our final observation now is that, for Milner's fragment $\mathbf{CCS}^{\mathbf{cc}}$, the transition semantics under admissible and strong enabling, as well as the notions of confluence and coherence, coincide. Firstly, if $P$ is discrete then in every c-action $\ell:H[E]$ executed by a derivative $Q$ of $P$ we must have $H = \{\ell\}$. Thus, the coherence Def. 12(1) becomes redundant since it is always satisfied. Further, any two c-actions $\ell_i:H_i[E_i]$ of transitions $Q \xrightarrow{\ell_1} H_1 Q_1$ and $Q \xrightarrow{\ell_2} H_2 Q_2$ for $\ell_1 \neq \ell_2$ or $Q_1 \neq Q_2$ are trivially interference-free. The confluent composition of Milner has the further effect that for every c-action $\ell:H[E]$ we must have $\ell \notin i\overline{A}^*(E)$. This is proven by induction on the structure of $P \in \mathbf{CCS}^{\mathbf{cc}}$. Further, the side condition of (Com) becomes trivial, and thus generally $\tau \notin H$. This is a result of the side-conditions of the confluent composition. Hence, for $\mathbf{CCS}^{\mathbf{cc}}$, strong enabling coincides with plain admissibility $\mathbf{CCS}$. Notice that the class of discrete processes and the class processes coherent for discrete policies is larger than $\mathbf{CCS}^{\mathbf{CW}}$. In particular, we can explain coherence of broadcast actions with repetitive prefixes. Hence, our results are more general even for the restricted class of discrete behaviours.

# D Proofs

First, we adopt a slightly more general form of interference, for general c-actions not just for those that are constructively enabled, as in Def. 11.

**Definition 53.** Two c-actions $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are called interference-free if the following holds for all $i \in \{1,2\}$:

(1) If $\alpha_1 \neq \alpha_2$ then $\alpha_i \notin H_{3-i}$.

(2) If $\alpha_{3-i} = \tau$ then $H_i \cap (i\overline{A}^*(E_i) \cup \{\tau\}) = \{\}$.

The extra condition (2) in Def. 53 says that for a c-action not to interfere with a silent (and thus uncontrollable) action it must be c-enabled. Obviously, Def. 53 is a weakening of Def. 11, i.e. if $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are interference-free according to Def. 53 they are interference-free according to Def. 11.

**Proposition 54.** If a coherent process $P$ offers enabled transitions on a clock $\sigma$ and another distinct action $\alpha \neq \sigma$ with $P \xrightarrow{\alpha} H_1 P_1$ and $P \xrightarrow{\sigma} H_2 P_2$ then $\alpha \in H_2$ or $\sigma \in H_1$. In particular, if $\alpha = \tau$ then $\sigma \in H_1$.

*Proof.* Since $R_2 = 0$ by Lem. 44(1) and $iA(0) = \{\}$, we have $\alpha \notin iA(R_2)$ and thus $\alpha$ cannot be an initial action $R_2 \xrightarrow{\alpha} R'_2$, by Lem. 44(2). Now we have $\{\alpha, \sigma\} \cap C \neq \{\}$. But then the coherence Def. 12(2) implies that the c-actions $\alpha:H_1[R_1]$ and $\sigma:H_2[R_2]$ must interfere. Since $\alpha \neq \sigma$ this implies $\alpha \in H_2$ or $\sigma \in H_1$, or $\alpha = \tau$ and $H_2 \cap (i\overline{A}^*(R_2) \cup \{\tau\}) \neq \{\}$. Since $R_2 = 0$ the latter reduces to $\alpha = \tau \in H_2$. The last part of the Proposition now follows from the fact that the clock transition is enabled and thus $\tau \notin H_2$. ◀
Of Thm. 14. Let $P$ be coherent and $Q$ a derivative with c-enabled reductions $Q \xrightarrow{\tau} \overline{R_1} \xrightarrow{H_1} Q_1$ and $Q \xrightarrow{\tau} \overline{R_2} \xrightarrow{H_2} Q_2$. If $Q_1 = Q_2$ we are done immediately. Suppose $Q_1 \neq Q_2$. Then c-enabling implies $\tau \notin H_i$ as well as $H_i \cap \overline{iA^*}(R_i) = \{\},$ which implies $H_i \cap (\overline{iA^*}(R_i) \cup \{\tau\}) = \{\}$. But then the c-actions $\tau: H_1[R_1]$ and $\tau: H_2[R_2]$ are interference-free, whence coherence Def. 12(2) implies there exist $H'_i$ and processes $R'_i$, $Q'$ such that $Q_1 \xrightarrow{\tau} \overline{R'_2} \xrightarrow{H'_2} Q'$ and $Q_2 \xrightarrow{\tau} \overline{R'_1} \xrightarrow{H'_1} Q'$ and $R_1 \xrightarrow{\tau} R'_1$ and $R_2 \xrightarrow{\tau} R'_2$ with $H'_i \subseteq H_i$. Finally, observe that $\overline{iA^*}(R'_i) \subseteq \overline{iA^*}(R_i)$ by Lem. 45 from which we infer $H'_i \cap (\overline{iA^*}(R'_i) \cup \{\tau\}) \subseteq H_i \cap (\overline{iA^*}(R_i) \cup \{\tau\})$. Thus, the reconverging reductions $Q_i \xrightarrow{\tau} \overline{R'_{3-i}} \xrightarrow{H'_{3-i}} Q'$ are again c-enabled. This was to be shown. ◀

Of Prop. 15. The first part of the statement follows directly from Def. 12(2): The c-actions $\ell: H_i[R_i]$ are trivially interference-free. Now if $P_1 \neq P_2$, then coherence gives us a strong environment shifts implying $\ell \in iA(R_1)$. The second part is because by Lem. 44(1) we have $R_i = 0$ and thus $iA(R_i) = \{\}$ when $\ell \in C$. ◀

► Lemma 55. Let $P_1 \models \pi$ and $P_2 \models \pi$ be coherent for the same pivot policy $\pi$. If $P_1$ and $P_2$ are single-threaded, then every admissible transition of $P_1 | P_2$ is c-enabled.

Proof. Consider an admissible transition of $P_1 | P_2$ where $P_1$ and $P_2$ are single-threaded. Firstly, by Lem. 44, each of the single-threaded processes can only generate c-actions $\ell_i: H_i[R_i]$ where $\tau \notin H_i$ and $R_i = 0$. Such transitions are always c-enabled for trivial reasons. Further, any rendez-vous synchronisation of such an $\ell_1: H_1[R_1]$ and $\ell_2: H_2[R_2]$ generates a c-action $\tau: (H_1 \cup H_2 \cup B)[R_1 | R_2]$ with $R_1 | R_2 = 0$. Because of Lem. 51, the set

$$B = \{\tau \mid H_1 \cap \overline{iA}(P_2) \subseteq \{\ell\} \text{ or } H_2 \cap \overline{iA}(P_1) \subseteq \{\overline{\ell}\}\}$$

must be empty. Thus, the reduction $\ell_1 | \ell_2$ is c-enabled, too. ◀

The following, slightly extended version of Prop. 23 says that a pivotable process cannot offer a clock action and exhibit another clock or a rendez-vous synchronisation at the same time. This means that in this class of processes, clocks and reductions are sequentially scheduled.

► Proposition 56 (Sequential Schedule and Clock Maximal Progress). Suppose $P$ is coherent and pivotable and $\sigma \in iA(P)$. Then, for all $\ell \in \mathcal{L}$ with $\ell \neq \sigma$ we have $\ell \notin iA(P)$ or $\overline{\ell} \notin iA(P)$. In particular, $P$ is in normal form, i.e., there is no reduction $P \xrightarrow{\tau} P'$.

Proof. The proof proceeds by contradiction. Let $P \models \pi$ for pivot policy $\pi$. Suppose $\ell \in \mathcal{L}$, $\ell \neq \sigma$ and $P \xrightarrow{\sigma} H_1 P_1$ and $P \xrightarrow{\ell} N_1 P_2$ and $P \xrightarrow{\overline{\ell}} M_1 P_2$. By Prop. 54 we infer $\sigma \in N$ or $\ell \in H$, i.e., by conformance Def. 17 we have $\pi \models \sigma \dashv\vdash \ell$ or $\pi \models \ell \dashv\vdash \sigma$. Hence, $\pi \not\models \sigma \diamond \ell$. For the same reason we have $\pi \not\models \sigma \diamond \overline{\ell}$. However, this contradicts the pivot property of $\pi$, which requires $\pi \models \sigma \diamond \ell$ or $\pi \models \sigma \diamond \overline{\ell}$. Finally, if $P \xrightarrow{\tau} P'$ then the reduction must arise from a rendez-vous synchronisation inside $P$, i.e., there is $\ell \in \mathcal{R}$ with $\ell \in iA(P)$ and $\overline{\ell} \in iA(P)$. But then $\sigma \in iA(P)$ is impossible as we have just seen. ◀

The proof of Thm. 24 will be conducted in the following Secs. D.1–D.4. It proceeds by induction on the structure of derivations in the SOS of CCS$^{spt}$, given in Fig. 2. We first show that the indirections of syntactic transformations via the static laws of Fig. 1, built into the SOS by the (Struct) rule, can in fact be eliminated in terms of a finite number of standard SOS rules that do not refer to structural laws.

► Definition 57. A process $P$ is called 0-free if either $P = 0$ or all occurrences of 0 in $P$ are guarded by a prefix $\ell:H.R$.
► **Proposition 58.** Every process *P* is structurally congruent to a 0-free process *Q*.

1523

**Proof.** By application of the laws $P \star 0 \equiv P$ and $0 \intercal L \equiv 0$, where $\star \in \{|, +\}$ and $\intercal \in \{\setminus, /\}$ we can eliminate every occurrence of 0 in an process $P$ that is not of the form $\alpha:H.0$. ◀

1524

1525

► **Proposition 59.** If *P* is a 0-free process, and there is a derivation *D* for $P \xrightarrow{\alpha/R} H * Q$, then all uses of the rule (Struct) in *D* can be eliminated in terms of the following symmetric versions of the rules (Par) and (Sum):

$$ \frac{P \xrightarrow{\alpha/R} P'}{P + Q \xrightarrow{\alpha/R} P'} \quad (\text{Sum}_1) $$

$$ \frac{Q \xrightarrow{\alpha/R} Q'}{P + Q \xrightarrow{\alpha/R} Q'} \quad (\text{Sum}_2) $$

$$ \frac{P \xrightarrow{\alpha/R} P' \quad \alpha \notin \mathcal{C}}{P | Q \xrightarrow{\alpha/R} P' | Q} \quad (\text{Par}_1) $$

$$ \frac{Q \xrightarrow{\alpha/R} Q' \quad \alpha \notin \mathcal{C}}{P | Q \xrightarrow{\alpha/R} P | Q'} \quad (\text{Par}_2) $$

1526

More specifically, there is a derivation $D'$ for $P \xrightarrow{\alpha/R} H * Q'$ with $R' \equiv R$ and $Q' \equiv Q$.

**Proof Sketch.** By induction on the structure of processes one shows that the transitions generated by the SOS with (Struct) can be simulated by the extended SOS without (Struct). The argument is based on the following case analysis:

1527

1528

1529

■ If $P = 0$ then no process structurally equivalent to $P$ can generate any transition: If $P \equiv Q$ and $Q \xrightarrow{\alpha/R} H * Q'$ then $P \neq 0$. Hence, the statement of the proposition holds trivially.

1530

1531

■ For prefixes we show that if $P \equiv \ell:H.Q$ and $P \xrightarrow{\ell/E'} H * Q'$ then $\ell' = \ell$, $H' = H$, $E' \equiv 0$ and $Q' \equiv Q$.

1532

1533

■ For sums we observe that if $P \equiv P_1 + P_2$ and $P \xrightarrow{\ell/E} H * Q$ then there exists $i \in \{1, 2\}$ such that $P_i \xrightarrow{\ell/E'} H * Q'$ such that $E' \equiv E$ and $Q' \equiv Q$.

1534

1535

■ For all other operators, e.g. $P \equiv P_1 | P_2$, $P \equiv Q/L$, $P \equiv Q \setminus L$, we can easily show that transitions $P \xrightarrow{\alpha/R} H * P'$ can be obtained from transitions of $P_i$ and $Q$.

1536

1537

Note that the restriction in Prop. 59 is necessary. If $P$ is not 0-free, say $P = 0 | Q$, then we can have $0 | Q \xrightarrow{\sigma} Q'$ because of (Struct), because $0 | Q \equiv Q$ and $Q \xrightarrow{\sigma} Q'$, but without (Struct) we could not derive $0 | Q \xrightarrow{\sigma} Q'$.

1539

1540

1541

Because of Prop. 58 we may assume our processes are 0-free. Because of Prop. 59 we may prove the preservation of coherence (for 0-free processes) by induction on the SOS rules without considering (Struct), but including the symmetric rules (Par$_i$) and (Sum$_i$) for $i \in \{1, 2\}$.

1542

1543

1544

1545

## D.1 Stop and Prefixes

1546

► **Proposition 60.** The process 0 is coherent for any policy, i.e., $0 \models \pi$ for all $\pi$.

1547

**Proof.** The inactive process 0 is locally coherent for trivial reasons, simply because it does not offer any transitions at all. There is no SOS rule applicable to it in the (Struct)-free setting. Note that in the system with (Struct) rule, we would have to argue that no process structurally equivalent to 0 has any transitions. ◀

1548

1549

1550

1551

► **Proposition 61.** Let process *Q* be coherent for $\pi$. Then, for every action $\ell \in \mathcal{R}$ the prefix expression $\ell:H.Q$ is coherent for $\pi$, if $\ell \in H \subseteq \{\ell' | \ell' \dashrightarrow \ell \in \pi\}$.

1552

1553
1554
1555

**Proof.** A prefix expression $P = \ell:H.Q$ generates only a single transition by rule (Act), so that the assumption

$$
1556 \qquad P \xrightarrow[\mathcal{E}_1]{\alpha_1} H_1 Q_1 \text{ and } P \xrightarrow[\mathcal{E}_2]{\alpha_2} H_2 Q_2 \tag{1}
$$

implies $\alpha_i = \ell$, $H_i = H$, $E_i \equiv 0$ and $Q_i \equiv Q$. It is easy to see that $\ell:H.Q$ conforms to $\pi$ if $H \subseteq \{\beta \mid \beta \dashv\dashv \alpha \in \pi\}$. Since $\alpha_i = \ell \in H = H_i$ and $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ nothing needs to be proved. Finally, note that the only immediate derivative of $\alpha:H.Q$ is $Q$ which is coherent for $\pi$ by assumption.

Again, it is important to notice that the SOS with (Struct) would not immediately warrant the conclusion that both derivations (1) are by (Act). This is because these transitions could be the transitions of two syntactically distinct (but structurally congruent) expressions $P_1 \equiv P \equiv P_2$. Instead, we would have to argue that if $P = \ell:H.Q \equiv P'$ and $P' \xrightarrow{\alpha'} E' \xrightarrow{H'} Q'$ then $\alpha' = \ell$, $H' = H$, $E' \equiv 0$ and $Q' \equiv Q$. That this is the case is a property of our specific system of structural laws and handled by the above Prop. 59. This would obviously be violated, e.g., if we added a structural law like $\ell:H.Q \equiv \alpha':H'.Q'$ where $\alpha' \neq \ell$, $H' \neq H$, $E' \neq 0$ or $Q' \neq Q$. ◀

As Examples 8 and 9 show, a prefix $\ell:H.Q$ for $\ell \in \mathcal{R}$ can very well be coherent even if $\ell \notin H$. Here we note that for clock prefixes, the blocking set is only constrained by the policy.

► **Proposition 62.** If $Q$ is coherent for $\pi$ and $\sigma \in \mathcal{C}$ is a clock, then the prefix expression $\sigma:H.Q$ is coherent for $\pi$, too, if $H \subseteq \{\beta \mid \beta \dashv\dashv \sigma \in \pi\}$.

Proof. The argument runs exactly as in case of Prop. 61. However, we do not need to require condition $\sigma \in H$ because if $\alpha_i = \sigma$ then $\alpha_1 = \alpha_2$, $Q_1 \equiv Q_2$ and $\{\alpha_1, \alpha_2\} \notin \mathcal{R}$. So, no reconvergence is required. Again, we observe that the only immediate derivative of $\sigma:H.Q$ is $Q$ which is coherent for $\pi$ by assumption. ◀

1577

D.2 Summation

► **Proposition 63.** Let $P_1 \models \pi_1$ and $P_2 \models \pi_2$ be coherent and for all pairs of initial transitions
$P \xrightarrow[F_1]{\alpha_1} H_1 P_1$ and $P \xrightarrow[F_2]{\alpha_2} H_2 P_2$ we have $\alpha_1 \neq \alpha_2$ as well as $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$. Then $P_1 + P_2$
is coherent for $\pi$ if $\pi_1 \subseteq \pi$ and $\pi_2 \subseteq \pi$.

Proof. Let $P = Q + R$ be given with $Q$ and $R$ locally coherent for $\pi_1$ and $\pi_2$, respectively and the rest as in the statement of the proposition. Every transition of $P$ is either a transition of $Q$ or of $R$ via rules (Sum$_i$). Conformance to $\pi$ directly follows from the same property of $Q$ or $R$, respectively. The proof of coherence Def. 12 is straightforward, exploiting that two competing but non-interfering transitions must either be both from $Q$ or both from $R$. More precisely, suppose $P \xrightarrow[F_1]{\alpha_1} H_1 P_1$ and $P \xrightarrow[F_2]{\alpha_2} H_2 P_2$ with $\alpha_1 \neq \alpha_2$ or $P_1 \not\equiv P_2$ or $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$. Also, we assume that $\alpha_1:H_1[F_1]$ and $\alpha_2:H_2[F_2]$ are interference-free. Now if the two transitions of $P$ are by (Sum$_1$) from $Q$ or by (Sum$_2$) from $R$, then $\alpha_1 \in iA(Q)$ and $\alpha_2 \in iA(R)$. But then by assumption, $\alpha_1 \neq \alpha_2$ and $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$, which implies that $\alpha_1:H_1[F_1]$ and $\alpha_2:H_2[E_2]$ are not interference-free. This means, to prove coherence Def. 12(2) we may assume that both transitions of $P$ are either by (Sum$_1$) from $Q$ or both by (Sum$_2$) from $R$. Suppose both reductions of $P = Q + R$ are generated by rule (Sum$_1$), i.e., $Q \xrightarrow[F_1]{\alpha_1} H_1 Q_1$ and $Q \xrightarrow[F_2]{\alpha_2} H_2 Q_2$ where the transitions generated by (Sum$_1$) are $Q + R \xrightarrow[F_1]{\alpha_1} H_1 Q_1$ and $Q + R \xrightarrow[F_2]{\alpha_2} H_2 Q_2$. Under the given assumptions, the reconverging transitions of coherence Def. 12(2) are obtained directly from coherence of $Q$, by induction.
1596 The case that both transitions are from $R$ by rule $(Sum_2)$ is symmetrical. Finally, the
1597 immediate derivatives $P_1$ and $P_2$ of $P_1 + P_2$ are coherent for $\pi$, because they are coherent
1598 for $\pi_i$ by assumption and thus also for the common extension $\pi_i \subseteq \pi$. ◀

1599 D.3 Parallel

1600 ▶ Lemma 64 (Key lemma). Let $Q \Vdash \pi$ and $R \Vdash \pi$ be such that $\pi \setminus R$ is a pivot policy. Then
1601 $(Q|R) \Vdash \pi$.

**Proof.** Let $P = Q|R$ such that both $Q$ and $R$ are coherent for $\pi$ where $\pi \setminus R$ is a pivot policy. For conformance consider a transition

$$P \xrightarrow{\ell} E H P'$$

with $\ell \in \mathcal{L}$ and $\ell' \in H$. First suppose $\ell \notin \mathcal{C}$. Then this transition is not a synchronisation but a transition of either one of the sub-processes $Q$ by $(Par_1)$ or $P$ by $(Par_2)$ with the same blocking set $H$. In either case, we thus use coherence $Q \Vdash \pi$ or $R \Vdash \pi$ to conclude $\ell' \dashrightarrow \ell \in \pi$. If $\ell = \sigma$, then the transition in question is a synchronisation of $Q$ and $R$ via rule (Com)

$$Q|R \xrightarrow{\sigma} 0 H_2 \cup N_2 \cup B_2 Q_2|R_2$$

with $E \equiv 0$, $H = H_2 \cup N_2 \cup B_2$ and $P' = Q_2|R_2$ generated from transitions

$$Q \xrightarrow{\sigma} 0 H_2 Q_2 \text{ and } R \xrightarrow{\sigma} 0 N_2 R_2.$$

1602 and $B_2 = \{\ell | \bar{\ell} | H_2 \cap \overline{iA}(R) \notin \{\sigma\} \text{ or } N_2 \cap \overline{iA}(Q) \notin \{\sigma\}\}$. By Lem. 51 we have $B_2 = \{\}$.
1603 If we now take an arbitrary $\ell' \in H \cap \mathcal{L}$ then $\ell' \in H_2$ or $\ell' \in N_2$. In these cases, we obtain
1604 $\ell' \dashrightarrow \ell \in \pi$ by conformance Def. 17 from $Q \Vdash \pi$ or $R \Vdash \pi$.

In the sequel, we tackle coherence Def. 12. As before, we work in the SOS without $(Struct)$ but with symmetrical rules $(Par_i)$. First we observe that the immediate derivatives of $Q|R$ are always parallel compositions $Q'|R'$ of derivatives of $Q$ and $R$. Thus, we may assume that the immediate derivatives $Q'|R'$ are coherent for $\pi$ because coherence of $P$ and $Q$ is preserved under transitions (i.e., by co-induction). Now suppose

$$P \xrightarrow{\alpha_1} E_1 H_1 P_1 \text{ and } P \xrightarrow{\alpha_2} E_2 H_2 P_2$$

such that $\alpha_1 \neq \alpha_2$ or $P_1 \neq P_2$ or $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$. Moreover, the c-actions $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are interference-free. We argue reconvergence by case analysis on the rules that generate these transitions. These could be $(Par_1)$, $(Par_2)$ or $(Com)$. First note that by Lem. 51 we can drop the consideration of the synchronisation action $\ell | \bar{\ell}$ for the blocking set in $(Com)$ altogether:

$$\frac{P \xrightarrow{\ell} R_1 H_1 P' \quad Q \xrightarrow{\bar{\ell}} R_2 H_2 Q'}{P | Q \xrightarrow{\ell | \bar{\ell}} R_1 | R_2 H_1 \cup H_2 P' | Q'} \quad (Com)$$

1605 We will use the name $(Com_a)$ to refer to the instance of $(Com)$ with $\ell \in \mathcal{R}$ and the name $(Com_\sigma)$ for the instance with $\ell \in \mathcal{C}$ and we proceed by case analysis.

■ $(Par_1, Par_2) \diamond (Com_a)$. We start with the case where one of the reductions to $P_i$ is non-synchronising by $(Par_1)$ or $(Par_2)$ and the second reduction to $P_{3-i}$ is a synchronisation
obtained by (Com$_a$). By symmetry, it suffices to consider the case that the non-synchronising transition is by (Par$_1$) from $Q$, i.e., $\alpha_1 \notin C$ and $\alpha_2 = \ell | \bar{\ell}$ and

$$Q | R \xrightarrow{\frac{\alpha_1}{F_1} | R} H_1 Q_1 | R \text{ and } Q | R \xrightarrow{\frac{\ell | \bar{\ell}}{F_2 | G_2}} H'_2 \cup N_2 Q_2 | R_2$$

with $E_1 = F_1 | R$, $E_2 = F_2 | G_2$, $H_2 = H'_2 \cup N_2$, $P_1 = Q_1 | R$ and $P_2 = Q_2 | R_2$, where $\ell \in \mathcal{R}$ is a rendezvous action such that

$$Q \xrightarrow{\frac{\alpha_1}{F_1}} H_1 Q_1 \text{ and } Q \xrightarrow{\frac{\ell}{F_2}} H'_2 Q_2 \text{ and } R \xrightarrow{\frac{\bar{\ell}}{G_2}} N_2 R_2.$$

We may safely assume $\alpha_1 \neq \ell | \bar{\ell} = \tau$ or $Q_1 | R \neq Q_2 | R_2$. The third case $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ is excluded since $\alpha_2 = \tau$. Further, suppose the c-actions $\alpha_1:H_1[F_1|R]$ and $\ell|\bar{\ell}:(H'_2 \cup N_2)[F_2|G_2]$ are non-interfering. Observe that $\{\alpha_1, \ell|\bar{\ell}\} \notin \mathcal{R}$ and also $\{\alpha_1, \ell|\bar{\ell}\} \cap C = \{\}$. Thus only a weak environment shift is needed. We wish to exploit coherence of $Q$. The first observation is that since $\alpha_2 = \tau$, the assumptions on non-interference Def. 11(2) implies that $H_1 \cap \bar{\mathbb{A}}^*(F_1|R) = \{\}$. Since $\ell = \bar{\ell} \in \bar{\mathbb{A}}(R) \cap \mathcal{L} \subseteq \bar{\mathbb{A}}^*(F_1|R)$ by Lem. 44 and Lem. 45, this implies that $\ell \notin H_1$ up front. Next, if $\alpha_1 \neq \ell | \bar{\ell}$, non-interference Def. 11(1) means $\alpha_1 \notin H_2 = H'_2 \cup N_2$ and thus $\alpha_1 \notin H'_2$. The same is true if $\alpha_1 = \ell | \bar{\ell} = \tau$, but then by non-interference Def. 11(2) we have the non-interference equation

$$(H'_2 \cup N_2) \cap (\bar{\mathbb{A}}^*(F_2 | G_2) \cup \{\tau\}) = H_2 \cap (\bar{\mathbb{A}}^*(E_2) \cup \{\tau\}) = \{\}$$

from which $\alpha_1 = \tau \notin H'_2$ follows. This settles the first part of the non-interference property Def. 11(1) for the diverging transitions out of $Q$.

For the second part of non-interference, suppose $\alpha_1 = \tau$. Then the non-interference assumption implies that $H'_2 \cap \bar{\mathbb{A}}^*(F_2|G_2) = \{\}$. Now since $\bar{\mathbb{A}}^*(F_2) \subseteq \bar{\mathbb{A}}^*(F_2|G_2)$ we conclude from this that $H'_2 \cap \bar{\mathbb{A}}^*(F_2) = \{\}$. This completes the proof that the c-actions $\alpha_1:H_1[F_1]$ and $\ell:H'_2[F_2]$ must be non-interfering in all cases.

Note that we always have $\alpha_1 \neq \ell$ or $\{\alpha_1, \ell\} \subseteq \mathcal{R}$, and in the latter case also $\alpha_1 \notin H'_2$ and $\ell \notin H_1$ from the above. Hence, we can use coherence Def. 12 of $Q$ and obtain processes $F'_1, F'_2, Q'$ with reconverging transitions

$$Q_1 \xrightarrow{\frac{\ell}{F'_2}} H''_2 Q' \text{ and } Q_2 \xrightarrow{\frac{\alpha_1}{F'_1}} H'_1 Q'$$

such that $H''_2 \subseteq H'_2$ and $H'_1 \subseteq H_1$. We now invoke (Com$_a$) and (Par$_1$) to obtain reconverging transitions

$$Q_1 | R \xrightarrow{\frac{\ell}{F'_2} | \bar{\ell}} H''_2 \cup N_2 Q' | R_2 \text{ and } Q_2 | R_2 \xrightarrow{\frac{\alpha_1}{F'_1} | R_2} H'_1 Q' | R_2$$

such that $H'_1 \subseteq H_1$ and $H''_2 \cup N_2 \subseteq H'_2 \cup N_2$. Regarding the concurrent environments, if $\alpha_1 \in \mathcal{R}$ then the coherence of $Q$ guarantees that $F_1 \xrightarrow{\ell} F'_1$ and $F_2 \xrightarrow{\alpha_1} F'_2$ from which we infer $F_2 | G_2 \xrightarrow{\alpha_1} F'_2 | G_2$ and $F_1 | R \xrightarrow{\ell | \bar{\ell}} F'_1 | R_2$.

If $\alpha_1 = \tau$ the above guarantee from the coherence of $Q$ is weaker: We only have $F_1 \xrightarrow{\ell} F'_1$ and $F_2 \xrightarrow{\alpha_1} F'_2$. In any case we obtain the environment shifts $F_2 | G_2 \xrightarrow{\alpha_1} F'_2 | G_2$ and $F_1 | R \xrightarrow{\ell | \bar{\ell}} F'_1 | R_2$, as required.

■ (Par$_1$) ♦ (Par$_2$): Suppose the two non-interfering transitions of $P = Q|R$ are by (Par$_1$) from $Q$ and (Par$_2$) from $R$. Thus, we are looking at transitions

$$Q \xrightarrow{\frac{\alpha_1}{F_1}} H_1 Q_1 \text{ and } R \xrightarrow{\frac{\alpha_2}{F_2}} H_2 R_2$$
for {$\alpha_1, \alpha_2$} $\subseteq \mathcal{R}$ $\cup$ $\{\tau\}$ combined via (Par) to generate

$$Q | R \xrightarrow[\overline{F_1}|R]{\alpha_1} H_1 Q_1 | R \text{ and } Q | R \xrightarrow[\overline{Q}|\overline{F_2}]{\alpha_2} H_2 Q | R_2$$

with $E_1 = F_1 | R$ and $E_2 = Q | F_2$. Then we can directly construct reconverging transitions, applying (Par) for

$$Q_1 | R \xrightarrow[\overline{Q_1}|\overline{F_2}]{\alpha_2} H_2 Q_1 | R_2 \text{ and } Q | R_2 \xrightarrow[\overline{F_1}|\overline{R}]{\alpha_1} H_1 Q_1 | R_2.$$

Obviously, $Q_1 | R_2$ reduces to $Q_1 | R_2$ and by (Par$_1$) and (Par$_2$) we also have the strong environment shifts $F_1 | R \xrightarrow{\alpha_2} F_1 | R_2$ and $Q | F_2 \xrightarrow{\alpha_1} Q_1 | F_2$ which completes the claim for we have, in particular, $F_1 | R \xrightarrow{\alpha_2} F_1 | R_2$ and $Q | F_2 \xrightarrow{\alpha_1} Q_1 | F_2$. Notice that in this case we do not need to assume that $Q$ or $R$ are coherent, i.e., the assumption that the c-actions $\alpha_i:H_i[E_i]$ are interference-free.

($Par_i$) $\diamond$ ($Par_i$) for $i \in \{1, 2\}$: Suppose both non-interfering and diverging reductions are by (Par$_1$) from $Q$ (or symmetrically, both by (Par$_2$) from $R$). Then,

$$Q | R \xrightarrow[\overline{F_1}|R]{\alpha_1} H_1 Q_1 | R \text{ and } Q | R \xrightarrow[\overline{F_2}|R]{\alpha_2} H_2 Q_2 | R$$

with {$\alpha_1, \alpha_2$} $\subseteq \mathcal{R}$ $\cup$ $\{\tau\}$ and $P_i = Q_i | R$, $E_i = F_i | R$, where

$$Q \xrightarrow[\overline{F_1}]{\alpha_1} H_1 Q_1 \text{ and } Q \xrightarrow[\overline{F_2}]{\alpha_2} H_2 Q_2$$

with $\alpha_1 \neq \alpha_2$ or $Q_1 | R \neq Q_2 | R$ or {$\alpha_1, \alpha_2$} $\subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$. This, in particular, implies $Q_1 \neq Q_2$. Further, assume non-interference of $\alpha_i:H_i[F_i|R]$. We obtain non-interference of $\alpha_i:H_i[F_i]$ by Prop. 46. We can therefore apply coherence Def. 12 of $Q$ and obtain processes $F'_1, F'_2$ and $Q'$ with reconverging transitions

$$Q_1 \xrightarrow[\overline{F'_2}]{\alpha_2} H'_2 Q' \text{ and } Q_2 \xrightarrow[\overline{F'_1}]{\alpha_1} H'_1 Q'$$

with $H'_i \subseteq H_i$ and such that

$$F_1 \xrightarrow{\alpha_2} F'_1 \text{ and } F_2 \xrightarrow{\alpha_1} F'_2 \qquad (2)$$

and if {$\alpha_1, \alpha_2$} $\subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $Q_1 \neq Q_2$, more strongly

$$F_1 \xrightarrow{\alpha_2} F'_1 \text{ and } F_2 \xrightarrow{\alpha_1} F'_2. \qquad (3)$$

Reapplying (Par$_1$) we construct the transitions

$$Q_1 | R \xrightarrow[\overline{F'_2}|R]{\alpha_2} H'_2 Q' | R \text{ and } Q_2 | R \xrightarrow[\overline{F'_1}|R]{\alpha_1} H'_1 Q' | R.$$

Obviously, by (Par$_1$) and (Par$_2$) we also obtain transitions $F_1 | R \xrightarrow{\alpha_2} F'_1 | R$ and $F_2 | R \xrightarrow{\alpha_1} F'_2 | R$ from (2) or, more strongly, $F_1 | R \xrightarrow{\alpha_2} F'_1 | R$ and $F_2 | R \xrightarrow{\alpha_1} F'_2 | R$ from (3) if {$\alpha_1, \alpha_2$} $\subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $Q_1 | R \neq Q_2 | R$.

($Com_a$) $\diamond$ ($Com_a$): This is the most interesting case in which we are going to exploit the assumption that $Q$ and $R$ are coherent for the same pivot policy $\pi$. Without loss of generality we assume $P = Q | R$ and both the reductions

$$Q | R \xrightarrow[\overline{E_i}]{\alpha_i} H_i \cup N_i Q_i | R_i$$

with $P_i = Q_i | R_i$ are $\tau$-actions generated by the communication rule (Com), i.e. $\alpha_1 = \ell_1 | \overline{\ell_1} = \tau = \ell_2 | \overline{\ell_2} = \alpha_2$ for actions $\ell_i \in \mathcal{R}$. Since $\alpha_1 = \alpha_2$ and {$\alpha_1, \alpha_2$} = {$\tau$} $\notin \mathcal{R}$ we
Thus, we are looking at transitions

$$Q \xrightarrow{\ell_i}{F_i} H_i Q_i \text{ and } R \xrightarrow{\bar{\ell}_i}{G_i} N_i R_i.$$

$$Q_1 \xrightarrow{\ell_2}{F'_2} H'_2 Q' \text{ and } Q_2 \xrightarrow{\ell_1}{F'_1} H'_1 Q'.$$

$$R_1 \xrightarrow{\bar{\ell}_2}{G'_2} N'_2 R' \text{ and } R_2 \xrightarrow{\bar{\ell}_1}{G'_1} N'_1 R'.$$

with $N'_i \subseteq N_i$. Finally, we invoke (Com) to obtain the re-converging reductions

$$Q_1 | R_1 \xrightarrow{\ell_2 | \bar{\ell}_2}{F'_2} H'_2 \cup N'_2 Q' | R' \text{ and } Q_2 | R_2 \xrightarrow{\ell_1 | \bar{\ell}_1}{F'_1} H'_1 \cup N'_1 Q' | R'$$

with $H'_i \cup N'_i \subseteq H_i \cup N_i$, and also

$$F_i | G_i \xrightarrow{\ell_{3-i} | \bar{\ell}_{3-i}} F'_i | G'_i$$

<footnote n="1633">1633 only need to prove confluence the case that $P_1 \neq P_2$, i.e., $Q_1 \neq Q_2$ or $R_1 \neq R_2$. Moreover, we only need a weak environment shift, because $\{\alpha_1, \alpha_2\} = \{\tau\} \notin \mathcal{R}$ and $\{\alpha_1, \alpha_2\} \cap \mathcal{C} = \{\}$. 1634</footnote>

<footnote n="1635">1635 Also, non-interference Def. 11(2) means that $(H_i \cup N_i) \cap (i\bar{A}^*(E_i) \cup \{\tau\}) = \{\}$, i.e.,</footnote>

<footnote n="1636">1636 $H_i \cap (i\bar{A}^*(E_i) \cup \{\tau\}) = \{\}$ and $N_i \cap (i\bar{A}^*(E_i) \cup \{\tau\}) = \{\}$. (4)</footnote>

<footnote n="1637">1637 We claim that the two c-actions $\ell_i:H_i[F_i]$ of $Q$, and likewise the two c-actions $\bar{\ell}_i:N_i[G_i]$ of $R$, are interference-free. Note that since $\ell_i \neq \tau$, we only need to consider the first part of Def. 11(1). We first show that at least one of these pairs of c-actions must be interference free, because of coherence and conformance to $\pi$ where $\pi \setminus \mathcal{R}$ is a pivot policy. It will then transpire that the other must be interference-free, too, because of the assumption (4).</footnote>

<footnote n="1638">1638 Obviously, if $\ell_1 = \ell_2$ then both $\ell_i:H_i[F_i]$ of $Q$ and $\bar{\ell}_i:N_i[G_i]$ are interference-free for 1639 trivial reasons. We distinguish two cases depending on whether $\ell_1$ and $\ell_2$ are identical or 1640 not. So, suppose $\ell_1 \neq \ell_2$. Both $Q$ and $R$ are coherent for the same policy $\pi$ and $\pi \setminus \mathcal{R}$ is 1641 a pivot policy. Thus, $\ell_1 \diamond \ell_2 \in \pi$ or $\bar{\ell}_1 \diamond \bar{\ell}_2 \in \pi$, by Def. 48. Hence, $\ell_i \notin H_{3-i}$ or $\bar{\ell}_i \notin N_{3-i}$ 1642 by conformance Def. 17, which means that at least one of the pairs of c-actions $\ell_i:H_i[F_i]$ 1643 of $Q$ or the two c-actions $\bar{\ell}_i:N_i[G_i]$ must be interference-free by policy. 1644</footnote>

<footnote n="1645">1645 Now we argue that if $\ell_1 \neq \ell_2$ and one of the pairs $\ell_i:H_i[F_i]$ or $\bar{\ell}_i:N_i[G_i]$ is interference-free the other must be, too, and so we can close the diamond for both $Q$ and $R$. By symmetry, it suffices to run the argument in case that the c-actions $\ell_i:H_i[F_i]$ of $Q$ are non-interfering. Then, we have $\{\ell_1, \ell_2\} \subseteq \mathcal{R}$ and $\ell_i \notin H_{3-i}$. Hence, we invoke coherence Def. 12 of $Q$ obtaining processes $F'_1$ and $F'_2$ with transitions (strong environment shift) $F_1 \xrightarrow{\ell_2} F'_1$ and $F_2 \xrightarrow{\ell_1} F'_2$ and a process $Q'$ with transitions</footnote>

<footnote n="1646">1646 such that $H'_i \subseteq H_i$. This means $\ell_i \in i\mathcal{A}(F_{3-i}) \subseteq i\mathcal{A}(F_{3-i} | G_{3-i}) = i\mathcal{A}(E_{3-i}) \subseteq i\mathcal{A}^*(E_{3-i})$ and therefore $\bar{\ell}_i \notin N_{3-i}$ because of (4). Thus, as claimed, the c-actions $\bar{\ell}_i:N_i[G_i]$ are interference-free, too. Again $\{\bar{\ell}_1, \bar{\ell}_2\} \subseteq \mathcal{R}$ and $\bar{\ell}_i \notin N_{3-i}$ entitles us to exploit coherence Def. 12 for $R$ from which we obtain processes $G'_1$ and $G'_2$ with transitions (again, a strong environment shift) $G_1 \xrightarrow{\bar{\ell}_2} G'_1$ as well as $G_2 \xrightarrow{\bar{\ell}_1} G'_2$ as well as a process $R'$ with</footnote>

<footnote n="1648">1648 as required, since this implies the weaker form $F_i | G_i \rightsquigarrow F'_i | G'_i$ of environment shift. It remains to consider the case that $\ell_1 = \ell = \ell_2$. By assumption $P_1 \neq P_2$ and so we must have $Q_1 \neq Q_2$ or $R_1 \neq R_2$. Suppose $Q_1 \neq Q_2$. If $R_1 \neq R_2$ we apply a symmetric argument with the role of $\ell_i$ and $\bar{\ell}_i$ interchanged. As observed above, the c-actions $\ell_i:H_i[F_i]$ are trivially interference-free according to Def. 11, because $\ell_1 = \ell_2$ and $\ell_i \neq \tau$. Then, by coherence Def. 12 applied to $Q$ we conclude that there are processes $F'_1$ and</footnote>
$F'_2$ with transitions $F_1 \xrightarrow{\ell} F'_1$ and $F_2 \xrightarrow{\ell} F'_2$ and a process $Q'$ with transitions (the strong environment shift arises here because we have $\ell \in \mathcal{R}$ and $Q_1 \neq Q_2$)

$$Q_1 \xrightarrow{\ell} F'_2 Q' \text{ and } Q_2 \xrightarrow{\ell} F'_1 Q'$$

such that $H'_i \subseteq H_i$. This means that $\ell \in i\mathcal{A}(F_{3-i}) \subseteq i\mathcal{A}(E_{3-i})$ and so $\bar{\ell} \notin N_{3-i}$ because of $N_{3-i} \cap i\mathcal{A}^*(E_{3-i}) = \{\}$ as per (4). If $R_1 \equiv R_2$ then for each $i \in \{1, 2\}$, by coherence Def. 12 (as $\bar{\ell} \notin N_{3-i} \cup \mathcal{C}$) there is a transition

$$R_i \xrightarrow{\bar{\ell} \atop G'_{3-i}} N'_{3-i} R'$$

with $N'_i \subseteq N_i$ and $G_i \equiv G'_i$ or $G_i \xrightarrow{\bar{\ell}} G'_i$. Using these transitions we now recombine

$$Q_i | R_i \xrightarrow{\ell | \bar{\ell} \atop F'_{3-i} | G'_{3-i}} H'_{3-i} \cup N'_{3-i} Q' | R'$$

with $H'_i \cup N'_i \subseteq H_i \cup N_i$. Note that if $G_i \equiv G'_i$ then

$$F_i | G_i \xrightarrow{\ell} F'_i | G_i = F'_i | G'_i$$

or if $G_i \xrightarrow{\bar{\ell}} G'_i$ then

$$F_i | G_i \xrightarrow{\ell | \bar{\ell}} F'_i | G'_i.$$

This means that, in all cases, $F_i | G_i \xrightarrow{\ell | \bar{\ell}} F'_i | G'_i$ as desired. If $R_1 \neq R_2$ we can apply coherence Def 12 to $R$ in the same way and close the diamond with processes $G'_1$ and $G'_2$ and transitions (again, the strong environment shift arises here because we have $\bar{\ell} \in \mathcal{R}$ and $R_1 \neq R_2$) $G_1 \xrightarrow{\bar{\ell}} G'_1$ and $G_2 \xrightarrow{\bar{\ell}} G'_2$ as well as a process $R'$ with

$$R_1 \xrightarrow{\bar{\ell} \atop G'_{2}} N'_{2} R' \text{ and } R_2 \xrightarrow{\bar{\ell} \atop G'_{1}} N'_{1} R'$$

with $N'_i \subseteq N_i$. Finally, we invoke (Com) to obtain the re-converging reductions

$$Q_1 | R_1 \xrightarrow{\ell | \bar{\ell} \atop F'_2 | G'_2} H'_2 \cup N'_2 Q' | R' \text{ and } Q_2 | R_2 \xrightarrow{\ell | \bar{\ell} \atop F'_1 | G'_1} H'_1 \cup N'_1 Q' | R'$$

with $H'_i \cup N'_i \subseteq H_i \cup N_i$, and also $F_i | G_i \xrightarrow{\ell | \bar{\ell}} F'_i | G'_i$ which also implies $F_i | G_i \xrightarrow{\ell | \bar{\ell}} F'_i | G'_i$ as required.

1649

1650

(Com$_a$) ♦ (Com$_\sigma$) and, by symmetry, the induction case (Com$_\sigma$) ♦ (Com$_a$): We assume $P = Q | R$ and the non-interfering, diverging reductions

$$Q | R \xrightarrow{\ell | \bar{\ell} \atop E_1} H_1 \cup N_1 \cup B_1 Q_1 | R_1 \text{ and } Q | R \xrightarrow{\sigma \atop 0} H_2 \cup N_2 \cup B_2 Q_2 | R_2$$

for $\ell \in \mathcal{L}$, $\sigma \in \mathcal{C}$, with $P_i = Q_i | R_i$ and $E_i = F_i | G_i$ are generated by instances (Com$_a$) and (Com$_\sigma$) of the communication rules, respectively. These transitions arise from

$$Q \xrightarrow{\ell} F_1 Q_1 \text{ and } R \xrightarrow{\bar{\ell}} N_1 R_1 \text{ and } Q \xrightarrow{\sigma \atop 0} H_2 Q_2 \text{ and } R \xrightarrow{\sigma \atop 0} N_2 R_2.$$

1651

1652

1653

We assume that the c-actions $(\ell | \bar{\ell}):(H_1 \cup N_1 \cup B_1)[E_1]$ and $\sigma:(H_2 \cup N_2 \cup B_2)[0]$ are non-interfering. Note that $\ell \neq \sigma$ and $\bar{\ell} \neq \sigma$. First, observe that by Lem. 51, $B_1 = \{\} = B_2$. Also, $\ell | \bar{\ell} = \tau \neq \sigma$ and so the non-interference assumption means that $\sigma \notin H_1 \cup N_1 \cup B_1$.