Inria, FrancePartially funded by ETSI. University of Bamberg, GermanyPartially
funded by UniCA/I3S. Liquori and Mendler Theory of computation, Process
algebras

###### Acknowledgements.

The authors wish to thanks all the Synchron’23 participants for their useful
comments. The second author is grateful to Martin Steffen and Gerald Lüttgen
for helpful discussions.

# Strong Priority and Determinacy in Timed CCS

Luigi Liquori  Michael Mendler

###### Abstract

Building on the classical theory of process algebra with priorities, we
identify a new scheduling mechanism, called (sequentially) constructive
reduction which is designed to capture the essence of synchronous programming.
The distinctive property of this evaluation strategy is to achieve
determinism-by-construction for multi-cast concurrent communication. In
particular, it permits us to model shared memory multi-threading with reaction
to absence as it lies at the core of the programming language Esterel. In the
technical setting of CCS extended by clocks and priorities, we prove for a
large class of processes, which we call structurally coherent the confluence
property for constructive reductions. We further show that under some
syntactic restrictions, called pivotable the operators of prefix, summation,
parallel composition, restriction and hiding preserve structural coherence.
This covers a strictly larger class of processes compared to those that are
confluent in Milner’s classical theory of CCS without priorities.

###### keywords:

Timed process algebras, determinacy, priorities, synchronous programming

##  1 Introduction

Classical process algebras, like CCS [22], CSP [16], $\Pi$-calculus [24, 25],
just to mention a few, have been devised as a model of concurrency where a
system and its environment continuously interact to mutually control each
other’s behaviour through synchronisation and communication actions. This
contrasts with automata theory where the interaction is single-pass: The
environment provides a sequence of input actions to be fully consumed by the
automaton before it outputs a result. This result is a decision value,
determining if the string is accepted or not. The difference is reflected in
the semantical theory:

  * •

Process algebras are based on forms of bisimulation equivalence [20, 35], a
game-theoretic notion. Two processes are equivalent if they define the same
interaction game.

  * •

Traditional automata theory is based on language equality, which is a
functional model. Two programs are equivalent if they implement the same
decision function.

These two modes of interaction are usually treated independently.
Specifically, process algebras are typically applied for asynchronous systems,
which are inherently non-deterministic. Functional models are used for
synchronous systems which are inherently deterministic.

However, there are models of computation in which the game-theoretic and the
functional mode are combined. In the domain of Synchronous Programming,
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 defined at the
point where all components pause to wait for a global logical clock. When this
clock arrives, all components proceed into the next computation cycle. Under
the so-called synchrony hypothesis111The “synchrony hypothesis” assume that
the reaction of a component to input happens faster than the environment is
able to produce new stimulus: the time needed to compute the reaction is
unobservable by the environment. Also known as the “zero-time” assumption [17]
or “fundamental mode operation” [33]., the final outcome of a macro-step for
each component 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 (a game-theoretic
process) can be abstracted into a global Mealy automaton (a deterministic IO-
function). This synchronous model of computation has been very successful
historically, replacing analogue and asynchronous circuits, dominating
hardware design up to today. Synchronous models started with Statecharts [14]
and has generated languages such as Signal [11], Lustre [13], Esterel [3],
Quartz [31], SCCharts [36], just to mention a few.

In this paper we take a fresh look at the synchronous process algebras as a
combination of game-theoretic and functional models. Specifically, we bring
together two concepts for CCS that have previously been studied independently,
viz. clocks and priorities. By strengthening the notion of process priority
[7, 30, 27] in a natural way to what we call strong priorities or precedence
policies, and combining this with the idea of a clock [12, 8, 26, 21], we
obtain an adequate compositional setting for synchronous programming that
reconciles non-determinism with functional reactions. This is surprising since
many different hand-crafted semantics have been developed over the years but
none of them fits into the classical framework of CCS.

###  1.1 Resolving Nondeterminism

Concurrency, by expression or by implementation, is both a convenient and
unavoidable feature of modern software systems. Functional determinism is
crucial for maintaining predictability and to manage design complexity by
simple mathematical models [19, 6, 10]. If all primitive data manipulations
are deterministic (as in the $\lambda$-calculus), then non-determinism arises
either from unpredictable input data or the unpredictable timing of
communication actions. External non-determinism that is resolved by the input
data is innocuous. A process that waits for input and then branches control
depending on the value of the input is functionally predictable. If the input
can arrive from different concurrent senders, then non-determinism arises if
the external timing is unobservable. For instance, the behaviour of a shared
data object, in general, may depend on the order in which two method calls are
executed on it. This creates non-determinism if the actions do not commute,
i.e. if the object’s state transitions are not confluent. The three standard
ways to resolve data races and achieve confluence are isolation, cloning and
precedence. Let us discuss these briefly. If actions $\alpha_{1}$ and
$\alpha_{2}$ affect two concurrently independent parts of $Q$, say,
$Q\stackrel{{{}_{\mathit{def}}}}{{=}}\alpha_{1}.Q_{1}\,|\,\alpha_{2}.Q_{2},$
then commutation is guaranteed. The parallel composition $P\,|\,Q\,|\,R$ ends
up in configuration $P_{1}\,|\,Q_{1}\,|\,Q_{2}\,|\,R_{2}$ no matter which of
$P$ or $R$ communicates first, and with which of the two concurrent parts of
$\alpha_{1}.Q_{1}$ or $\alpha_{2}.Q_{2}$ of $Q$ they synchronise with if
$\alpha_{1}$ and $\alpha_{2}$ are indistinguishable. This is the method of
isolation which is captured naturally by the parallel operator of process
algebras. Another solution is to clone a resource unboundedly often, via a
repetition operator. If $\alpha_{1}{=}\alpha{=}\alpha_{2}$ and
$Q\stackrel{{{}_{\mathit{def}}}}{{=}}\alpha^{\ast}.\,Q^{\prime}$ means the
prefix $\alpha$ is repeated infinitely often, i.e., $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{}\,$}(Q^{\prime}\,|\,\alpha^{\ast}.\,Q^{\prime})$,
then $Q$ will offer $\alpha$ to both processes $P$ and $R$ independently by
cloning the residual $Q^{\prime}$. The parallel composition $P\,|\,Q\,|\,R$
will always end up in configuration
$P_{1}\,|\,Q^{\prime}\,|\,Q^{\prime}\,|\,Q\,|\,R_{2}$ when both $P$ and $R$
have finished their communication with $Q$. In all cases, the shared object
$Q$ does not really care about the ordering in which $\alpha_{1}$ and
$\alpha_{2}$ are executed. Yet, what if the behaviour of a process $Q$ must
depend on the choice between $\alpha_{1}$ and $\alpha_{2}$? Then, the
canonical solution is to enforce a scheduling precedence on the actions of the
environment in order to preserve coherence of the resource. Technically, if
$Q=\alpha_{1}.Q_{1}+\alpha_{2}.Q_{2}$ represents a conflicting choice of
actions $\alpha_{i}$ leading to distinct states $Q_{i}$, then we may restrict
the concurrent environment $E=P\,|\,{[\cdot]}\,|\,R$ in the following ways:

  * •

If $Q$ is a store where $\alpha_{1}=a{?}v$ is a data input and
$\alpha_{2}=a{!}w$ an output, we want the input take precedence over the
output to implement data-flow causality. Let us write $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{\\{\alpha_{1}\\}}}\,$}Q_{2}$
to express that the output $\alpha_{2}$ only synchronises with a matching
$\overline{\alpha_{2}}$ action if the environment $E$ does not offer to engage
in an input $\overline{\alpha_{1}}$ at the same time. In contrast, the input
action $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{\\{\\}}}\,$}Q_{1}$
is not blocked by the output $\alpha_{2}$.

  * •

Sometimes an ordering does not make sense, say if $\alpha_{1}=a{?}v$ and
$\alpha_{2}=a{?}w$ are inputs of distinct values $v\neq w$ to be received by
$Q$. Since these actions make $Q$ take on distinct continuation states
$Q_{1}\neq Q_{2}$, the environment $E$ must be blocked as it attempts to
engage in both $\alpha_{1}$ and $\alpha_{2}$, concurrently from $P$ and from
$R$. This can be modelled as a precedence of $\alpha_{1}$ over $\alpha_{2}$
and $\alpha_{2}$ over $\alpha_{1}$ which generates transitions
$Q_{2}\xleftarrow[\raisebox{-1.99997pt}[0.0pt][0.0pt]{$$}]{\alpha_{2}}\\!\\!{{}_{\\{\alpha_{1}\\}}}\,Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{\\{\alpha_{2}\\}}}\,$}Q_{1}.$

As such, precedences can be used to resolve the timing uncertainty about which
one of two distinct (conflicting) action steps is taken by a shared process
and further, for this action step, resolve the uncertainty about which of
several concurrent processes in its environment is consuming it. In this paper
we use CCS as our formalism to study the use of precedences for achieving
determinism. Similar ideas might be possible for other process algebras like
SCCS, CSP or the $\pi$-calculus. We find CCS most plausible as a point of
departure since the concept of priorities (which is very related) is already
well established in CCS. Also, in CCS, the combination of synchronous
communication with consumable prefixes and asynchronous scheduling via local
rendezvous synchronisation makes the problem of generating determinacy more
prominent. Isolation and cloning are well-known techniques to achieve
determinism in process algebras, see e.g., Chap. 11 of [22]. However,
scheduling priorities do not seem to have been systematically used for that
purpose. In this paper we propose _precedence policies_ as a refinement of
existing priority schemes for CCS for achieving determinism. Similar ideas
might be possible for other process algebras like SCCS, CSP or the
$\pi$-calculus.

Few papers extending CCS have been of great inspiration of this paper, namely
the Camilleri-Winskell $\mathsf{CCS}^{\mathsf{CW}}$ [7], the Phillips
$\mathsf{CCS}^{\mathsf{Ph}}$ [27], and and Cleaveland-Lüttgen-Natarajan
$\mathsf{CCS}^{\mathsf{CLN}}$ [30] extensions of CCS with some priority
choices, together with Chap. 11 of Milner’s book introducing the CCS dialect
$\mathsf{CCS}^{\mathsf{cc}}$. A fairly informal presentation and comparison of
those algebras can be found in App. A. Nevertheless, none of them has been
able to reach full confluence, _conditio sine qua non_ to set up a solid basis
for semantic of synchronous programming. This paper argues that adding
broadcasting actions like _synchronous clocks_ to the above proposals is a
sufficient condition to reach confluence. Clocks are a well-known notion from
Timed Process Algebras, like e.g. TPL [15], PMC [12] and CSA [8]. Intuitively,
a clock $\sigma$ is a “broadcast action” in the spirit of Hoare’s CSP [16]
that acts as a synchronisation barrier for a set of concurrent processes. It
bundles each process’ 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 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 sequential circuits [33] and VHDL [17], or synchronous programming like
Esterel [3], Lustre [13], SCCharts [36], BSP [34], 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. The idea is that the clock should fire only if the system has
stabilised and no other admissible data actions are possible (maximal
progress) is a standard assumption in timed process algebras [15, 8].
Combining prioritised rendez-vous with broadcast actions in a Plotkin SOS
style and discovering that an interleaving of micro- and macro-steps leads to
confluence is the main result of this paper.

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. For lack of
space, three separate appendices will present how research towards determinism
for process algebras pass through those above cite papers, a collection of
more tricky examples, and the full proofs.

##  2 A Process Algebra with Clocks and Priorities

We call our clocked process algebra “SynPaTick” (denoted by
$\mathsf{CCS}^{\mathsf{spt}}$), whose syntax and operational semantics are
defined in the subsections below. In a nutshell, $\mathsf{CCS}^{\mathsf{spt}}$
is an extension of Milner’s CCS process algebra with priorities à la Phillips’
$\mathsf{CCS}^{\mathsf{Ph}}$ and broadcasted clock actions à la Hoare’s CSP
and as in timed algebras TPL [15] and CSA [8].

###  2.1 $\mathsf{CCS}^{\mathsf{spt}}$ Syntax

The terms in $\mathsf{CCS}^{\mathsf{spt}}$ form a set $\mathcal{P}$ of agents.
We use $P,Q,R,S\ldots$ to range over $\mathcal{P}$. Let $\mathcal{A}$ be a
countably infinite set of channel names with $a,b,c\ldots$ ranging over
$\mathcal{A}$. As in CCS, the set $\overline{\mathcal{A}}$ is a disjoint set
of co-names with elements denoted by
$\overline{a},\overline{b},\overline{c}\ldots$ that are in bijection with
$\mathcal{A}$; in other words, the overbar operator $\overline{\cdot}$
switches between $\mathcal{A}$ and $\overline{\mathcal{A}}$, i.e.,
$\overline{\overline{a}}=a$ for all $\overline{a}\in\mathcal{A}$. We will
refer to the names $a\in\mathcal{A}$ as input (or receiver) labels while the
co-names $\overline{a}\in\overline{\mathcal{A}}$ denote output (or sender)
labels. Let $\mathcal{C}$ be a countably infinite set of broadcasted clock
names, disjoint from both $\mathcal{A}$ and $\overline{\mathcal{A}}$ and let
$\sigma$ range over $\mathcal{C}$. Every clock acts as its own co-name,
$\overline{\sigma}=\sigma$ and so each $\sigma\in\mathcal{C}$ is also
considered as a clock label. Let $\mathcal{L}$ be the set of input, output and
clock labels defined as $\mathcal{A}\cup\overline{\mathcal{A}}\cup\mathcal{C}$
and let $\ell$ range over $\mathcal{L}$, and let $L,H$ range over subsets of
$\mathcal{L}$. We write $\overline{L}$ for the set
$\\{\overline{\ell}\mid\ell\in L\\}$. Let $\mathit{Act}$ be the set of all
actions defined as $\mathcal{L}\cup\\{\tau\\}$ by adjoining the silent action
$\tau\notin\mathcal{L}$ and let $\alpha$ range over $\mathit{Act}$. Viewed as
actions, the input and output labels
$\ell\in\mathcal{R}\stackrel{{{}_{\mathit{def}}}}{{=}}\mathcal{A}\cup\overline{\mathcal{A}}\subseteq\mathit{Act}$
are referred to as rendez-vous or channel actions to distinguish them from the
clock actions $\sigma\in\mathcal{C}\subseteq\mathit{Act}$ which also called
broadcast actions. Further, to distinguish the elements of
$\mathcal{R}\cup\mathcal{C}$ from $\tau$ as a subset of $\mathit{Act}$ we call
the former visible actions in contrast to $\tau$ that is the invisible action.
All symbols can appear indexed. The process terms $\mathcal{P}$ are defined by
the following abstract syntax:
$\begin{array}[]{lcll@{\qquad}l}P,Q,R,S&::=&{{\mathsf{0}}}&&\text{stop
(inaction)}\\\ &\mid&\alpha{:}H.P&&\text{action prefix with
}\alpha\in\mathcal{L}\text{ and }H\subseteq\mathcal{L}\\\
&\mid&P+Q&&\text{choice}\\\ &\mid&P\,|\,Q&&\text{parallel composition}\\\
&\mid&P\,\backslash\,L&&\text{restriction}\\\ &\mid&P\,/\,L&&\text{hiding}\\\
&\mid&A&&\text{process name }A\in\mathcal{I}\end{array}$
Intuitively, ${{\mathsf{0}}}$ denotes the inactive process which stops all
computations, including broadcasting synchronisation actions. The action
prefix $\alpha{:}H.P$ denotes a process that offers to engage in the action
$\alpha$ and then behave as $P$ while the blocking set $H\subseteq\mathcal{L}$
lists all actions taking precedence over $\alpha$. A prefix with
$\alpha\in\mathcal{R}$ denotes a CCS-style rendez-vous action. In case
$\alpha\in\mathcal{C}$, it denotes a CSP-style broadcast action that can
communicate with all the surrounding processes sharing on the same clock only
when the clock is universally consumed. The process $A\in\mathcal{I}$, where
$\mathcal{I}$ is a set of process identifiers, refers to a process whose
behaviour is specified indirectly by a definitional equation
$A\stackrel{{{}_{\mathit{def}}}}{{=}}P$. We assume that in every restriction
expression $P\,\backslash\,L$ the set $L\subseteq\mathcal{R}$ consists of
rendez-vous actions, and in every hiding expression $P\,/\,L$ we have
$L\subseteq\mathcal{C}$. These scoping operators act as name binders that
introduce local scopes.

The acute reader surely notices the absence of the relabelling operator
$P[f]$, useful in Milner’s CCS to define the well-known “standard concurrent
form” $(P_{1}[f_{1}]\,|\,\cdots\,|\,P_{2}[f_{n}])\,\backslash\,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{\mathsf{.}}P$ instead of $a{:}\\{\,\\}{\mathsf{.}}P$ and $a{:}H$
rather than $a{:}H{\mathsf{.}}{{\mathsf{0}}}$. Also, it is useful to drop
brackets for the blocking set if it is a singleton, writing
$a{:}b{\mathsf{.}}P$ instead of $a{:}\\{b\\}{\mathsf{.}}P$. With these
notational shortcuts we can naturally take each action $\alpha\in\mathcal{L}$
also as a prefix process $\alpha{:}\\{\,\\}{\mathsf{.}}{{\mathsf{0}}}$. In
this way, each action $\alpha$ is a process that offers to engage in $\alpha$,
without blocking, and then stops.

In our concrete notation for expressions using the abstract syntax of
processes, we will assume that the binary operator $+$ is right associative
and taking higher binding power than the binary operator $\,|\,$. Thus, we
write $P+Q+R\,|\,S$ instead of $(P+(Q+R))\,|\,S$. Also, we assume that the
unary operators of prefix, restriction and hiding have higher binding power
than the binary operators. Hence, we write
$P\,\backslash\,c+a{\mathsf{.}}b{\mathsf{.}}c{\mathsf{.}}Q\,|\,R\,/\,\sigma$
instead of
$((P\,\backslash\,c)+(a{\mathsf{.}}(b{\mathsf{.}}(c{\mathsf{.}}Q))))\,|\,(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{{{}_{\mathit{def}}}}{{=}}Q$ where $A$ is a sub-expression of $P$.
Sometimes it is useful to consider processes in a fragment of
$\mathsf{CCS}^{\mathsf{spt}}$. Specifically, a process is called unclocked if
$P$ does not contain any clock prefix $\sigma{:}H{\mathsf{.}}Q$ as a sub-
process. A process is called sequential or single-threaded if it does not
contain any parallel sub-process $Q\,|\,R$. $P$ is action-closed, or simply
closed, if if all sub-processes $\ell{:}H{\mathsf{.}}Q$ in $P$ occur in the
scope of a restriction or hiding operator that binds $\ell$. We write
$\textsf{vA}(P)$ for the set of free (“visible”) action names of $P$. We
identify syntactically two processes that differ only in the choice of bound
names, and we work under the Barendregt’s hygiene convention [1].

Following Milner’s CCS description in Chapter 3 of [22] and Milner’s
presentation of the $\pi$-calculus in [23], we define a structural congruence
over processes. The idea of the structural congruence is to split interaction
rules between agents from rules governing the “left-to-right” representation
of expressions. The idea of introducing an equivalence of processes via a set
of equations (congruence) is not new and it has many advantages: 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 reductions,
that, otherwise would be blocked (non reducible). Milner divides CCS equations
in static, dynamic and expressions laws: we will choose a modern approach
inspired by the pioneering work of Berry and Boudol [5].

######  Definition 2.1 (Structural Congruence $\equiv$).

Structural congruence, written $\equiv$, is the smallest congruence over
$\mathcal{P}$ that satisfies the equations in Fig. 1, where
$\star\in\\{\,|\,,+\\}$ and $\wr\in\\{\,\backslash\,,\,/\,\\}$:

$\begin{array}[]{l@{\qquad}rcl@{\quad}l}({\sf Const})&A&\equiv&P&\mbox{ if
}A\stackrel{{{}_{\mathit{def}}}}{{=}}P\\\\[2.84526pt] ({\sf Comm})&P\star
Q&\equiv&Q\star P\\\\[2.84526pt] ({\sf Assoc})&(P\star Q)\star
R&\equiv&P\star(Q\star R)\\\\[2.84526pt] ({\sf
Zero})&P\star{{\mathsf{0}}}&\equiv&P&\\\\[2.84526pt] ({\sf
Idem}_{+})&P+P&\equiv&P&\\\\[2.84526pt] ({\sf Scope}_{\wr})&P\wr L\wr
L^{\prime}&\equiv&P\wr(L\cup L^{\prime})\\\\[2.84526pt] ({\sf
Scope}_{{{\mathsf{0}}}})&{{\mathsf{0}}}\wr
L&\equiv&{{\mathsf{0}}}&\\\\[2.84526pt] ({\sf
Scope}_{\alpha})&(\alpha{:}H.P)\,\backslash\,L&\equiv&\left\\{\begin{array}[]{l}{{\mathsf{0}}}\\\
\alpha{:}H.(P\,\backslash\,L)\end{array}\right.&\begin{array}[]{l}\mbox{if
}\alpha\in L\cup\overline{L}\\\ \mbox{otherwise}\end{array}\\\\[2.84526pt]
({\sf Scope}_{\,\backslash\,})&(P\star
Q)\,\backslash\,L&\equiv&\left\\{\begin{array}[]{ll}P\star Q\,\backslash\,L\\\
P\,\backslash\,L+Q\,\backslash\,L\\\
P\,\backslash\,L\,|\,Q\,\backslash\,L\end{array}\right.&\begin{array}[]{l}\mbox{if
}\textsf{vA}(P)\cap(L\cup\overline{L})=\\{\,\\}\\\ \mbox{if }\star=+\\\
\mbox{if }\star=\,|\,\mbox{ and
}\textsf{vA}(P)\cap\overline{\textsf{vA}(Q)}\cap(L\cup\overline{L})=\\{\,\\}\end{array}\par\end{array}$

Figure 1: Structural Congruence.

Note that we have dropped from our structural rules all of Milner’s
$\tau$-laws, i.e. the ones related to the presence of invisible 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, Prop. 2, Prop. 4(2) and 4(5) of [22], respectively). This
is not surprising. It is known that timed process algebras and process
algebras with priorities enjoy extra expressiveness that invalidates some of
the familiar dynamic laws, see e.g., [12, 15, 8, 30, 27].
$\mathsf{CCS}^{\mathsf{spt}}$ shares features (clocks and priorities) with
timed and prioritised extensions of CCS. Hence, we must 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

$\begin{array}[]{l@{\hspace{2cm}}r}\lx@intercol\alpha{:}H{\mathsf{.}}P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P\qquad\hfill
P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}Q\lx@proof@logical@and
P^{\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R^{\prime}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}Q^{\prime}P\equiv
P^{\prime}Q\equiv Q^{\prime}R\equiv<EMAIL_ADDRESS>\lx@intercol P\,\backslash\,L\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R\,\backslash\,L}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H^{\prime}}}\,$}Q\,\backslash\,L\lx@proof@logical@and
P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}QL^{\prime}=L\cup\overline{L}\alpha\not\in
L^{\prime}H^{\prime}=H-L^{\prime}\qquad P\,/\,L\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R\,/\,L}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha\,/\,L}$}}\\!\\!{{}_{H^{\prime}}}\,$}Q\,/\,L\lx@proof@logical@and
P\mbox{
<EMAIL_ADDRESS>\lx@intercol P\,|\,Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R\,|\,Q}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}\,|\,Q\lx@proof@logical@and
P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}\alpha\not\in\mathcal{C}\qquad\hfill
P+Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}P\mbox{
<EMAIL_ADDRESS>\lx@intercol
P\,|\,Q\xrightarrow[R_{1}\,|\,R_{2}]{\ell\,|\,\overline{\ell}}\\!\\!{{}_{H_{1}\cup
H_{2}\cup H}}\,P^{\prime}\,|\,Q^{\prime}\lx@proof@logical@and P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\ell}$}}\\!\\!{{}_{H_{1}}}\,$}P^{\prime}Q\mbox{
<EMAIL_ADDRESS>\lx@intercol\textit{where }\hfill\begin{array}[]{l}\hskip
28.45274pt\alpha\,/\,L\stackrel{{{}_{\mathit{def}}}}{{=}}\left\\{\begin{array}[]{l@{\quad\
\ }l}\tau&\text{if }\alpha\in L\\\
\alpha&\text{otherwise}\end{array}\right.\quad\ell\,|\,\overline{\ell}\stackrel{{{}_{\mathit{def}}}}{{=}}\left\\{\begin{array}[]{ll}\tau&\text{if
}\ell\in\mathcal{R}\\\ \sigma&\text{if
}\ell=\sigma\end{array}\right.\\\\[11.38109pt]
race(P\,|\,Q)\stackrel{{{}_{\mathit{def}}}}{{=}}\left\\{\begin{array}[]{ll}\\{\tau\\}&\mbox{if
}H_{1}\cap\overline{\textsf{iA}}(Q)\not\subseteq\\{\ell\\}\text{ or
}H_{2}\cap\overline{\textsf{iA}}(P)\not\subseteq\\{\overline{\ell}\\}\\\
\\{\,\\}&\mbox{otherwise}\end{array}\right.\end{array}\hfil\lx@intercol\end{array}$

Figure 2: The $\mathsf{CCS}^{\mathsf{spt}}$ Plotkin’s Structural Operational
Semantics.

The operational semantics for $\mathsf{CCS}^{\mathsf{spt}}$ is given using a
labelled transition relation
$P\mathrel{\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}}Q$ in the style of
Plotkin’s Structured Operational Semantics (SOS) [29, 28], where
$\alpha\in\mathit{Act}$ is the action that labels the SOS transition. When
$\alpha\in\mathcal{L}$ the transition corresponds to a communication step,
namely a rendez-vous 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 will decorate the nondeterministic SOS with annotations
that provides sufficient information to express a uniform and confluent
reduction strategy based on scheduling precedences. We will call this new
reduction strategy (sequentially) constructive scheduling. Including these
annotations, our SOS judgment takes the form $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}Q$
where $P,Q,R\in\mathcal{P}$ are processes, $\alpha\in\mathit{Act}$ is an
action, and $H\subseteq\mathit{Act}$ a set of actions. We call the three
composite labels $\alpha$, $H$, and $R$ a c-action, written $\alpha{:}H[R]$.
The information provided by such a c-action is sufficient to define our
constructive reduction strategy for $\mathsf{CCS}^{\mathsf{spt}}$ that
satisfies a Church-Rosser property. We will use $P\xrightarrow{\alpha}Q$ as an
abbreviation to state that there is a transition for some $R$ and $H$.

The semantics is defined inductively as the smallest relation closed under
rules in Fig. 2. We call each transition derivable by Fig. 2 an admissible
transition. The intended meaning of our annotated semantics for admissible
transitions is as follows: $\alpha$ is the usual action “passed back” in the
SOS, $H$ (also called blocking set) is the set of actions that block the
transition, and $R$ (also called concurrent context) is a process that
represents the behaviour of all threads in $P$ that execute concurrently with
the transition: note that actions in $R$ are potentially in competition with
$\alpha$. The set $H$ represents the resources that are consumed by the action
and of $R$ as the concurrent context that potentially competes for $H$. In a
parallel composition $P\,|\,Q$ of $P$ with another process $Q$, the context
$R$ of 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. 2.4).

In 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 $(\textit{Act})$ is the axiom annotating in the transition the action and
the (empty) environment. Rules $(\textit{Restr})$ and $(\textit{Hide}$) deal
with “local restriction” of rendez-vous actions and “local hiding” of
broadcasted clocks. Rules $(\textit{Par}_{1,2})$ and $(\textit{Sum}_{1,2})$
are almost standard and deal with parallelism and sum. Rule
$(\textit{Struct})$ internalises in the transition the above presented
structural equivalence of processes. Rule $(\textit{Par}_{3})$ is
compositional as one can expect for both rendez-vous and broadcast, and it
have the extra $race$ condition enriching the blocking set of the conclusion
in case $P$ can interfere with $Q$ and vice-versa. Note that if we ignore the
scheduling labels, then the operational semantics of unclocked processes
coincides precisely with the operational semantics of CCS. The rules for clock
actions coincide with the semantics of CSP broadcast actions.

###  2.3 Constructive Scheduling

The scheduling mechanism of $\mathsf{CCS}^{\mathsf{spt}}$ provides a new form
of constructive evaluation that satisfies a confluence property for a large
class of processes, the so-called coherent processes. To connect our approach
with that of $\mathsf{CCS}^{\mathsf{Ph}}$ and $\mathsf{CCS}^{\mathsf{CW}}$ we
first consider the following definition of a weaker form of scheduling based
on the strong initial actions of a process.

######  Definition 2.2 (Strong Initial Actions).

The set $\textsf{iA}(P)\subseteq\mathit{Act}$ of _strong initial_ actions of a
process $P$ is the smallest set closed under the inductive rules in Fig. 3.

$\begin{array}[]{rcl}\textsf{iA}({{\mathsf{0}}})&\stackrel{{{}_{\mathit{def}}}}{{=}}&\\{\,\\}\\\
\textsf{iA}(\alpha{:}H{\mathsf{.}}P)&\stackrel{{{}_{\mathit{def}}}}{{=}}&\\{\alpha\\}\\\
\textsf{iA}(P+Q)&\stackrel{{{}_{\mathit{def}}}}{{=}}&\textsf{iA}(P)\cup\textsf{iA}(Q)\\\
\textsf{iA}(P\,|\,Q)&\stackrel{{{}_{\mathit{def}}}}{{=}}&(\textsf{iA}(P)\cup\textsf{iA}(Q))-\mathcal{C}\cup\\{(\ell\,|\,\overline{\ell})\mid\ell\in\textsf{iA}(P)\cap\overline{\textsf{iA}(Q)}\\}\\\
\textsf{iA}(P\,\backslash\,L)&\stackrel{{{}_{\mathit{def}}}}{{=}}&\textsf{iA}(P)-(L\cup\overline{L})\\\
\textsf{iA}(P\,/\,L)&\stackrel{{{}_{\mathit{def}}}}{{=}}&\textsf{iA}(P)-L\cup\\{\tau\mid
L\cap\textsf{iA}(P)\neq\\{\,\\}\\}\\\
\textsf{iA}(A)&\stackrel{{{}_{\mathit{def}}}}{{=}}&\textsf{iA}(P)\qquad\text{
where $A\stackrel{{{}_{\mathit{def}}}}{{=}}P$}\end{array}$

Figure 3: Strong Initial Actions.

The traditional approach in prioritised process algebras [7, 30, 27] is to
block the transitions of a process $P$ by its strong initial actions
$\textsf{iA}(P)$ as captured by the following Def. 2.3.

######  Definition 2.3 (Weakly Enabled Transitions).

An admissible transition $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}Q$
is called _weakly enabled_ if
$H\cap(\overline{\textsf{iA}}(R)\cup\\{\tau\\})=\\{\,\\}$.

Let us call a process $P$ free if the blocking sets of all action prefixes
$\alpha{:}H{\mathsf{.}}Q$ occurring as sub-processes of $P$ have an empty
blocking set, i.e. $H=\\{\,\\}$. The presence of blocking information makes
weakly enabled transitions become a proper subset of admissible transitions.
For general non-free processes, weak enabling prunes certain transitions and
thus implements a priority-based scheduling regime. In order to implement our
stronger precedence-based scheduling we need to look at the weak initial
actions for a process.

######  Definition 2.4 (Weak Initial Actions & Strong Enabling).

The set $\textsf{iA}^{\tau}(P)$ of _weak initial_ transitions is the smallest
extension $\textsf{iA}(P)\subseteq\textsf{iA}^{\tau}(P)$ such that if
$\alpha\in\textsf{iA}^{\tau}(Q)$ and $P\xrightarrow{\tau}Q$ then
$\alpha\in\textsf{iA}^{\tau}(P)$. Let
$\overline{\textsf{iA}}^{{}_{\tau}}(P)=\overline{\textsf{iA}^{\tau}(P)}$. A
transition $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
is called _strongly enabled_ if
$H\cap(\overline{\textsf{iA}}^{{}_{\tau}}(R)\cup\\{\tau\\})=\\{\,\\}$.

By looking at the definition, it is easy to see that
$\textsf{iA}(P)\subseteq\textsf{iA}^{\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\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
is enabled, then we know that $H\cap\overline{\textsf{iA}}(R)=\\{\,\\}$ or
$H\cap\overline{\textsf{iA}}^{{}_{\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{\textsf{iA}}(R\,|\,Q)\neq\\{\,\\}$ or
$H\cap\overline{\textsf{iA}}^{{}_{\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\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H}}\,$}P^{\prime}\,|\,Q.$

We are interested in exploiting priority-based scheduling to achieve
determinacy of reduction. According to Milner [22], the notion of determinacy
is tied up with predictability: “if we perform the same experiment twice on a
determinate system, starting each time in its initial state, then we expect to
get the same result, or behaviour, each time.” The strongest form of
determinacy is the notion of structural determinism.

######  Definition 2.5.

A process $P$ is _structurally deterministic_ for an action
$\alpha\in\mathit{Act}$, if for every derivative $Q$ of $P$, if $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{}\,$}Q_{1}$
and $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{}\,$}Q_{2}$
we have $Q_{1}\equiv Q_{2}$.

Structural determinism disallows processes such as
$a{\mathsf{.}}A+a{\mathsf{.}}B$ for $A\not\equiv B$ or parallel compositions
such as $a{\mathsf{.}}A\,|\,a{\mathsf{.}}B$ where an action $a$ is used in
more than one prefix of a single thread or of concurrent threads. The former
violates predictability as it introduces externally uncontrollable non-
determinism. We don’t exclude the latter, as it would prevent multi-receiver
and multi-sender applications. For silent actions, structural determinism is
too strong. We are not interested in the uniqueness of the immediate
$\tau$-redexes of a process but the uniqueness of the final normal form. As
such, the notion of confluence is more useful.

######  Definition 2.6 (Structural Confluence).

A process $P$ is _structurally confluent_ if for every derivative $Q$ of $P$
and reductions $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}Q_{1}$
and $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}Q_{2}$
with $Q_{1}\not\equiv Q_{2}$, there exist $Q^{\prime}$ such that $Q_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}Q^{\prime}$
and $Q_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}Q^{\prime}$.

A process $P$ is in normal form if has no admissible $\tau$-transition. Then
all normal forms of a structurally confluent process must be structurally
equivalent. The main result of the paper (Thm. 4.5 together with Propositions
D.6–D.23) is to identify a large class of processes, called policy-coherent
processes, which are structurally confluent under c-enabled reductions. The
notion of policy-coherence is a refinement of Milner’s notion of confluence
([22] Chap. 11). The reduction strategy of c-enabledness implements a form of
constructive scheduling that refines strong enabling (Def. 2.4) discussed
above. It turns out that each policy-coherent process, under constructive
scheduling, is clock-deterministic (Prop. 4.7) and satisfies maximal progress
(Prop. 4.12). No matter in which order we execute c-enabled reductions, when
the normal form is reached, and only then, a clock can tick. Since the normal
form is uniquely determined by confluence, the next state reached by each
clock tick is uniquely determined. Thus, each policy-coherent process
represents a “synchronous stream”. As such, our work extends the classical
non-deterministic theory of timed (multi-clocked) process algebras [12, 15, 8]
for applications in deterministic synchronous programming. Before we expound
on the scheduling theory of $\mathsf{CCS}^{\mathsf{spt}}$ in Sec. 4, let us
discuss some examples.

##  3 Examples

We begin with some simple examples to illustrate the operation of our
scheduling semantics. The focus is on how the transitions labels, blocking
sets and action environment, implement precedences.

######  Example 3.1 (Read Before Write).

Let us see how the rendez-vous synchronisation is scheduled by the precedences
that come with a prioritised choice. Consider a “store” process
$S\stackrel{{{}_{\mathit{def}}}}{{=}}w+r{:}w$ that offers a write action $w$
and a read action $r$ but prefers the write over the read. If we put $S$ in
parallel with a reader $R\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{r}$ we
can let read actions $r$ and $\overline{r}$ synchronise in a reduction
$S\,|\,R\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}{{\mathsf{0}}}.$
The fact that $w$ takes priority over $r$ is recorded in the blocking set
$\\{w\\}$ which contains the action $w$. This will block $R$’s transition when
a parallel writer $W\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{w}$ is added.
Specifically, the reduction $w+r{:}w\,|\,\overline{r}\,|\,\overline{w}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\overline{w}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}\overline{w}$
is not weakly enabled, because
$\\{w\\}\cap\overline{\textsf{iA}}(\overline{w})=\\{w\\}\cap\\{w\\}\neq\\{\,\\}$.
The only enabled reduction of process $S\,|\,R\,|\,W$ is to let $S$ and $W$
synchronise to produce the transition
$w+r{:}w\,|\,\overline{r}\,|\,\overline{w}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\overline{r}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}\overline{r}$
which is even strongly enabled, since
$\\{w\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(\overline{r})=\\{\,\\}$.

######  Example 3.2 (Two Thread Process).

The two-thread process $a{:}b+\overline{b}\,|\,\overline{a}+b{:}a$ has two
admissible transitions under $(\textit{Par}_{3})$ for $\tau.{{\mathsf{0}}}$
through $a{:}b\,|\,\overline{a}$ or $\overline{b}\,|\,b{:}a$. However, since
$b\in\overline{\textsf{iA}}(a{:}b+\overline{b})$ and
$a\in\overline{\textsf{iA}}(\overline{a}+b{:}a)$ both the actions $a{:}b$ and
$b{:}a$ are blocked.

A more subtle form of blocking occurs for strong enabling. Two parallel
processes can create a circular dependency through the priorities of their
initial actions, e.g., when accessing a third process that is acting as a
resource. The following example simulates two processes that wait for each
other to write to different memory cells, before they can write to the memory
cell on which the other process is waiting.

######  Example 3.3 (Deadlock).

Consider the process
$S\stackrel{{{}_{\mathit{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{{{}_{\mathit{def}}}}{{=}}\overline{r_{0}}{\mathsf{.}}\overline{w_{1}}$
and
$P_{1}\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{r_{1}}{\mathsf{.}}\overline{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}\,|\,\overline{w_{0}}\xleftarrow[\raisebox{-1.99997pt}[0.0pt][0.0pt]{${}^{P_{0}\,|\,(w_{0}+r_{0}{:}w_{0})}$}]{\tau}\\!\\!{{}_{\\{w_{1}\\}}}\,P_{0}\,|\,S\,|\,P_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{w_{1}+r_{1}{:}w_{1}\,|\,P_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w_{0}\\}}}\,$}\overline{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}\mathrel{\stackrel{{\scriptstyle\tau}}{{\rightarrow}}}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. Abserve that none of the two
reductions displayed above is actually strongly enabled. For the right
reduction we find that its concurrent environment
$R_{0}\stackrel{{{}_{\mathit{def}}}}{{=}}w_{1}+r_{1}{:}w_{1}\,|\,P_{1}$ has a
reduction sequence
$R_{0}\mathrel{\stackrel{{\scriptstyle\tau}}{{\rightarrow}}}\overline{w_{0}}$
and thus
$\\{w_{0}\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(R_{0})\subseteq\\{w_{0}\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(\overline{w_{0}})=\\{w_{0}\\}\cap\\{w_{0}\\}\neq\\{\,\\}.$
Symmetrically, for the concurrent environment
$R_{1}\stackrel{{{}_{\mathit{def}}}}{{=}}P_{0}\,|\,w_{0}+r_{0}{:}w_{0}$ of the
left reduction we have
$R_{1}\mathrel{\stackrel{{\scriptstyle\tau}}{{\rightarrow}}}\overline{w_{1}}$
and hence
$\\{w_{1}\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(R_{1})\neq\\{\,\\}$.

The deadlocking processes of Ex. 3.3 have the special property that priorities
only exist between receiver actions, while sender actions never appear in any
choice contexts. These are the processes covered by
$\mathsf{CCS}^{\mathsf{CW}}$ [7] which restricts prioritised choice to
receiver actions in the same way as the programming language Occam [2] with
its “PRIALT” construct does.

######  Example 3.4 (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

$\displaystyle\mathsf{wAND}_{0}$
$\displaystyle\stackrel{{{}_{\mathit{def}}}}{{=}}$ $\displaystyle
w_{1}{\mathsf{.}}\mathsf{wAND}_{1}+w_{0}{:}w_{1}{\mathsf{.}}\mathsf{wAND}_{0}+r_{0}{:}\\{w_{0},w_{1}\\}{\mathsf{.}}\mathsf{wAND}_{0}$
$\displaystyle\mathsf{wAND}_{1}$
$\displaystyle\stackrel{{{}_{\mathit{def}}}}{{=}}$ $\displaystyle
w_{1}{\mathsf{.}}\mathsf{wAND}_{1}+w_{0}{:}w_{1}{\mathsf{.}}\mathsf{wAND}_{0}+r_{1}{:}\\{w_{0},w_{1}\\}{\mathsf{.}}\mathsf{wAND}_{1}$

The process $\mathsf{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
$\mathsf{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}\\}$.

Between the write actions, the blocking sets implement a precedence of $w_{1}$
over $w_{0}$. Notice that the blocking sets are visualised as dashed arrows.

######  Example 3.5 (Esterel Signals).

Concurrent Esterel threads communicate via signals [4, 32]. 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 that
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 that does not stabilise is called
non-constructive and rejected by the compiler. A pure, temporary signal is
modelled by the following recursive behaviour:

$\displaystyle S_{0}$ $\displaystyle\stackrel{{{}_{\mathit{def}}}}{{=}}$
$\displaystyle\mathit{abs}{:}\mathit{emit}{\mathsf{.}}S_{0}+\mathit{emit}{\mathsf{.}}S_{1}+\sigma{:}\\{\mathit{abs},\mathit{emit}\\}{\mathsf{.}}S_{0}$
$\displaystyle S_{1}$ $\displaystyle\stackrel{{{}_{\mathit{def}}}}{{=}}$
$\displaystyle\mathit{pres}{\mathsf{.}}S_{1}+\mathit{emit}{\mathsf{.}}S_{1}+\sigma{:}\\{\mathit{pres},\mathit{emit}\\}{\mathsf{.}}S_{0}$

which is depicted on side and structurally coherent according to Def. 4.4.

######  Example 3.6 ($\mathsf{ABRO}$).

The hallo word in synchronous languages, see [4], $\mathsf{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. [32]
The behaviour of $\mathsf{ABRO}$ is expressed as a Mealy machine and as a
SyncCharts, as displayed 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. In $\mathsf{CCS}^{\mathsf{spt}}$ we
represent the micro-steps as sequences of $\tau$-transitions, i.e., local and
asynchronous rendez-vous synchronisations, whereas the macro-step is captured
as a global clock synchronisation. Unfortunately, the Mealy machine formalism
is not scalable because of 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, as displayed on the

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

right. The loop loop P each R 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 $\mathsf{CCS}^{\mathsf{spt}}$.
As such, we may present in the figure the following coding of the
$\mathsf{ABRO}$ process in $\mathsf{CCS}^{\mathsf{spt}}$.

$\begin{array}[]{rcl}\mathsf{ABRO}&\stackrel{{{}_{\mathit{def}}}}{{=}}&\sigma{\mathsf{.}}(\mathsf{R}\,|\,\mathsf{ABO})\\\
\mathsf{ABO}&\stackrel{{{}_{\mathit{def}}}}{{=}}&(\mathsf{A}\,|\,\mathsf{B}\,|\,\mathsf{T}\,|\,\mathsf{O})\,\backslash\,\\{s,t\\}\\\
\mathsf{R}&\stackrel{{{}_{\mathit{def}}}}{{=}}&r{:}r{\mathsf{.}}\overline{k}_{1}{:}\overline{k}_{1}{\mathsf{.}}\overline{k}_{2}{:}\overline{k}_{2}{\mathsf{.}}\overline{k}_{4}{:}\overline{k}_{4}{\mathsf{.}}\overline{k}_{5}{:}\overline{k}_{5}{\mathsf{.}}\mathsf{ABRO}+\tau{:}{r}{\mathsf{.}}\sigma{\mathsf{.}}\mathsf{R}\\\
\mathsf{A}&\stackrel{{{}_{\mathit{def}}}}{{=}}&k_{1}{:}k_{1}{\mathsf{.}}{{\mathsf{1}}}+a{:}\\{k_{1},a\\}{\mathsf{.}}\overline{s}{:}\overline{s}{\mathsf{.}}{{\mathsf{1}}}+\sigma{:}\\{k_{1},a\\}{\mathsf{.}}\mathsf{A}\\\
\mathsf{B}&\stackrel{{{}_{\mathit{def}}}}{{=}}&k_{2}{:}k_{2}{\mathsf{.}}{{\mathsf{1}}}+b{:}\\{k_{2},b\\}{\mathsf{.}}\overline{s}{:}\overline{s}{\mathsf{.}}{{\mathsf{1}}}+\sigma{:}\\{k_{2},b\\}{\mathsf{.}}\mathsf{B}\\\
\mathsf{T}&\stackrel{{{}_{\mathit{def}}}}{{=}}&k_{4}{:}k_{4}{\mathsf{.}}{{\mathsf{1}}}+s{:}\\{k_{4}\\}{\mathsf{.}}\mathsf{T}+\overline{t}{:}\\{k_{4},\overline{t},s\\}{\mathsf{.}}{{\mathsf{1}}}+\sigma{:}\\{k_{4},\overline{t},s\\}{\mathsf{.}}\mathsf{T}\\\
\mathsf{O}&\stackrel{{{}_{\mathit{def}}}}{{=}}&k_{5}{:}k_{5}{\mathsf{.}}{{\mathsf{1}}}+t{:}\\{k_{5},t\\}{\mathsf{.}}\overline{o}{:}\overline{o}{\mathsf{.}}{{\mathsf{1}}}+\sigma{:}\\{k_{5},t\\}{\mathsf{.}}\mathsf{O}.\end{array}$

Figure 4: $\mathsf{ABRO}$.

The $\mathsf{CCS}^{\mathsf{spt}}$ code follows the structure of the Esterel
code. $\mathsf{ABRO}$ is obtained as a parallel composition
$\mathsf{R}\,|\,\mathsf{ABO}$ combining a watchdog $\mathsf{R}$ with the
behaviour $\mathsf{ABO}$. The $\mathsf{R}$ is responsible to implement the
reset loop at the superstate called $\mathsf{ABO}$, as in the state charts.
The $\mathsf{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 $\mathsf{A}\,|\,\mathsf{B}$ making up the
behaviour of the region called $\mathsf{AB}$ with code `await A || await B`.
The processes $\mathsf{T}\,|\,\mathsf{O}$ implement the synchronisation that
waits for termination of $\mathsf{AB}$ to start the output process
$\mathsf{O}$. We assume that the channels $a$, $b$, $r$, $o$ modelling
interface signals `A`, `B`, `R`, `O` all have a unique sender and receiver
(full-multicast in App. B.B.14). This is seen in our coding from the fact that
the prefixes for these channels are self-blocking.

##  4 Constructive Scheduling for $\mathsf{CCS}^{\mathsf{spt}}$

This section presents the core elements of our scheduling theory for
$\mathsf{CCS}^{\mathsf{spt}}$ based on the notions of constructive enabling,
coherence, policies, and policy-coherent processes. As indicated by the
examples of Sec. 3, strong enabling generates confluent reductions in cases
where rendez-vous actions have a unique sender and a unique receiver process.
For multi-cast communication we need an even stronger notion of enabledness,
called constructive enabling.

######  Definition 4.1 (Constructive Enabling).

The set $\textsf{iA}^{\ast}(P)\subseteq\mathcal{L}$ of _potential actions_ is
the smallest extension
$\textsf{iA}(P)\cap\mathcal{L}\subseteq\textsf{iA}^{\ast}(P)$ such that if
$\ell\in\textsf{iA}^{\ast}(Q)$ and $P\xrightarrow{\alpha}Q$ for
$\alpha\in\mathcal{R}\cup\\{\tau\\}$, then $\ell\in\textsf{iA}^{\ast}(P)$. A
transition $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}Q$
is called _constructively enabled_ , or _c-enabled_ for short, if
$H\cap(\overline{\textsf{iA}}^{{}_{\ast}}(R)\cup\\{\tau\\})=\\{\,\\}$.

Def. 4.1 models the deterministic semantics of synchronous programming
languages like Esterel [3] which permit local multicast synchronisation.
Associated with it is the notion of Coherence (Def. 4.4) which is inspired by
Milner’s confluence in CCS. The latter is preserved by prefixing, parallel
composition and restriction only subject to serious restrictions identified in
[22]. The former satisfies stronger closure properties and covers a larger
class of processes.

######  Definition 4.2.

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\\}$:

If $\alpha_{1}\neq\alpha_{2}$ then $\alpha_{i}\not\in H_{3-i}$.

If $\alpha_{3-i}=\tau$ then
$H_{i}\cap(\overline{\textsf{iA}}^{{}_{\ast}}(E_{i})\cup\\{\tau\\})=\\{\,\\}$.

Def. 4.2(1) says that distinct interference-free c-actions must not block each
other. This ensures that they are not part of a conflicting choice in which
each preempts the other. By Def. 4.2(2), non-interference with a silent action
requires that the action does not get blocked by computations in its own
reduction context.

######  Proposition 4.3.

Suppose $\alpha_{1}{:}H_{1}[E_{1}\,|\,R]$ and
$\alpha_{2}{:}H_{2}[E_{2}\,|\,R]$ are interference-free. Then,
$\alpha_{1}{:}H_{1}^{\prime}[E_{1}]$ and $\alpha_{2}{:}H_{2}^{\prime}[E_{2}]$
are interference-free for arbitrary subsets $H_{1}^{\prime}\subseteq H_{1}$
and $H_{2}^{\prime}\subseteq H_{2}$.

Coherence is formulated using an auxiliary form of transition
$P\mathrel{\stackrel{{\scriptstyle\alpha}}{{\rightsquigarrow}}}Q$ which
abbreviates a form of residual transition with the following two cases: $(i)$
If $\alpha\in\mathcal{L}$ then $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{}\,$}Q$
or $P\equiv Q$ and $(ii)$ if $\alpha=\tau$ then $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}Q$,
$P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\ell}$}}\\!\\!{}\,$}Q$,
or $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{\ell}}$}}\\!\\!{}\,$}Q$
for some $\ell\in\mathcal{R}$. This says that there is a transition from $P$
to $Q$ with an action that is a “factor” of $\alpha$.

######  Definition 4.4 (Coherence).

A process $P$ is _(structurally) coherent_ if for all its derivatives $Q$ the
following holds, where $\alpha_{1},\alpha_{2}\in\mathit{Act}$: Given two
transitions $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}}}\,$}Q_{1}\text{
and }Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}}}\,$}Q_{2}$
such that $\alpha_{1}\neq\alpha_{2}$ or $Q_{1}\not\equiv Q_{2}$ or
$\\{\alpha_{1},\alpha_{2}\\}\subseteq\mathcal{R}$ and $\alpha_{i}\not\in
H_{3-i}$. Further, suppose the c-actions $\alpha_{i}{:}H_{i}[E_{i}]$ are
interference-free. Then, there exist $H_{i}^{\prime}$ and processes
$E_{i}^{\prime}$, $Q^{\prime}$ such that $Q_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E_{2}^{\prime}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}^{\prime}}}\,$}Q^{\prime}\text{
and }Q_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E_{1}^{\prime}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}^{\prime}}}\,$}Q^{\prime}$
with $H_{i}^{\prime}\subseteq H_{i}$ and
$E_{1}\mathrel{\stackrel{{\scriptstyle\alpha_{2}}}{{\rightsquigarrow}}}E_{1}^{\prime}$
and
$E_{2}\mathrel{\stackrel{{\scriptstyle\alpha_{1}}}{{\rightsquigarrow}}}E_{2}^{\prime}$.
In particular, $E_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{}\,$}E_{1}^{\prime}\text{
and }E_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{}\,$}E_{2}^{\prime}$
if $\\{\alpha_{1},\alpha_{2}\\}\subseteq\mathcal{R}$ and
$\alpha_{1}\neq\alpha_{2}$ or $Q_{1}\not\equiv Q_{2}$, or
$\\{\alpha_{1},\alpha_{2}\\}\cap\mathcal{C}\neq\\{\,\\}$.

######  Theorem 4.5 (Coherence implies confluence).

Every coherent process is structurally confluent for 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.

######  Proposition 4.6.

If a coherent process $P$ offers enabled transitions on a clock $\sigma$ and
another distinct action $\alpha\neq\sigma$ with $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}\text{
and }P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\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}$.

Coherent processes are structurally deterministic for clock transitions. They
do not offer a choice on the same visible label to structurally different
successor states unless these actions also occur in concurrent threads.

######  Proposition 4.7 (Action Determinism).

Let $P$ be coherent with $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\ell}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}$
such that $\ell\in\mathcal{L}$ and $\ell\not\in\textsf{iA}(R_{1})$. Then, for
every transition $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\ell}$}}\\!\\!{{}_{H_{2}}}\,$}P_{2}$
we have $P_{1}\equiv P_{2}$. In particular, $P$ is structurally clock
deterministic, i.e., if $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\sigma}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}\text{
and }P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\sigma}$}}\\!\\!{{}_{H_{2}}}\,$}P_{2}$
then $P_{1}\equiv P_{2}$.

The problem of causality cycles that occurs in the parallel composition of two
single-threaded processes stems from the symmetry between input and output
actions. The standard trick to eliminate the problem as used e.g., in Occam,
is to introduce a causality order so that outputs (sender actions) are
deterministic by construction. All remaining choices are choices between
inputs and these are resolved by the environment selecting the matching
output. To express such causality properties of processes by static interfaces
we refine the notion of a sort known from CCS for
$\mathsf{CCS}^{\mathsf{spt}}$.

######  Definition 4.8 (Policy).

A _precedence policy_ is a pair $\pi=(L,\raisebox{-1.0pt}{$\dotarrow{}$})$
where $L\subseteq\mathcal{L}$ is a subset of visible actions, called the
_alphabet_ of $\pi$ and $\raisebox{-1.0pt}{$\dotarrow{}$}\subseteq L\times L$
a binary relation on $L$, called the _precedence relation_. If
$(\ell_{1},\ell_{2})\in\raisebox{-1.0pt}{$\dotarrow{}$}$ we write
$\pi\Vdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$, or simply
$\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ when $\pi$ is understood.
When $\ell\in L$ we say that $\ell$ is _admissible_ under $\pi$ and simply
write $\ell\in\pi$. If $\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ we
say that $\ell_{1}$ takes _precedence_ over $\ell_{2}$ under $\pi$. If
$\ell_{1},\ell_{2}\in L$ and
$\pi\nVdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ as well as
$\pi\nVdash\ell_{2}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{1}$ we say that
$\ell_{1}$ and $\ell_{2}$ are _concurrently independent_ under $\pi$, written
$\pi\Vdash\ell_{1}\mathrel{\diamond}{}\ell_{2}$ or simply
$\ell_{1}\mathrel{\diamond}{}\ell_{2}$ when $\pi$ is understood.

We obtain a partial ordering $\pi_{1}\preceq\pi_{2}$ on precedence policies by
subset inclusion. Specifically, we have
$(L_{1},\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{1}$})\preceq(L_{2},\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{2}$})$
if $L_{1}\subseteq L_{2}$ such that for all $\ell_{1},\ell_{2}\in L_{1}$, if
$\ell_{1}\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{2}$}\ell_{2}$ then
$\ell_{1}\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{1}$}\ell_{2}$. Intuitively, if
$\pi_{1}\preceq\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}$. There is also the normal
inclusion ordering $\pi_{1}\subseteq\pi_{2}$ between policies defined by
$L_{1}\subseteq L_{2}$ and
$\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{1}$}\subseteq\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{2}$}$.
It differs from $\preceq$ in the inclusion direction of the precedence
alphabets. Another notation we need is restriction. For any policy
$\pi=(L,\raisebox{-1.0pt}{$\dotarrow{}$})$ and set of labels
$K\subseteq\mathcal{L}$ we denote by $\pi\,\backslash\,K$ the policy $\pi$
restricted to the alphabet $L-(K\cup\overline{K})$ in the obvious way.

For any policy $\pi$ on alphabet $L$ we define its dual as a policy
$\overline{\pi}$ on the set of labels $\overline{L}$ where for all
$\overline{\ell}_{1},\overline{\ell}_{2}\in\overline{L}$ we stipulate
$\overline{\pi}\Vdash\overline{\ell}_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\overline{\ell}_{2}$
iff $\ell_{1}=\ell_{2}$ or $\pi\Vdash\ell_{1}\mathrel{\diamond}{}\ell_{2}$,
i.e., both $\pi\nVdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ and
$\pi\nVdash\ell_{2}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{1}$. Intuitively, the
dual policy $\overline{\pi}$ consists of matching copies $\overline{\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” $\overline{\pi}$
from $\pi$, which is reflexive and symmetric. Note that
$\overline{\overline{\pi}}$ need not be identical to $\pi$ but contains more
precedences. In general, we have $\overline{\overline{\pi}}\preceq\pi$ and
$\overline{\overline{\pi}}=\pi$ if $\pi$ is symmetric. The policy
$\overline{\pi}$ captures the independences between actions of $\pi$ and is
called the associated independence alphabet, in the sense of trace theory [9].
Analogously, $\overline{\overline{\pi}}$ expresses the dependencies of actions
in $\pi$, called the associated dependence alphabet.

We are going to use policies to measure the degree of concurrency exhibited by
a process. The alphabet of the $\preceq$-maximal policy $\pi_{max}$ contains
all labels $\mathcal{L}$ and its precedence relation $\dotarrow\\!\\!{}_{max}$
is empty. It is the largest policy in the $\preceq$ ordering. Its dual
$\overline{\pi}_{max}$ contains all labels and precedences between all of
them, i.e.,
$\overline{\pi}_{max}\nVdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$
for all $\ell_{1},\ell_{2}\in\mathcal{L}$. The $\preceq$-minimal policy
$\pi_{min}$ has empty alphabet and empty precedences. It is self-dual, i.e.,
$\overline{\pi}_{min}=\pi_{min}$. The following definition explains how
policies can statically specify the externally observable scheduling behaviour
of a process. The maximal policy $\pi_{max}$ is least restrictive in the sense
that it permits a process to offer arbitrary actions with arbitrary blocking.
The minimal policy $\pi_{min}$ is most restrictive in that it does not permit
any externally visible actions.

######  Definition 4.9 (Conformance).

$P$ _conforms_ to a policy $\pi$ if for each of its derivatives $Q$: If
$Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\ell}$}}\\!\\!{{}_{H}}\,$}Q^{\prime}$
with $\ell\in\mathcal{L}$, then $\ell\in\pi$ and for all
$\ell^{\prime}\in\mathcal{L}$, if $\ell^{\prime}\in H$ then
$\pi\Vdash\ell^{\prime}\raisebox{-1.0pt}{$\dotarrow{}$}\ell$.

If $P$ conforms to $\pi$ then the admissible actions of $\pi$ corresponds to
“sorts” of $P$ in CCS. It gives an upper bound on the labels that can be used
by the process. The precedence relation $\dotarrow{}$ is specific to
$\mathsf{CCS}^{\mathsf{spt}}$. It provides for a static over-approximation of
the blocking between visible actions, i.e., which labels can be in a choice
conflict with each other. Specifically, if
$\pi\Vdash\ell_{1}\mathrel{\diamond}{}\ell_{2}$ then all transitions with
labels $\ell_{1}$ and $\ell_{2}$ must be from concurrent threads and thus
cannot block each other. If
$\pi\Vdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ and
$\ell_{1}\neq\ell_{2}$ are distinct, then $P$ may take $\ell_{1}$ and
$\ell_{2}$ transitions to completely different states from the same thread.
Necessarily, these must be transitions combined in a prioritised sum, where
one of $\ell_{i}$ blocks the other $\ell_{3-i}$. A special case occurs if
$\ell_{1}=\ell_{2}$. Then, the presence of
$\pi\Vdash\ell\raisebox{-1.0pt}{$\dotarrow{}$}\ell$ permits $P$ and its
derivatives $Q$ to execute $\ell$ without any guarantee that $\ell$ can
synchronise with arbitrarily many concurrent partners. In contrast, if the
policy specifies $\pi\Vdash\ell\mathrel{\diamond}{}\ell$, then a conformant
$P$ can execute $\ell$ only in concurrent threads and each $\ell$-transition
is arbitrarily repeatable.

Here we are interested in a restricted class of processes that conform to
policies with special properties. We write $P:\pi$ to express that $P$ is
coherent and conforms to policy $\pi$.

######  Definition 4.10 (Pivotable, Precedence-closed, Input-scheduled
Processes).

  * •

A policy $\pi$ is a _pivot_ policy if $\overline{\pi}\preceq\pi$.

  * •

A policy $\pi$ is _input-scheduled_ if $\pi\subseteq\pi_{is}$ where
$\pi_{is}=(L_{is},\raisebox{-1.0pt}{$\dotarrow\\!\\!{}_{is}$})$ given by
$L_{is}=\mathcal{L}$ and
$\pi_{is}\Vdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ iff
$\ell_{1}=\ell_{2}$ or $\ell_{1},\ell_{2}\in\mathcal{A}\cup\mathcal{C}$.

  * •

A policy $\pi$ is _precedence-closed_ for $L\subseteq\mathcal{L}$ if
$\ell_{1}\in L$ and
$\pi\Vdash\ell_{1}\raisebox{-1.0pt}{$\dotarrow{}$}\ell_{2}$ implies
$\ell_{2}\in L$.

A process is _pivotable_ /_input-scheduled_ /_precedence-closed_ if $P:\pi$
where $\pi$ is a pivot policy/input-scheduled/precedence-closed.

In a pivotable process, the choice between any two synchronisations is
resolved by the precedences in third independent thread, acting as the
“pivot”. For instance, the process
$P\stackrel{{{}_{\mathit{def}}}}{{=}}a+\overline{b}{:}a\,|\,b+\overline{a}{:}b$
is not pivotable (see also Ex. 3.2 in App. B). It consists of two threads,
each able to synchronise on $a$ and also $b$. Which one is chosen, must be
resolved between the two threads. This is not possible, because the first
wants channel $a$ to take priority over $\overline{b}$ and the second the
other way around. This is reflected in any associated policy $\pi$ for which
$P$ is conformant, which must satisfy $\pi\Vdash
a\raisebox{-1.0pt}{$\dotarrow{}$}\overline{b}$ and $\pi\Vdash
b\raisebox{-1.0pt}{$\dotarrow{}$}\overline{a}$. Obviously, this is not a pivot
policy which requires $\pi\Vdash a\mathrel{\diamond}\overline{b}$ or
$\pi\Vdash\overline{a}\mathrel{\diamond}b$. For contrast, the process
$Q\stackrel{{{}_{\mathit{def}}}}{{=}}a+\overline{b}{:}a\,|\,b\,|\,\overline{a}$
is pivotable as it conforms to the pivot policy with $\pi\Vdash
a\raisebox{-1.0pt}{$\dotarrow{}$}\overline{b}$ and
$\pi\Vdash\overline{a}\mathrel{\diamond}{}b$. Here, the choice between
synchronising on $a$ or on $b$ is uniquely resolved by the first thread
$a+\overline{b}{:}a$ which, being offered $\overline{a}$ and $b$ concurrently
by its environment, takes the synchronisation $\tau=a\,|\,\overline{a}$.

Input-scheduled processesare processes in which choices between distinct
actions need to be resolved only between receiver actions and clocks. In other
words, each thread executes its send actions always deterministically, rather
than in a preemption context. The policy $\pi_{is}$ forces all output actions
to be concurrently independent from each other. On the other hand, the policy
permits a process to introduce arbitrary priorites between receiver actions
and clocks. Note that $\pi_{is}$ is a pivot policy and thus every input-
scheduled process is pivotable.

Reductions of pivotable processes never block because of two threads entering
into a circular precedence deadlock with each other. Therefore, it suffices to
check enabling relative to the concurrent environment in which a rendez-vous
synchronisation is happening. One can show that for pivotable processes of at
most two threads, the three operational semantics of CCS (admissible), of
$\mathsf{CCS}^{\mathsf{Ph}}$ (weak enabling) and our
$\mathsf{CCS}^{\mathsf{spt}}$ (strong enabling) all coincide. This is a
consequence of the fact (cf. Lem. C.10 and C.12 in the Appendix) that the side
condition in the rule $(\textit{Par}_{3})$ is never introducing the silent
action $\tau$ into the blocking sets. In general, pivotable processes may
consist of three or more interacting threads. Then, blocking may occur and the
semantics of CCS, $\mathsf{CCS}^{\mathsf{Ph}}$ and
$\mathsf{CCS}^{\mathsf{spt}}$ are different. However, two single-threaded
pivotable processes never block each other.

######  Lemma 4.11.

Let $P_{1}:\pi$ and $P_{2}:\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.

The following proposition 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 4.12 (Clock Maximal Progress).

Suppose $P$ is coherent and pivotable and $\sigma\in\textsf{iA}(P)$. Then, for
all $\ell\in\mathcal{L}$ with $\ell\neq\sigma$ we have
$\ell\not\in\textsf{iA}(P)$ or $\overline{\ell}\not\in\textsf{iA}(P)$. In
particular, $P$ is in normal form, i.e., there is no reduction
$P\mathrel{\stackrel{{\scriptstyle\tau}}{{\rightarrow}}}P^{\prime}$.

Prop. 4.12 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 [15, 8]. More importantly (Thm. 4.4) 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. We identify a set of closure operators for coherent processes
based on policy-coherence. The associated Propositions D.6–D.23 (Appendix)
cover idling and prefixes (SSec. D.1), summation (SSec. D.2), parallel
composition (SSec. D.3), repetition (SSec. D.4), hiding (SSec. D.5) and
restriction (SSec. D.6). For lack of space, the results are summarised:

  * •

${{\mathsf{0}}}:\pi$ for all $\pi$.

  * •

If $Q:\pi$ then for every $\ell\in\mathcal{R}$ we have
$\ell{:}H{\mathsf{.}}Q:\pi$ if $\ell\in
H\subseteq\\{\ell^{\prime}\mid\pi\Vdash\ell^{\prime}\raisebox{-1.0pt}{$\dotarrow{}$}\ell\\}$.

  * •

If $Q:\pi$ and clock $\sigma\in\mathcal{C}$, then
$\sigma{:}H{\mathsf{.}}Q:\pi$ if
$H\subseteq\\{\beta\mid\pi\Vdash\beta\raisebox{-1.0pt}{$\dotarrow{}$}\sigma\\}$.

  * •

If $P_{1}:\pi_{1}$ and $P_{2}:\pi_{2}$ and for all pairs of initial
transitions $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{F_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}$
and $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{F_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\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}:\pi$ if $\pi_{1}\subseteq\pi$ and
$\pi_{2}\subseteq\pi$.

  * •

If $Q:\pi$ and $R:\pi$ where $\pi\,\backslash\,\mathcal{R}$ is a pivot policy.
Then $(Q\,|\,R)\mathrel{:}\pi$.

  * •

If $P:\pi$ and $\pi\,\backslash\,\mathcal{R}$ is a pivot policy then for each
$\ell\in\pi\,\backslash\,\mathcal{R}$, the sequential bang prefix
${\ell}^{\ast}{:}H{\mathsf{.}}P:\pi$ if
$H\subseteq\\{\ell^{\prime}\mid\pi\Vdash\ell^{\prime}\raisebox{-1.0pt}{$\dotarrow{}$}\ell\\}$.

  * •

If $Q:\pi$ and $\pi\nVdash\sigma\raisebox{-1.0pt}{$\dotarrow{}$}\ell$ for all
$\sigma\in L$, then $Q\,/\,L:\pi$.

  * •

If $Q:\pi$ and $\pi$ precedence-closed for $L\cup\overline{L}$, then
$({Q}\,\backslash\,{L}):\pi-L$.

These are processes that are structurally deterministic for clocks (Prop. 4.7)
and structurally confluent for strongly enabled reductions (Thm. 4.5).

##  5 Further work

We list in spare order some possible future works:

  * •

C-actions are somewhat related with continuation passing style, and, in some
sense they are more powerful because they do a kind of “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: introducing a partial order could be an interesting,
although economic and fine grained, way to reason about time and time
priorities.

  * •

Plugging a type system to $\mathsf{CCS}^{\mathsf{spt}}$ seems worth of study:
among possible type disciplines we just mention: behavioural type systems,
including session-types to capture rendez-vous interactions; intersection-
types, including non-idempotent ones to characterise termination and resources
awareness, and linear-types to model consuming resources.

## References

  * [1] H. Barendregt.  The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics.  North-Holland, Amsterdam, revised edition, 1984.
  * [2] 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.
  * [3] G. Berry.  The Constructive Semantics of Pure Esterel.  Draft Book, 1999.  ftp://ftp-sop.inria.fr/esterel/pub/papers/constructiveness3.ps.
  * [4] G. Berry.  The Foundations of Esterel.  In Proof, Language and Interaction: Essays in Honour of Robin Milner, pages 425–454. MIT Press, 2000.
  * [5] 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.
  * [6] 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.
  * [7] J. Camilleri and G. Winskel.  CCS with priority choice.  Information and Computation, 116(1):26–37, 1995.
  * [8] 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.
  * [9] V. Dieckert and G. Rozenberg, editors.  The Book of Traces.  World Scientific, 1995.
  * [10] S. A. Edwards.  On determinism.  In M. Lohstroh et. al., editor, Lee Festschrift, pages 240–253. Springer, 2018.
  * [11] 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.
  * [12] M. Mendler H. R. Andersen.  An asynchronous process algebra with multiple clocks.  In D. Sannella, editor, In Proc. ESOP’94, pages 58–73, 1994.
  * [13] 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.
  * [14] 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.
  * [15] M. Hennessy and T. Regan.  A process algebra for timed system.  Information and Computation, 117:221–239, 1995.
  * [16] C.A.R. Hoare.  Communicating Sequential Processes.  Prentice-Hall, 1985.  256 pages.
  * [17] C. D. Kloos and P. Breuer, editors.  Formal Semantics for VHDL.  Kluwer, 1995.
  * [18] J. W. Klop.  Combinatory reduction systems.  PhD thesis, Univ. Utrecht, 1980.
  * [19] E. A. Lee.  The problem with threads.  Computer, 39(5):33–42, 2006.
  * [20] E. A. Lee and T. M. Parks.  Dataflow process networks.  In Proceedings of the IEEE, pages 773–799, May 1995.
  * [21] G. Lüttgen and M. Mendler.  When 1 clock is not enough.  In L. Aceto and A.D. Gordon, editors, Algebraic Process Calculi: The First Twenty Five Years and Beyond (PA’05), number NS-05-03 in BRICS Notes Series, pages 155–158, June 2005.
  * [22] R. Milner.  Communication and Concurrency.  Prentice Hall, 1989.
  * [23] R. Milner.  Functions as processes.  Math. Struct. Comput. Sci., 2(2):119–141, 1992.  URL: https://doi.org/10.1017/S0960129500001407, doi:10.1017/S0960129500001407.
  * [24] 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.
  * [25] 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.
  * [26] 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.
  * [27] I. Phillips.  CCS with priority guards.  In K. G. Larsen and M. Nielsen, editors, Proc. Concur 2001, pages 305–320, 2001.
  * [28] 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.
  * [29] G. D. Plotkin.  A structural approach to operational semantics.  J. Log. Algebraic Methods Program., 60-61:17–139, 2004.
  * [30] V. Natarajan R. Cleaveland, G. Lüettgen.  Handbook of Process Agebra, chapter Priority in Process Algebra.  Elsevier, 2001.
  * [31] K. Schneider.  The synchronous programming language Quartz.  Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, December 2009.
  * [32] 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.
  * [33] 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.
  * [34] 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.
  * [35] R. J. van Glabbeek.  Notes on the methodology of CCS and CSP.  Theor. Comput. Sci., 177(2):329–349, 1997.  URL: https://doi.org/10.1016/S0304-3975(96)00251-4, doi:10.1016/S0304-3975(96)00251-4.
  * [36] 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.

##  Appendix A From Asynchronous Weak to Synchronous Strong Priorities

This rather informal section give 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.

###  A.1 CCS with (Weak) Priorities

Let us look in more detail on how the precedence mechanism suggested above
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 222Here we use equations systems to define recursive
processes. The process $S$ in solved form is
$S\stackrel{{{}_{\mathit{def}}}}{{=}}w{\mathsf{.}}(\mathop{\textsf{rec}}x.\,r{\mathsf{.}}x)+r{\mathsf{.}}(\mathop{\textsf{rec}}x.\,(r{\mathsf{.}}x+e{\mathsf{.}}x))$,
where $\mathop{\textsf{rec}}$ is a recursion operator such as used in CCS. In
the formal syntax that we use later, we will not use recursion but repetition
to express recursive processes. This will turn out to be more convenient to
control confluence, as we shall see. by the equations
$S\stackrel{{{}_{\mathit{def}}}}{{=}}w{\mathsf{.}}S^{\prime}+r{\mathsf{.}}S^{\prime\prime}$
where $S^{\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime}$
and
$S^{\prime\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime\prime}+e{\mathsf{.}}S^{\prime\prime}$.

Figure 5: 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^{\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime}$ and
$S^{\prime\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime\prime}+e{\mathsf{.}}S^{\prime\prime}$.
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.

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^{\prime}$. In this filled state
$S^{\prime}$ 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^{\prime\prime}$ which represents an
error state. In the error state $S^{\prime\prime}$ 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^{\prime}$, while the write only in state $S$. If $S$ is put in parallel
with a reader offering $\overline{r}$ and a writer offering $\overline{w}$,
then the final state of $S$ depends on the order between the $\overline{r}$
and $\overline{w}$ actions. If we synchronise with the external sequence
$\overline{r}{\mathsf{.}}\overline{w}$ on $S$ where the read action is first,
the writer gets blocked on the error state $S^{\prime\prime}$, while if we
exercise $\overline{w}{\mathsf{.}}\overline{r}$ where the write action is
first, both can proceed and we obtain filled state $S^{\prime}$ (in term
rewriting system jargon [18] this is called “critical pairs”).

Formally, let
$R\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{r}{\mathsf{.}}{{\mathsf{0}}}$
be a reader process with a single read and
$W\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{w}{\mathsf{.}}{{\mathsf{0}}}$
the writer with a single write, both terminating in the empty behaviour
${{\mathsf{0}}}$. Then, according to the operational semantics of CCS, we have
the two execution sequences $R\,|\,S\,|\,W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}{{\mathsf{0}}}\,|\,S^{\prime\prime}\,|\,W$
and $R\,|\,S\,|\,W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}R\,|\,S^{\prime}\,|\,{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}{{\mathsf{0}}}\,|\,S^{\prime}\,|\,{{\mathsf{0}}}$,
where both configurations ${{\mathsf{0}}}\,|\,S^{\prime\prime}\,|\,W$ and
${{\mathsf{0}}}\,|\,S^{\prime\prime}\,|\,{{\mathsf{0}}}$ are distinct normal
forms, in the sense that no reductions are possible anymore. This is
pictorially illustrated in Fig. 5. Observe that the behaviour is not only non-
deterministic in the sense that there is more than one scheduling sequence. It
is also non-deterministic as the final outcome depends on the scheduling
decisions.

Among many CCS extension with priorities, we looked the one of Camilleri and
Winskell [7], referrered to as $\mathsf{CCS}^{\mathsf{CW}}$ in the sequel.
$\mathsf{CCS}^{\mathsf{CW}}$ provide a prioritised choice operator
$Q\stackrel{{{}_{\mathit{def}}}}{{=}}\alpha_{1}.Q_{1}\mathrel{\smalltriangleright}\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{\mathsf{.}}S^{\prime}+r{\mathsf{.}}S^{\prime\prime}$. 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 prioritised $\mathsf{CCS}^{\mathsf{CW}}$
[7] as
$S\stackrel{{{}_{\mathit{def}}}}{{=}}w{\mathsf{.}}S^{\prime}\mathrel{\smalltriangleright}r{\mathsf{.}}S^{\prime\prime}$
in which the prisum $\mathrel{\smalltriangleright}$ operator enforces a
precedence from left to right. The store $S$ is willing to engage in a read
action $r$ (to the right of $\mathrel{\smalltriangleright}$) only if the
environment does not offer a write $w$ (on the left of
$\mathrel{\smalltriangleright}$) at the same time, concurrently.

Another important study in the endeavour of adding priorities to CCS is the
work of Phillips. In Phillips’ extension of CCS with priority guards [27],
referred to as $\mathsf{CCS}^{\mathsf{Ph}}$, the previous behavior is
expressed by
$S\stackrel{{{}_{\mathit{def}}}}{{=}}{\\{\,\\}{:}w}{\mathsf{.}}\,S^{\prime}+{\\{w\\}{:}r}{\mathsf{.}}\,S^{\prime\prime}$,
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^{\prime\prime}$ 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^{\prime}$. 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 [7, 27, 30], let us write $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
to denote that process $P$ can engage in an action $\alpha$ to continue as
$P^{\prime}$, 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 rules for prefix and choice in $\mathsf{CCS}^{\mathsf{CW}}$ are the
following333For the fragment of $\mathsf{CCS}^{\mathsf{CW}}$ that we are
considering, the precise connection is the following: $\vdash_{R}P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{}\,$}P^{\prime}$
in $\mathsf{CCS}^{\mathsf{CW}}$ iff $R$ is a subset of $out$-actions and there
is a subset $L$ of $in$-actions such that $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
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}=\\{\,\\}$.:

(Act) $\alpha{\mathsf{.}}P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{\\{\,\\}}}\,$}P$
$P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
$(\textit{PriSum}_{1})$ $P\mathrel{\smalltriangleright}Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{L}}\,$}P^{\prime}$
$Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}Q^{\prime}$
$\tau,\alpha\not\in\textsf{iA}(P)$ $(\textit{PriSum}_{2})$
$P\mathrel{\smalltriangleright}Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H\cup\textsf{iA}(P)}}\,$}Q^{\prime}$

where $\textsf{iA}(P)$ (defined formally later) represents the set of initial
actions of $P$ that are offered by $P$ in some environment and
$\mathrel{\smalltriangleright}$ is the priority sum defined by
$\mathsf{CCS}^{\mathsf{CW}}$. From rule $(\textit{Act})$, individual prefixes
generate transitions without any blocking constraints. Rules
$(\textit{PriSum}_{1})$ and $(\textit{PriSum}_{2})$ describe how the
transitions of a choice $P\mathrel{\smalltriangleright}Q$ are obtained from
the transitions of $P$ and of $Q$: more in details, rule
$(\textit{PriSum}_{1})$ lets all transitions of the higher-prioritised process
$P$ pass through to form a transition of the choice
$P\mathrel{\smalltriangleright}Q$ without restriction. This is different for
$Q$, where, according to rule $(\textit{PriSum}_{2})$, 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:

$P_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}^{\prime}$
$H_{1}\cap\overline{\textsf{iA}}(P_{2})=\\{\,\\}$ $(\textit{Par}_{1})$
$P_{1}\,|\,P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H}}\,$}P_{1}^{\prime}\,|\,P_{2}$
$P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}}}\,$}P_{2}^{\prime}$
$H_{2}\cap\overline{\textsf{iA}}(P_{1})=\\{\,\\}$ $(\textit{Par}_{2})$
$P_{1}\,|\,P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}}}\,$}P_{1}\,|\,P_{2}^{\prime}$
$P_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}^{\prime}$
$P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}}}\,$}P_{2}^{\prime}$
$\alpha_{1}=\overline{\alpha}_{2}$
$H_{1}\cap\overline{\textsf{iA}}(P_{2})=\\{\,\\}$
$H_{2}\cap\overline{\textsf{iA}}(P_{1})=\\{\,\\}$ $(\textit{Par}_{3})$
$P_{1}\,|\,P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H_{1}\cup
H_{2}}}\,$}P_{1}^{\prime}\,|\,P_{2}^{\prime}$

More in details, rules $(\textit{Par}_{i})$ for $i\in\\{1,2\\}$ define an
action $\alpha_{i}$ by $P_{1}\,|\,P_{2}$ offered in one of the sub-processes
$P_{i}$. Such is enabled if the competing concurrent process $P_{3-i}$ has no
initial action that is in the blocking set $H_{i}$ of action $\alpha_{i}$,
i.e. when the condition $H_{i}\cap\overline{\textsf{iA}}(P_{3-i})=\\{\,\\}$ is
satisfied. Rule $(\textit{Par}_{3})$ implements the synchronisation between an
action $\alpha_{1}$ in $P_{1}$ and the associated matching action
$\alpha_{2}=\overline{\alpha}_{1}$, originating from $P_{2}$. The side-
condition is the same: each process $P_{i}$ only accepts the matching action
call from $P_{3-i}$ if it does not offer any action that blocks action
$\alpha_{i}$.

$S\stackrel{{{}_{\mathit{def}}}}{{=}}w{\mathsf{.}}S^{\prime}\,{\color[rgb]{0.9,0,0}{\mathrel{\smalltriangleright}}}\,r{\mathsf{.}}S^{\prime\prime}$

Figure 6: 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
$\tau{:}\\{w\\}$. Since there is only one execution path, the system is
deterministic. The continuations states
$S^{\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime}$ and
$S^{\prime\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime\prime}+e{\mathsf{.}}S^{\prime\prime}$
of the cell are the same as in Fig. 5.

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\stackrel{{{}_{\mathit{def}}}}{{=}}w{\mathsf{.}}S^{\prime}\mathrel{\smalltriangleright}r{\mathsf{.}}S^{\prime\prime},S^{\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime},\mbox{
and
}S^{\prime\prime}\stackrel{{{}_{\mathit{def}}}}{{=}}r{\mathsf{.}}S^{\prime\prime}+e{\mathsf{.}}S^{\prime\prime}.$
The cell $S$ has two potential transitions that can be fired, namely

$(\textit{Act})$ $w{\mathsf{.}}S^{\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{w}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime}$
$(\textit{PriSum}_{1})$ $S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{w}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime}$
or  $(\textit{Act})$ $r{\mathsf{.}}S^{\prime\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime\prime}$
$\tau,r\not\in\textsf{iA}(w{\mathsf{.}}S^{\prime})$ $(\textit{PriSum}_{2})$
$S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{w\\}}}\,$}S^{\prime\prime}$

considering that $\textsf{iA}(w{\mathsf{.}}S^{\prime})=\\{w\\}$. The latter
transition synchronises with the reader process’ $\overline{r}$ transition to
give $R\,|\,S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}{{\mathsf{0}}}\,|\,S^{\prime\prime}$
as verified by the derivation

$(\textit{Act})$ $R\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{r}}$}}\\!\\!{{}_{\\{\,\\}}}\,$}{{\mathsf{0}}}$
$\vdots$ $S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{w\\}}}\,$}S^{\prime\prime}$
$\\{\,\\}\cap\overline{\textsf{iA}}(S)=\\{\,\\}$
$\\{w\\}\cap\overline{\textsf{iA}}(R)=\\{\,\\}$ $(\textit{Par}_{3})$
$R\,|\,S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}{{\mathsf{0}}}\,|\,S^{\prime\prime}$

in which the side-conditions
$\\{w\\}\cap\overline{\textsf{iA}}(R)=\\{w\\}\cap\\{r\\}=\\{\,\\}$ and
$\\{\,\\}\cap\overline{\textsf{iA}}(S)=\\{\,\\}$ of rule $(\textit{Par}_{3})$
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 $\overline{w}\in\textsf{iA}(W)$ conflicts with the
silent transition. The execution in the context $E=[\cdot]\,|\,W$ is blocked
by rule $(\textit{Par}_{1})$, because
$\\{w\\}\cap\overline{\textsf{iA}}(W)=\\{w\\}\cap\\{w\\}\neq\\{\,\\}$. The
derivation tree

$(\textit{Act})$ $R\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{r}}$}}\\!\\!{{}_{\\{\,\\}}}\,$}{{\mathsf{0}}}$
$(\textit{Act})$ $r{\mathsf{.}}S^{\prime\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime\prime}$
$(\textit{PriSum}_{2})$ $S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{w\\}}}\,$}S^{\prime\prime}$
$(\textit{Par}_{3})$ $R\,|\,S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}{{\mathsf{0}}}\,|\,S^{\prime\prime}$
${\color[rgb]{0.9,0,0}{\\{w\\}\cap\textsf{iA}(W)\neq\\{\,\\}}}$
$(\textit{Par}_{1})$
${\color[rgb]{0.9,0,0}{R\,|\,S\,|\,W\,\,\,/\\!\\!\\!\\!\\!\\!\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w\\}}}\,$}{{\mathsf{0}}}\,|\,S^{\prime\prime}\,|\,W}}$

where the side-conditions of $(\textit{PriSum}_{2})$ and of
$(\textit{Par}_{3})$ are satisfied, blocks at side-condition of rule
$(\textit{Par}_{1})$. On the other hand, the writing of $S$ by $W$ followed by
the reading of $S^{\prime}$ by $R$ can be derived, i.e., we have
$R\,|\,S\,|\,W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\,\\}}}\,$}R\,|\,S^{\prime}\,|\,{{\mathsf{0}}}\text{
and }R\,|\,S^{\prime}\,|\,{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\,\\}}}\,$}{{\mathsf{0}}}\,|\,S^{\prime}\,|\,{{\mathsf{0}}}.$
The derivation trees in the SOS are as follows

$(\textit{Act})$ $w{\mathsf{.}}S^{\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{w}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime}$
$(\textit{PriSum}_{1})$ $S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{w}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime}$
$(\textit{Par}_{2})$ $R\,|\,S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{w}$}}\\!\\!{{}_{\\{\,\\}}}\,$}R\,|\,S^{\prime}$
$(\textit{Act})$ $W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{w}}$}}\\!\\!{{}_{\\{\,\\}}}\,$}{{\mathsf{0}}}$
$(\textit{Par}_{3})$ $R\,|\,S\,|\,W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\,\\}}}\,$}R\,|\,S^{\prime}\,|\,{{\mathsf{0}}}$
$(\textit{Act})$ $R\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{r}}$}}\\!\\!{{}_{\\{\,\\}}}\,$}{{\mathsf{0}}}$
$(\textit{Act})$ $S^{\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime}$
$(\textit{Par}_{1})$ $S^{\prime}\,|\,0\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{\,\\}}}\,$}S^{\prime}\,|\,{{\mathsf{0}}}$
$(\textit{Par}_{3})$ $R\,|\,S^{\prime}\,|\,{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\,\\}}}\,$}{{\mathsf{0}}}\,|\,S^{\prime}\,|\,{{\mathsf{0}}}$

where the blocking side-conditions of $(\textit{Par}_{1})$,
$(\textit{Par}_{2})$ and $(\textit{Par}_{3})$ are all trivially satisfied. The
scheduling which resolves the non-determinism is depicted in Fig. 6.

###  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 (that we sometimes call “precedence-based” in this paper).

What we want is that every process using only strong priority satisfies the
following weak local confluence property [18]. Suppose $P$ admits two
transitions to different states $P_{1}\neq P_{2}$ that do not block each
other, i.e., $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}\text{
and }P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}}}\,$}P_{2}$
such that $\alpha_{1}\not\in H_{2}$ and $\alpha_{2}\not\in H_{1}$. Then, each
action $\alpha_{i}$ (for $i\in\\{1,2\\}$) is still admissible in $P_{3-i}$,
and there exist $P^{\prime}$ and $H_{i}^{\prime}\subseteq H_{i}$ such that
$P_{i}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{3-i}}$}}\\!\\!{{}_{H_{i}^{\prime}}}\,$}P^{\prime}.$
The assumption $\alpha_{i}\not\in H_{3-i}$ uses the blocking sets to express
non-interference between transitions. Then, our weak444In the pure
$\lambda$-calculus the diamond property holds for $\beta$-reduction without
any assumptions. We use the term “weak” confluence, because of the side-
condition of non-interference. local confluence expresses a weak “diamond
property” stating that every diverging choice of non-interfering transitions
immediately reconverges. The subset inclusions $H_{i}^{\prime}\subseteq H_{i}$
ensure that delaying an admissible action does not introduce more chances of
interference.

####  A.2.1 Fix 1

The standard notion of priority for CCS, as implemented in
$\mathsf{CCS}^{\mathsf{CW}}$ or $\mathsf{CCS}^{\mathsf{Ph}}$, of course was
not designed to restrict CCS for determinism but to extend it conservatively
to be able to express scheduling control. Even in the fragment of
$\mathsf{CCS}^{\mathsf{CW}}$ 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{{{}_{\mathit{def}}}}{{=}}W_{1}\,|\,[\cdot]\,|\,W_{2}$ of
two writers
$W_{i}\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{w}{\mathsf{.}}W_{i}^{\prime}$,
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
$\mathsf{CCS}^{\mathsf{CW}}$ we can derive the (non-interfering) transitions
$W_{1}\,|\,S\,|\,W_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\,\\}}}\,$}W_{1}^{\prime}\,|\,S^{\prime}\,|\,W_{2}\text{
and }W_{1}\,|\,S\,|\,W_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\,\\}}}\,$}W_{1}\,|\,S^{\prime}\,|\,W_{2}^{\prime}.$
Still, the two outcomes of the divergence are a critical pair that have no
reason to reconverge $W_{1}^{\prime}\,|\,S^{\prime}\,|\,W_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{$$}}\\!\\!{}\,$}P^{\prime}$
and $W_{1}\,|\,S^{\prime}\,|\,W_{2}^{\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{$$}}\\!\\!{}\,$}P^{\prime}$
if $W_{i}^{\prime}$ are arbitrary behaviours. To preserve confluence we must
block the environment from consuming the single prefix
$w{\mathsf{.}}S^{\prime}$ twice. The problem is that the synchronisations
$W_{1}\,|\,S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H_{1}}}\,$}W_{1}^{\prime}\,|\,S^{\prime}\text{
and }S\,|\,W_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H_{2}}}\,$}S\,|\,W_{2}^{\prime}$
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
$(\textit{Par}_{3-i})$ would automatically prevent the second reader. Now,
suppose we extend the action rule $(\textit{Act})$ to expose the singleton
nature of a prefix, like by $(\textit{Act}^{+})$, $\alpha{\mathsf{.}}P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{\\{\alpha\\}}}\,$}P$
we would not only prevent a second concurrent writer but already a single
writer. The transitions $W_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{w}}$}}\\!\\!{{}_{\\{\overline{w}\\}}}\,$}W_{1}^{\prime}\text{
and }S\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{w}$}}\\!\\!{{}_{\\{w\\}}}\,$}S^{\prime}$
would not be able to communicate, violating both side-condition
$\\{\overline{w}\\}\cap\overline{\textsf{iA}}(S)=\\{\,\\}$ and
$\\{w\\}\cap\overline{\textsf{iA}}(W_{1})=\\{\,\\}$ of $(\textit{Par}_{3})$.
The issue is that in the setting of $\mathsf{CCS}^{\mathsf{CW}}$ (and
$\mathsf{CCS}^{\mathsf{Ph}}$) the blocking set $H$ of a transition $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
expresses a priority rather than an interference. An action cannot take
priority over itself without blocking itself. Therefore, in
$\mathsf{CCS}^{\mathsf{CW}}$ (and $\mathsf{CCS}^{\mathsf{Ph}}$) we always have
$\alpha\not\in H$. Here, we need to apply a weaker interpretation. The actions
in $H$ only prevent $\alpha$ from synchronising with a matching
$\overline{\alpha}$ in the environment, if they are executed in a different
(and thus competing) prefix from the one that executes $\overline{\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
$\overline{\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\overline{\textsf{iA}}(P_{3-i})$ in $(\textit{Par}_{3})$ to check
not all initial actions $\overline{\textsf{iA}}(P_{3-i})$ but only those
initial actions of $P_{3-i}$ that are competing with the matching transitions
$P_{1}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{1}}$}}\\!\\!{{}_{H_{1}}}\,$}P_{1}^{\prime}\text{
and }P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{2}}$}}\\!\\!{{}_{H_{2}}}\,$}P_{2}^{\prime}$
with $\alpha_{1}=\overline{\alpha}_{2}$, involved in the communication
$P_{1}\,|\,P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H_{1}\cup
H_{2}}}\,$}P_{1}^{\prime}\,|\,P_{2}^{\prime}$ that we want to protect. We fix
this by refining the information exposed by a transition. More specifically,
we extend each transition $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{K}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{H}}\,$}P^{\prime}$
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
$\textsf{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 A.1.

Note that we cannot simply define
$K\stackrel{{{}_{\mathit{def}}}}{{=}}\textsf{iA}(P)-\\{\alpha\\}$, because
$\alpha$ could be contained in $K$. For example, take
$P\stackrel{{{}_{\mathit{def}}}}{{=}}\alpha{\mathsf{.}}{{\mathsf{0}}}\,|\,\alpha{\mathsf{.}}{{\mathsf{0}}}$,
where $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{\alpha\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha}$}}\\!\\!{{}_{\\{\alpha\\}}}\,$}\alpha{\mathsf{.}}{{\mathsf{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 $\textsf{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

$P_{i}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{K_{i}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\alpha_{i}}$}}\\!\\!{{}_{H_{i}}}\,$}P_{i}^{\prime}$
$\alpha_{1}=\overline{\alpha}_{2}$ $H_{i}\cap\overline{K}_{3-i}=\\{\,\\}$ for
$i\in\\{1,2\\}$ $(\textit{Par}_{3}^{+})$ $P_{1}\,|\,P_{2}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{K_{1}\cup
K_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H_{1}\cup
H_{2}}}\,$}P_{1}^{\prime}\,|\,P_{2}^{\prime}$

and achieve the same as before but can accommodate the action rule
$(\textit{Act}^{+})$ that introduces a “reflexive precedence”.

####  A.2.2 Fix 2

Figure 7: The store $S$ in composition with a reader
$\overline{r}{\mathsf{.}}{{\mathsf{0}}}$ and a delayed writer
$d{\mathsf{.}}{{\mathsf{0}}}\,|\,\overline{d}{\mathsf{.}}\overline{w}{\mathsf{.}}{{\mathsf{0}}}$.
The behaviour has two incongruent final outcomes, a store $S^{\prime\prime}$
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.

In the previous subsection we have seen how priorities can be beneficial to
approaching to a deterministic scheduling in an intrinsic non-deterministic
PA. 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\mathrel{\smalltriangleright}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{\mathsf{.}}P$ are of form
$\alpha{\mathsf{.}}{{\mathsf{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{{{}_{\mathit{def}}}}{{=}}S\,|\,d{\mathsf{.}}{{\mathsf{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{{{}_{\mathit{def}}}}{{=}}\overline{d}{\mathsf{.}}W\stackrel{{{}_{\mathit{def}}}}{{=}}\overline{d}{\mathsf{.}}\overline{w}{\mathsf{.}}{{\mathsf{0}}}.$
The scheduling sequences are depicted in Fig. 7. We can still derive
$S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{w,d\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{r,w\\}}}\,$}S^{\prime\prime}\,|\,d{\mathsf{.}}{{\mathsf{0}}}\text{
but also }S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{r,w\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{d}$}}\\!\\!{{}_{\\{d\\}}}\,$}S.$
The reading synchronisation $R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{w,d\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\overline{r},r,w\\}}}\,$}S^{\prime\prime}\,|\,d{\mathsf{.}}{{\mathsf{0}}}$
can now take place by $(\textit{Par}_{3})$ before the write to give the
following reduction sequence:
$R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{w,d,\overline{d}\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\overline{r},r,w\\}}}\,$}S^{\prime\prime}\,|\,d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{r,e\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{d\\}}}\,$}S^{\prime\prime}\,|\,W.$
The first reduction is justified by rule $(\textit{Par}_{1})$, because the
side-condition
$\\{w\\}\cap\overline{\textsf{iA}}(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 $\overline{w}$ by $W^{*}$
hidden behind its initial action $\overline{d}$. It lets process $R$ access
and read the store $S$. As before, however, the following reduction sequence
is allowed, too: $R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{\overline{r},r,w\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{d\\}}}\,$}R\,|\,S\,|\,W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{\overline{r},r\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w,\overline{w}\\}}}\,$}R\,|\,S^{\prime}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{\\{w\\}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{\overline{r},r,w\\}}}\,$}S^{\prime}$
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^{\prime}$ or $S^{\prime\prime}$, non-deterministically.

Our insight is that the blocking side-conditions of the standard Camilleri-
Winskell theory [7], described above, are too weak in scheduling control for
our purposes and to guaranteeing a weak Church-Rosser property [18]. The
problem is that in the side-condition of rule $\textit{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. 7 but not out of state ①. In state ① there is no
pending initial write. The write action $\overline{w}$ only becomes initial
when the parallel processes
$\overline{d}{\mathsf{.}}{{\mathsf{0}}}\,|\,d{\mathsf{.}}\overline{w}{\mathsf{.}}{{\mathsf{0}}}$
have interacted on action $d$ and advanced together with a silent action
$\tau$, i.e.
$\overline{d}{\mathsf{.}}{{\mathsf{0}}}\,|\,d{\mathsf{.}}\overline{w}{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{$$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{}\,$}{{\mathsf{0}}}\,|\,\overline{w}{\mathsf{.}}{{\mathsf{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 $\overline{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\textsf{iA}(E)$. This
finally gives a transition relation of the form $P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{a}$}}\\!\\!{{}_{H\cup
L}}\,$}P^{\prime}.$ The label $E$, called the reduction context, is
accumulated in the parallel compositions of $P$. The rules $(\textit{Act})$
and $(\textit{PriSum}_{i})$ are the one presented above. Further, let
$\textsf{iA}^{\tau}(E)$ be informally the set of all actions that can become
initial along $\tau$-sequences from $E$, which obviously includes
$\textsf{iA}(E)$ (formally defined later on). We will call the set
$\textsf{iA}^{\tau}(E)$ the set of weak initial actions of $E$. The rules
$(\textit{Par}^{{}_{\ast}}_{1})$ and $(\textit{Par}^{{}_{\ast}}_{2})$ need to
be reformulated. Rule $(\textit{Par}^{{}_{\ast}}_{1})$, propagating an action
in a parallel composition, is as follows:

$P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{a}$}}\\!\\!{{}_{H\cup
L}}\,$}P^{\prime}$ $E^{\prime}=E\,|\,Q$
$H\cap\overline{\textsf{iA}^{\tau}}(E^{\prime})=\\{\,\\}$
$(\textit{Par}^{{}_{\ast}}_{1})$ $P\,|\,Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E^{\prime}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{a}$}}\\!\\!{{}_{H\cup
L}}\,$}P^{\prime}\,|\,Q$

Rule $(\textit{Par}^{{}_{\ast}}_{2})$ is symmetric to
$(\textit{Par}^{{}_{\ast}}_{1})$. Rule $(\textit{Par}_{3})$, for the
synchronisation of an action $\alpha$ and its co-action $\overline{\alpha}$
using these weak initial sets, is reformulated as follows:

$P\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E_{1}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{a}$}}\\!\\!{{}_{H_{1}\cup
L_{1}}}\,$}P^{\prime}$ $Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E_{2}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{\alpha}}$}}\\!\\!{{}_{H_{2}\cup
L_{2}}}\,$}Q^{\prime}$ $E=E_{1}\,|\,E_{2}$ $\forall
i.\,H_{i}\cap(\overline{\textsf{iA}^{\tau}}(E)\cup L_{3-i})=\\{\,\\}$
$(\textit{Par}^{{}_{\ast}}_{3})$ $P\,|\,Q\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{E}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{H_{1}\cup
H_{2}\cup L_{1}\cup L_{2}}}\,$}P^{\prime}\,|\,Q^{\prime}$

We are now ready to revisit our running example. By
$(\textit{Par}^{{}_{\ast}}_{2})$, since

$R\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{r}}$}}\\!\\!{{}_{\\{r\\}\cup\\{\,\\}}}\,$}R^{\prime}\text{
and }S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{d{\mathsf{.}}{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{r}$}}\\!\\!{{}_{\\{w,r\\}\cup\\{\,\\}}}\,$}S^{\prime\prime}\text{,
we get }R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{d{\mathsf{.}}{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{w,r\\}\cup\\{\,\\}}}\,$}S^{\prime\prime}\,|\,d{\mathsf{.}}{{\mathsf{0}}}.$

The side-condition of $(\textit{Par}^{{}_{\ast}}_{3})$ is satisfied since the
“weak” initial action set (where $\tau$ actions are dropped)
$\textsf{iA}^{\tau}(d{\mathsf{.}}{{\mathsf{0}}})=\\{d\\}$. Thus, both
$\\{r\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(d{\mathsf{.}}{{\mathsf{0}}})=\\{\,\\}$
as well as
$\\{w,r\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(d{\mathsf{.}}{{\mathsf{0}}})=\\{\,\\}$.
If now want to shunt this past the writer process $W^{*}$ using rule
$(\textit{Par}^{{}_{\ast}}_{1})$, then we get stuck. Since
$d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{d,\overline{d}\\}\cup\\{\,\\}}}\,$}W$
and $\overline{w}\in\textsf{iA}(W)$, we find
$\overline{w}\in\textsf{iA}^{\tau}(d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*})$ and
thus
$\\{w\\}\cap\overline{\textsf{iA}}^{{}_{\ast}}(d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*})\neq\\{\,\\}$.
Therefore, the side-condition of $(\textit{Par}^{{}_{\ast}}_{1})$ is violated
and the reading interaction of $R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}$
cannot be composed with $W^{*}$. This is what we want. The transition from
state ② to state ③ in Fig. 7 is now blocked. On the other hand, the reduction
$R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R\,|\,S}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{d}$}}\\!\\!{{}_{\\{d\\}\cup\\{\,\\}}}\,$}R\,|\,S\text{
can be composed with }W^{*}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{{{\mathsf{0}}}}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\overline{d}}$}}\\!\\!{{}_{\\{\overline{d}\\}\cup\\{\,\\}}}\,$}W$
via $(\textit{Par}^{{}_{\ast}}_{3})$ to make a reduction
$R\,|\,S\,|\,d{\mathsf{.}}{{\mathsf{0}}}\,|\,W^{*}\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{R\,|\,S}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{d,\overline{d}\\}\cup\\{\,\\}}}\,$}R\,|\,S\,|\,W.$
Regarding the side-condition, we notice that the weak initial action set
$\textsf{iA}^{\tau}(R\,|\,S)$ of the reduction context is irrelevant, because
it does not contain $d$ or $\overline{d}$. In configuration $R\,|\,S\,|\,W$
(state ② in Fig. 7), the reader $R$ cannot interact with $S$. The associated
reduction $R\,|\,S\,|\,W\mbox{
$\xrightarrow[\raisebox{-2.5pt}[0.0pt][0.0pt]{${}^{W}$}]{\raisebox{-5.0pt}[0.0pt][0.0pt]{${}^{\tau}$}}\\!\\!{{}_{\\{r,w\\}\cup\\{\,\\}}}\,$}S^{\prime\prime}\,|\,W$
is blocked by the reduction environment, because
$w\in\overline{\textsf{iA}}^{{}_{\ast}}(\overline{w}{\mathsf{.}}W^{\prime})$.
For our further discussion, let us call the proposed change in the side-
conditions leading to $(\textit{Par}^{{}_{\ast}}_{i})$ from
$(\textit{Par}^{{}_{\ast}}_{i})$ a process algebra with strong
priorities555The 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. and let’s call the traditional process algebra with
priorities, introduced by [7, 30], as process algebra with weak priorities.

####  A.2.3 Digression: Strong Priorities lead to some 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{\textsf{iA}}^{{}_{\ast}}(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 $\textsf{iA}^{\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 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
$\mathop{\textsf{rec}}p.\,P$ to have a transition to $P^{\prime}$ if it does
not have a transition to $P^{\prime}$ for a suitable $P^{\prime}$? Such would
be plainly inconsistent at the meta-level, because it would not only define
simply an empty transition relation666As an example consider the unguarded
process $\mathop{\textsf{rec}}p{\mathsf{.}}p$ in the standard inductive