Process Algebra with Strategic Interleaving
 54 Downloads
Abstract
In process algebras such as ACP (Algebra of Communicating Processes), parallel processes are considered to be interleaved in an arbitrary way. In the case of multithreading as found in contemporary programming languages, parallel processes are actually interleaved according to some interleaving strategy. An interleaving strategy is what is called a processscheduling policy in the field of operating systems. In many systems, for instance hardware/software systems, we have to do with both parallel processes that may best be considered to be interleaved in an arbitrary way and parallel processes that may best be considered to be interleaved according to some interleaving strategy. Therefore, we extend ACP in this paper with the latter form of interleaving. The established properties of the extension concerned include an elimination property, a conservative extension property, and a unique expansion property.
Keywords
Process algebra Arbitrary interleaving Strategic interleaving Abstract scheduler Interleaving history1 Introduction
In algebraic theories of processes, such as ACP [5, 7], CCS [18, 21] and CSP [12, 19], processes are discrete behaviours that proceed by doing steps in a sequential fashion. The parallel composition of two processes is usually considered to incorporate all conceivable interleavings of their steps. In each interleaving, the steps of both processes occur in some order where each time one step is taken from either of the processes. According to many, this interpretation of parallel composition, called arbitrary interleaving, is a plausible, general, if not idealized interpretation. Underlying the usual justification of this claim is the assumption that at most one step is done at each point in time. However, others contend that interpretations in which this simplifying assumption is fulfilled are not faithful. Be that as it may, arbitrary interleaving turns out to be appropriate for many applications and to facilitate formal algebraic reasoning.
Multithreading as found in programming languages such as Java [16] and C# [17], gives rise to parallel composition of processes. In the case of multithreading, however, the steps of the processes concerned are interleaved according to a processscheduling policy. We use the term strategic interleaving for this more constrained form of interleaving; and we further use the term interleaving strategy instead of processscheduling policy. Arbitrary interleaving and strategic interleaving are quite different. The following points illustrate this: (a) whether the interleaving of certain processes leads to inactiveness depends on the interleaving strategy used; (b) sometimes inactiveness occurs with a particular interleaving strategy whereas arbitrary interleaving would not lead to inactiveness and vice versa.
In previous work, we studied strategic interleaving in the setting of thread algebra, which is built on a specialized algebraic theory of processes devoted to the behaviours produced by instruction sequences under execution (see e.g. [8, 9, 10]). We have, for instance, given demonstrations of points (a) and (b) above in this setting. Nowadays, multithreading is often used in the implementation of systems. Because of this, in many systems, for instance hardware/software systems, we have to do with parallel processes that may best be considered to be interleaved in an arbitrary way as well as parallel processes that may best be considered to be interleaved according to some interleaving strategy. This is what motivated us to do the work presented in this paper, namely extending ACP such that it supports both arbitrary interleaving and strategic interleaving.
To our knowledge, there exists no work on strategic interleaving in the setting of a general algebraic theory of processes like ACP, CCS and CSP. In the work presented in this paper, we consider strategic interleaving where process creation is taken into account. The approach to process creation followed in this paper originates from the one first followed in [6] to extend ACP with process creation and later followed in [2, 3, 11] to extend different timed versions of ACP with process creation. The only other approach that we know of is the approach, based on [1], that has for instance been followed in [4, 14]. However, with that approach, it is most unlikely that data about the creation of processes can be made available for the decision making concerning the strategic interleaving of processes.
The extension of ACP presented in this paper covers a generic interleaving strategy that can be instantiated with different specific interleaving strategies. We found two plausible ways to deal with inactiveness of a process whose steps are being interleaved with steps of other processes in the case of strategic interleaving. This gives rise to two plausible extensions of ACP. We will treat only one of them in detail.
The rest of this paper is organized as follows. In Section 2, we review ACP (Section 2.1), guarded recursion in the setting of ACP (Section 2.2), and some relevant results about the latter (Section 2.3). In Section 3, we extend ACP with strategic interleaving (Section 3.1) and establish some important properties of the extension (Section 3.2). In Section 4, we make some concluding remarks.
2 ACP with Guarded Recursion
In this section, we give a survey of ACP (Algebra of Communicating Processes), guarded recursion in the setting of ACP, and some relevant results about the extension of ACP with guarded recursion. For a comprehensive overview, the reader is referred to [5, 13].
2.1 ACP
In ACP, it is assumed that a fixed but arbitrary set A of actions, with δ∉A, has been given. We write A_{δ} for A ∪{δ}. It is further assumed that a fixed but arbitrary commutative and associative communication function γ: A_{δ} ×A_{δ} →A_{δ}, with γ(δ,a) = δ for all a ∈A_{δ}, has been given. The function γ is regarded to give the result of synchronously performing any two actions for which this is possible, and to give δ otherwise.

for each a ∈A, the action constant a ;

the inaction constant δ ;

the binary alternative composition operator _+_ ;

the binary sequential composition operator _ ⋅_ ;

the binary parallel composition operator _∥_ ;

the binary left merge operator Open image in new window ;

the binary communication merge operator _∣_ ;

for each H ⊆A, the unary encapsulation operator ∂_{H}.

the constant a denotes the process that is only capable of first performing action a and next terminating successfully;

the constant δ denotes the process that is not capable of doing anything;

a closed term of the form t + t^{′} denotes the process that behaves either as the process denoted by t or as the process denoted by t^{′}, but not both;

a closed term of the form t ⋅ t^{′} denotes the process that first behaves as the process denoted by t and on successful termination of that process it next behaves as the process denoted by t^{′};

a closed term of the form t∥t^{′} denotes the process that behaves as the process that proceeds with the processes denoted by t and t^{′} in parallel;

a closed term of the form Open image in new window denotes the process that behaves the same as the process denoted by t∥t^{′}, except that it starts with performing an action of the process denoted by t;

a closed term of the form t∣t^{′} denotes the process that behaves the same as the process denoted by t∥t^{′}, except that it starts with performing an action of the process denoted by t and an action of the process denoted by t^{′} synchronously;

a closed term of the form ∂_{H}(t) denotes the process that behaves the same as the process denoted by t, except that actions from H are blocked.
Axioms of ACP
In other presentations of ACP, γ(a,b) is regularly replaced by a∣b in CM5–CM7. By CM12, which is more often called CF, these replacements give rise to an equivalent axiomatization. In other presentations of ACP, CM10 and CM11 are usually absent. These equations are not derivable from the other axioms, but all there closed substitution instances are derivable from the other axioms. Moreover, CM10 and CM11 hold in virtually all models of ACP that have been devised.
In the sequel, we will use the sum notation \({\sum }_{i<n} t_{i}\). For each \(i \in \mathbb {N}\), let t_{i} be a term of ACP or an extension of ACP . Then \({\sum }_{i<0} t_{i} = \delta \) and, for each \(n \in \mathbb {N}_1\),^{1} the term \({\sum }_{i<n} t_{i}\) is defined by induction on n as follows: \({\sum }_{i<1} t_{i} = t_{0}\) and \({\sum }_{i<n + 1} t_{i} ={\sum }_{i<n} t_{i} {+} t_{n}\).
2.2 Guarded Recursion
A closed ACP term denotes a process with a finite upper bound to the number of actions that it can perform. Guarded recursion allows the description of processes without a finite upper bound to the number of actions that it can perform.
Let T be ACP or a concrete extensions of ACP,^{2} and let t be a T term containing a variable X. Then an occurrence of X in t is guarded if t has a subterm of the form a ⋅ t^{′} where a ∈A and t^{′} is a T term containing this occurrence of X.
Let T be ACP or a concrete extension of ACP. Then a T term t is a guarded T term if all occurrences of variables in t are guarded.
Let T be ACP or a concrete extension of ACP. Then a guarded recursive specification over T is a finite or countably infinite set of recursion equations E = {X = t_{X}∣X ∈ V }, where V is a set of variables and each t_{X} is either a guarded T term in which variables other than the variables from V do not occur or a T term rewritable to such a term using the axioms of T in either direction and/or the equations in E, except the equation X = t_{X}, from left to right. We write V(E) for the set of all variables that occur in E. A solution of E in some model of T is a set {P_{X}∣X ∈V(E)} of elements of the carrier of that model such that the equations of E hold if, for all X ∈V(E), X is assigned P_{X}. We are only interested models of ACP and concrete extensions of ACP in which guarded recursive specifications have unique solutions.
Axioms for guarded recursion
〈XE〉 = 〈t_{X}E〉  ifX = t_{X} ∈ E  RDP 
E ⇒ X = 〈XE〉  ifX ∈V(E)  RSP 
The equations 〈XE〉 = 〈t_{X}E〉 for a fixed E express that the constants 〈XE〉 make up a solution of E. The conditional equations E ⇒ X = 〈XE〉 express that this solution is the only one.
In extensions of ACP whose axioms include RSP, we have to deal with conditional equational formulas with a countably infinite number of premises. Therefore, infinitary conditional equational logic is used in deriving equations from the axioms of extensions of ACP whose axioms include RSP. A complete inference system for infinitary conditional equational logic can be found in, for example, [15]. It is noteworthy that derivations are allowed to be of countably infinite length in infinitary conditional equational logic.
2.3 Some Results about Guarded Recursion
This section is concerned with legitimate ways of manipulating guarded recursive specifications and with guarded terms of a special form.
Let T be ACP or a concrete extension of ACP. Then, each guarded recursive specification over T can be manipulated in several ways that are justified by RDP and RSP.
Proposition 1 (Manipulation)
 (1)
if Y = t_{Y} ∈ E and \(t_{Y} = t^{\prime }_{Y}\) isderivable from the axioms of T, then\(\langle X \vert E \rangle = \langle X \vert (E \setminus \nolinebreak [4]\left \{ Y = t_{Y} \right \}) \cup \left \{ Y = t^{\prime }_{Y} \right \} \rangle \) isderivable from the axioms of T, RDP and RSP;
 (2)
if Y = t_{Y} ∈ E,Z = t_{Z} ∈ E,and \(t^{\prime }_{Y}\) ist_{Y} with some occurrence of Z in t_{Y} replaced by t_{Z},then \(\langle X \vert E \rangle = \langle X \vert (E \setminus \left \{ Y = t_{Y} \right \}) \cup \left \{ Y = t^{\prime }_{Y} \right \} \rangle \) isderivable from the axioms of T, RDP and RSP;
 (3)
if Y ∉V(E) and t_{Y} is a guarded T term in which variables other than the variables from V(E) do not occur, then 〈XE〉 = 〈XE ∪{Y = t_{Y}}〉 is derivable from the axioms of T, RDP and RSP.
Proof 1
In case (1), first we apply RDP for each recursion equation in E, next we apply \(t_{Y} = t^{\prime }_{Y}\) to 〈Y E〉 = 〈t_{Y}E〉, and finally we apply RSP to the resulting set of equations. In case (2), first we apply RDP for each recursion equation in E, next we apply 〈ZE〉 = 〈t_{Z}E〉 to 〈Y E〉 = 〈t_{Y}E〉, and finally we apply RSP to the resulting set of equations. In case (3), we first apply RDP for each recursion equation in E ∪{Y = t_{Y}} and then we apply RSP to the resulting set of equations.^{3} □
Proposition 1 will be used in the proof of Theorem 1 in Section 3.2.

δ ∈HNF;

if a ∈A, then a ∈HNF;

if a ∈A and t is a T term, then a ⋅ t ∈HNF;

if t,t^{′}∈HNF, then t + t^{′}∈HNF.
It is wellknown that each guarded ACP_{rec} term is derivably equal to a head normal form of ACP_{rec} (see also Lemma 2.4.7 in [5]).
Proposition 2 (Head normal form)
For each guarded ACP_{rec}term t, there exists a head normal form t^{′} of ACP such that t = t^{′} is derivable from the axioms of ACP_{rec}.
Proof 2
The proof is analogous to the proof of Proposition 3 in Section 3.2. □
3 Strategic Interleaving
In this section, we extend ACP with strategic interleaving, i.e. interleaving according to some interleaving strategy. Interleaving strategies are abstractions of scheduling algorithms. Interleaving according to some interleaving strategy is what really happens in the case of multithreading as found in contemporary programming languages.
3.1 ACP with Strategic Interleaving
In the extension of ACP with strategic interleaving presented below, it is expected that an interleaving strategy uses the interleaving history in one way or another to make processscheduling decisions.

\({\langle \rangle } \in \mathcal {H}\);

if i ≤ n, then \(\left (i,n \right ) \in \mathcal {H}\);

Open image in new window j ≤ n, and n − 1 ≤ m ≤ n + 1, then h ↷ (i,n) ↷ (j,m) ∈. ^{4}
The presented extension of ACP is called ACP + SI (ACP with Strategic Interleaving). It covers a generic interleaving strategy that can be instantiated with different specific interleaving strategies that can be represented in the way that is explained below.

a fixed but arbitrary set S;

for each \(n \in \mathbb {N}_1\), a fixed but arbitrary function \(\sigma _{n} {:} \mathcal {H} \times S \to \left \{ 1,\ldots ,n \right \}\);

for each \(n \in \mathbb {N}_1\), a fixed but arbitrary function \(\vartheta _{n} {:} \mathcal {H} \times S \times \left \{ 1,\ldots ,n \right \} \times \mathsf {A} \to S\).

the control states from S encode data that are relevant to the interleaving strategy, but not derivable from the interleaving history;

if σ_{n}(h,s) = i, then the i th process gets the next turn after interleaving history h in control state s;

if 𝜗_{n}(h,s,i,a) = s^{′}, then s^{′} is the control state that arises from the i th process doing a after interleaving history h in control state s.
In ACP + SI, it is also assumed that a fixed but arbitrary set D of data and a fixed but arbitrary function ϕ:D → P, where P is the set of all closed terms over the signature of ACP + SI (given below), have been given and that, for each d ∈ D and a,b ∈A, \(\mathsf {cr}(d),\overline {\mathsf {cr}}(d) \in \mathsf {A}\), γ(cr(d),a) = δ, and γ(a,b)≠cr(d). The action cr(d) can be considered a process creation request and the action \(\overline {\mathsf {cr}}(d)\) can be considered a process creation act. They represent the request to start the process denoted by ϕ(d) in parallel with the requesting process and the act of carrying out that request, respectively.

for each \(n \in \mathbb {N}_1\), \(h \in \mathcal {H}\), and s ∈ S, the nary strategic interleaving operator \(\parallel ^{n}_{h,s}\);

for each \(n,i \in \mathbb {N}_1\) with i ≤ n, \(h \in \mathcal {H}\), and s ∈ S, the nary positional strategic interleaving operator Open image in new window .

a closed term of the form \(\parallel ^{n}_{h,s}(t_{1},\ldots ,t_{n})\) denotes the process that results from interleaving of the n processes denoted by t_{1},…,t_{n} after interleaving history h in control state s, according to the interleaving strategy represented by S, \({\left \langle \sigma _{n} \right \rangle }_{n \in \mathbb {N}_1}\), and \({\left \langle \vartheta _{n} \right \rangle }_{n \in \mathbb {N}_1}\).
Axioms for strategic interleaving
Alternative axioms for SI2
In (ACP + SI)_{rec}, i.e. ACP + SI extended with guarded recursion in the way described in Section 2, the processes that can be created are restricted to the ones denotable by a closed ACP + SI term. This restriction stems from the requirement that ϕ is a function from D to the set of all closed ACP + SI terms. The restriction can be removed by relaxing this requirement to the requirement that ϕ is a function from D to the set of all closed (ACP + SI)_{rec} terms. We write (ACP + SI)\(_{\text {rec}}^{+}\) for the theory resulting from this relaxation. In other words, (ACP + SI)\(_{\text {rec}}^{+}\) differs from (ACP + SI)_{rec} in that it is assumed that a fixed but arbitrary function ϕ : D → P, where P is the set of all closed terms over the signature of (ACP + SI)_{rec}, has been given.
It is customary to associate transition systems with closed terms of the language of an ACPlike theory of processes by means of structural operational semantics and to use this to construct a model in which closed terms are identified if their associated transition systems are bisimilar. The structural operational semantics of ACP can be found in [5, 13]. The additional transition rules for the strategic interleaving operators and the positional strategic interleaving operators are given in Appendix A.
3.2 Basic Properties of ACP with Strategic Interleaving
In this section, the subject of concern is the connection between ACP and ACP + SI. The main results are an elimination result and a conservative extension result. We begin with establishing some results that will be used in the proof of those main results.
Each guarded ACP + SI term is derivably equal to a head normal form of ACP + SI.
Proposition 3 (Head normal form)
For each guarded ACP + SIterm t, there exists a head normal formt^{′} of ACP + SIsuch thatt = t^{′} is derivable from the axioms of ACP + SI.
Proof 3
The proof is straightforward by induction on the structure of t. The case where t is of the form δ and the case where t is of the form a (a ∈A) are trivial. The case where t is of the form t_{1} ⋅ t_{2} follows immediately from the induction hypothesis and the claim that, for all head normal forms t_{1} and t_{2} of ACP + SI, there exists a head normal form t^{′} of ACP + SI such that t_{1} ⋅ t_{2} = t^{′} is derivable from the axioms of ACP + SI. This claim is easily proved by induction on the structure of t_{1}. The case where t is of the form t_{1} + t_{2} follows immediately from the induction hypothesis. The cases where t is of one of the forms Open image in new window are proved along the same lines as the case where t is of the form t_{1} ⋅ t_{2}. In the case that t is of the form t_{1} ∣ t_{2}, each of the cases to be considered in the inductive proof of the claim demands a proof by induction on the structure of t_{2}. In the case that t is of the form Open image in new window the claim is of course proved by induction on the structure of t_{i} instead of t_{1}. The case that t is of the form t_{1} ∥ t_{2} follows immediately from the case that t is of the form Open image in new window and the case that t is of the form t_{1}  t_{2}. The case that t is of the form \(\parallel ^{n}_{h,s}{(t_1,\ldots ,t_n)}\) follows immediately from the case that t is of the form Open image in new window . Because t is a guarded ACP+SI term, the case where t is a variable cannot occur. □
Each of the four theorems to come refer to several process algebras. It is implicit that the same set A of actions and the same communication function γ are assumed in the process algebras referred to.
Each guarded recursive specification over ACP + SI can be reduced to a guarded recursive specification over ACP.
Theorem 1 (Reduction)
For each guarded recursive specification E over ACP + SI and eachX ∈V(E), there exists a guarded recursive specificationE^{′} over ACP such that 〈XE〉 = 〈XE^{′}〉 is derivable from the axioms of ( ACP + SI)\(_{\text {rec}}^{+}\).
Proof 4
Let E be a guarded recursive specification over ACP + SI. Assume that, for each equation X = t_{X} from E, t_{X} is a guarded ACP + SI term. It follows from Proposition 1 that this assumption does not lead to loss of generality.
Let X = t_{X} be an equation from E. Now, by Proposition 3, there exist \(n,m \in \mathbb {N}\) such that, for each \(i \in \mathbb {N}\) with i < n and \(j \in \mathbb {N}\) with j < m, there exist an a_{i} ∈A, an ACP + SI term t_{i}, and a b_{j} ∈A such that \(t_{X} = {\sum }_{i<n} a_{i} \cdot t_{i} {+} {\sum }_{j<m} b_{j}\) is derivable from the axioms of ACP+SI. For each \(i \in \mathbb {N}\) with i < n, let \(t^{\prime }_{i}\) be t_{i} with, for each equation Y = t_{Y} from E, each unguarded occurrence of Y in t_{i} replaced by the guarded ACP + SI term t_{Y}. For each \(i \in \mathbb {N}\) with i < n, by its construction, the term \(t^{\prime }_{i}\) is a guarded ACP + SI terms in which variables other than the ones from V(E) do not occur. Now, by Proposition 1, the equation \(X_{i} = t^{\prime }_{i}\), where X_{i} is a fresh variable, can be added to E for each \(i \in \mathbb {N}\) with i < n and the equation X = t_{X} can be replaced by the equation \(X = {\sum }_{i<n} a_{i} \cdot X_{i} {+} {\sum }_{j<m} b_{j}\) in E. The other equations from E can be replaced by a set of equations in the same way as the equation X = t_{X}.
The set of equations so obtained can be manipulated following the same procedure as in the case of E, but the manipulation can be restricted to the added equations. Repeating this procedure, perhaps countably infinitely many times, we obtain a guarded recursive specification E^{′} over ACP for which 〈XE〉 = 〈XE^{′}〉 is derivable from the axioms of (ACP+SI)\(_{\text {rec}}^{+}\). □
The next three theorems will be proved by means of term rewriting systems. In Appendix B, basic definitions and results regarding term rewriting systems are collected. This appendix also serves to fix the terminology on term rewriting systems used in the proofs of the next three theorems.
Each closed (ACP+SI)\(_{\text {rec}}^{+}\) term is derivably equal to a closed ACP_{rec} term.
Theorem 2 (Elimination)
For each closed ( ACP + SI)\(_{\text {rec}}^{+}\) term t, there exists a closed ACP_{rec} term t^{′} such that t = t^{′} is derivable from the axioms of ( ACP + SI)\(_{\text {rec}}^{+}\).
Proof 5
We prove this by means of a term rewriting system that takes equational axioms of (ACP+SI)\(_{\text {rec}}^{+}\) and equations derivable from the axioms of (ACP+SI)\(_{\text {rec}}^{+}\) as rewrite rules. Thus, the proof boils down to showing that (a) the term rewriting system concerned has the property that each (ACP+SI)\(_{\text {rec}}^{+}\) term has a unique normal form modulo axioms A1 and A2 and (b) each closed (ACP+SI)\(_{\text {rec}}^{+}\) term that is a normal form modulo axioms A1 and A2 is a closed ACP_{rec} term. Henceforth, we will write AC for the set of equations that consists of axioms A1 and A2.
Let R be a set of equations that contains for each guarded recursive specification E over ACP + SI and X ∈V(E) an equation 〈XE〉 = 〈XE^{′}〉, where E^{′} is a guarded recursive specification over ACP, that is derivable from the axioms of (ACP + SI)\(_{\text {rec}}^{+}\). Such a set R exists by Theorem 1. Consider the term rewriting system \(\mathcal {R}((\text {ACP}+\text {SI})_{\text {rec}}^{+})\) that consists of the axioms of (ACP + SI)\(_{\text {rec}}^{+}\), with the exception of A1, A2, RDP, and RSP, and the equations from R taken as rewrite rules.
We show that \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) has the property that each (ACP + SI)\(_{\text {rec}}^{+}\) term has a unique normal form modulo AC by proving that \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+})\) is terminating modulo AC and confluent modulo AC.
where it is assumed that, for each variable X over processes, X is a variable over integers. The following is easy to see: (a) t > t^{′} for all rewrite rules t = t^{′} of \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) and (b) t > t^{′} implies s > s^{′} for all (ACP + SI)\(_{\text {rec}}^{+}\) terms s and s^{′} for which t = s and t^{′} = s^{′} are derivable from AC.^{7} Hence, \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) is terminating modulo AC.
Next, we show that \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) is confluent modulo AC. It follows from Theorems 5 and 16 in [20] and the fact that \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) is terminating modulo AC that \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) is confluent modulo AC if it does not give rise to critical pairs modulo AC that are not convergent. It is easy to see that all critical pairs modulo AC arise from overlappings of (a) A3 on A4, CM4, CM8, CM9, D3, and SI8, (b) A6 on A4, CM4, CM8, CM9, D3, and SI8, (c) A7 on CM3, CM5, CM6, CM7, D4, and SI5, (d) CM10 on CM9, and (e) CM11 on CM8. It is straightforward to check that all critical pairs concerned are convergent. Hence, \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) is confluent modulo AC.
Above, we have shown that \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) is terminating modulo AC and confluent modulo AC and by this that it has the property that each (ACP + SI)\(_{\text {rec}}^{+}\) term has a unique normal form modulo AC. It remains to be shown that each closed (ACP + SI)\(_{\text {rec}}^{+}\) term that is a normal form modulo AC is a closed ACP_{rec} term. It is not hard to see that, for each closed (ACP + SI)\(_{\text {rec}}^{+}\) term in which other operators than + and ⋅ occur, a reduction step modulo AC is still possible in \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)). Because a reduction step modulo AC is impossible for a normal form modulo AC, no other operators than + or ⋅ can occur in a closed (ACP + SI)\(_{\text {rec}}^{+}\) term that is a normal form modulo AC. Hence, each closed (ACP + SI)\(_{\text {rec}}^{+}\) term that is a normal form modulo AC is a closed ACP_{rec} term. □
Each equation between closed ACP terms that is derivable in ACP + SI is also derivable in ACP.
Theorem 3 (Conservative extension)
For each two closed ACP terms t andt^{′},t = t^{′} is derivable from the axioms of ACP + SI only ift = t^{′} is derivable from the axioms of ACP.
Proof 6
We prove this by means of a restriction of the term rewriting system from the proof of Theorem 2. Consider the term rewriting system \(\mathcal {R}\)(ACP + SI) that consists of the axioms of ACP + SI, with the exception of A1 and A2. \(\mathcal {R}\)(ACP + SI) is \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) restricted to ACP + SI terms. Just like \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)), \(\mathcal {R}\)(ACP + SI) is terminating modulo AC and confluent modulo AC. The proofs of these properties for \(\mathcal {R}\)((ACP + SI)\(_{\text {rec}}^{+}\)) carry over to \(\mathcal {R}\)(ACP + SI).
Let t and t^{′} be two closed ACP terms such that t = t^{′} is derivable from the axioms of ACP + SI. Reduce t and t^{′} to normal forms s and s^{′}, respectively, by means of the term rewriting system \(\mathcal {R}\)(ACP + SI). By Theorem 5 in [20], being confluent modulo AC is equivalent to being ChurchRosser modulo AC for a term rewriting system that is terminating modulo AC. This means that t and t^{′} have the same normal form modulo AC. In other words, s = s^{′} is derivable from axioms A1 and A2. Because (a) no other operators than + and ⋅ occur in t and t^{′} and (b) no rewrite rule introduces one or more of the other operators if one or more of the other operators was not already in its lefthand side, each rewrite rule applied in the reduction from t to s or the reduction from t^{′} to s^{′} is one of the axioms of ACP. Therefore, each rewrite rule involved in the reduction from t to s or the reduction from t^{′} to s^{′} is an axiom of ACP. Hence, the reduction from t to s shows that t = s is derivable from the axioms of ACP and the reduction from t^{′} to s^{′} shows that t^{′} = s^{′} is derivable from the axioms of ACP. From this and the fact that s = s^{′} is derivable from axioms A1 and A2, it follows t = t^{′} is derivable from the axioms of ACP. □
The following theorem concerns the expansion of minimal models of ACP to models of ACP + SI.
Theorem 4 (Unique expansion)
Each minimal model of ACP has a unique expansion to a model of ACP + SI.
Proof 7
We write \(f^{\mathcal {A}}\), where \(\mathcal {A}\) is a model of ACP or ACP + SI and f is a constant or operator from the signature of \(\mathcal {A}\), for the interpretation of f in \(\mathcal {A}\). We write \(t^{\mathcal {A}}\), where \(\mathcal {A}\) is a model of ACP or ACP + SI and t is a closed term over the signature of \(\mathcal {A}\), for the interpretation of t in \(\mathcal {A}\).
Let \(\mathcal {A}\) be a minimal model of ACP. Let CT be a function from the carrier of \(\mathcal {A}\) to the set of all closed ACP terms such that, for each element p of the carrier of \(\mathcal {A}\), \(\mathit {CT}(p)^{\mathcal {A}} = p\). Because \(\mathcal {A}\) is a minimal model of ACP, CT(p) is a total function. We write \(\underline {p}\), where p is an element of the carrier of \(\mathcal {A}\), for CT(p). Let NF be a function from the set of all closed ACP + SI terms to the set of all closed ACP terms such that, for each closed ACP + SI term t, NF(t) is one of the normal forms that t can be reduced to by means of the term rewriting system \(\mathcal {R}\)(ACP + SI) from the proof of Theorem 3.
for all p_{1},…,p_{n} from the carrier of \(\mathcal {A}\).

for all closed substitution instances t = t^{′} of SI1–SI8, \(t^{\mathcal {B}} = {\mathit {NF}(t)}^{\mathcal {A}}\);

for all closed substitution instances t = t^{′} of SI1–SI8, \(t^{\prime \mathcal {B}} = {\mathit {NF}(t^{\prime })}^{\mathcal {A}}\);

for all closed substitution instances t = t^{′} of SI1–SI8, \(\mathit {NF}(t)^{\mathcal {A}} = \mathit {NF}(t^{\prime })^{\mathcal {A}}\).
We still have to prove that \(\mathcal {B}\) is the only expansion of \(\mathcal {A}\) to a model of ACP + SI. We can prove this by contradiction. Assume that \(\mathcal {C}\) is an expansion of \(\mathcal {A}\) to a model of ACP + SI that differs from \(\mathcal {B}\). Then at least one of the additional operators of ACP + SI has different interpretations in \(\mathcal {B}\) and \(\mathcal {C}\). By the definitions of the interpretations of the additional operators of ACP + SI in \(\mathcal {B}\), this means that there exists a closed ACP + SI term t such that \(t^{\mathcal {C}} \neq \mathit {NF}(t)^{\mathcal {A}}\). Moreover, because because t = NF(t) is derivable from the axioms of ACP + SI, \(t^{\mathcal {C}} = \mathit {NF}(t)^{\mathcal {C}}\). Hence, \(\mathit {NF}(t)^{\mathcal {C}} \neq \mathit {NF}(t)^{\mathcal {A}}\). Because NF(t) is a closed ACP term, this contradicts the fact that \(\mathcal {C}\) is an expansion of \(\mathcal {A}\). □
4 Concluding Remarks
We have extended the algebraic theory of processes known as ACP with the form of interleaving that underlies multithreading as found in contemporary programming languages. We have also established some basic properties of the resulting theory. It remains an open question whether strategic interleaving is definable in an established extension of ACP.
Footnotes
 1.
We write \(\mathbb {N}_1\) for the set \(\left \{ n \in \mathbb {N} \mid n \geq 1 \right \}\) of positive natural numbers.
 2.
A concrete extension of ACP is an extension of ACP that does not offer the possibility of abstraction from certain actions. All extensions of ACP introduced in this paper are concrete extensions.
 3.
Further details on cases (1) and (2) can be found in the proof of Theorem 4.3.2 from [13].
 4.
We write 〈〉 for the empty sequence, d for the sequence having d as sole element, and Open image in new window for the concatenation of sequences α and α^{′}. We assume that the usual identities, such as 〈 〉↷ α = α Open image in new window and Open image in new window , hold.
 5.
In [8], various examples of interleaving strategies are given in the setting of the relatively unknown thread algebra. The representation of the more serious of these examples in the current setting demands nontrivial use of the control state.
 6.
Here, extended polynomials differ from polynomials in that both variables and expressions of the form 2^{X}, where X is a variable, are allowed where only variables are allowed in polynomials.
 7.
We do not have that t > t^{′} for all rewrite rules t = s if SI2 is replaced by SI2a and SI2b (see Table 4).
 8.
See e.g. Definition 10 in [20] for the definitions of most general unifier and complete set of unifiers modulo E.
Notes
Acknowledgements
We thank an anonymous referee for carefully reading a preliminary version of this paper, for pointing out an error in one of the proofs, and for suggesting improvements of the presentation.
References
 1.America, P., de Bakker, J.W.: Designing equivalent semantic models for process creation. Theor. Comput. Sci. 60(2), 109–176 (1988)MathSciNetCrossRefMATHGoogle Scholar
 2.Baeten, J.C.M., Bergstra, J.A.: Real space process algebra. Form. Asp. Comput. 5(6), 481–529 (1993)CrossRefMATHGoogle Scholar
 3.Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Monographs in Theoretical Computer Science, an EATCS Series. Springer, Berlin (2002)Google Scholar
 4.Baeten, J.C.M., Vaandrager, F.W.: An algebra of process creation. Acta Informatica 29(4), 303–334 (1992)MathSciNetCrossRefMATHGoogle Scholar
 5.Baeten, J.C.M., Weijland, W.P.: Process Algebra Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)Google Scholar
 6.Bergstra, J.A.: A process creation mechanism in process algebra. In: Baeten, J.C.M. (ed.) Applications of Process Algebra, Cambridge Tracts in Theoretical Computer Science, vol. 17, pp 81–88. Cambridge University Press, Cambridge (1990)Google Scholar
 7.Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control. 60(1–3), 109–137 (1984)MathSciNetCrossRefMATHGoogle Scholar
 8.Bergstra, J.A., Middelburg, C.A.: Thread algebra for strategic interleaving. Form. Asp. Comput. 19(4), 445–474 (2007)CrossRefMATHGoogle Scholar
 9.Bergstra, J.A., Middelburg, C.A.: A thread algebra with multilevel strategic interleaving. Theory Comput. Syst. 41(1), 3–32 (2007)MathSciNetCrossRefMATHGoogle Scholar
 10.Bergstra, J.A., Middelburg, C.A.: Distributed strategic interleaving with load balancing. Futur. Gener. Comput. Syst. 24(6), 530–548 (2008)CrossRefGoogle Scholar
 11.Bergstra, J.A., Middelburg, C.A., Usenko, Y.S.: Discrete time process algebra and the semantics of SDL. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp 1209–1268. Elsevier, Amsterdam (2001)Google Scholar
 12.Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)MathSciNetCrossRefMATHGoogle Scholar
 13.Fokkink, W.J.: Introduction to Process Algebra. Texts in Theoretical Computer Science, an EATCS Series. Springer, Berlin (2000)Google Scholar
 14.Gehrke, T., Rensink, A.: Process creation and full sequential composition in a namepassing calculus. Electron. Notes Theor. Comput. Sci. 7, 141–160 (1997)MathSciNetCrossRefMATHGoogle Scholar
 15.van Glabbeek, R.J., Vaandrager, F.W.: Modular specification of process algebras. Theor. Comput. Sci. 113(2), 293–348 (1993)MathSciNetCrossRefMATHGoogle Scholar
 16.Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. AddisonWesley, Reading (2000)MATHGoogle Scholar
 17.Hejlsberg, A., Wiltamuth, S., Golde, P.: C# Language Specification. AddisonWesley, Reading (2003)Google Scholar
 18.Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)CrossRefMATHGoogle Scholar
 19.Hoare, C.A.R.: Communicating Sequential Processes. PrenticeHall, Englewood Cliffs (1985)MATHGoogle Scholar
 20.Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)MathSciNetCrossRefMATHGoogle Scholar
 21.Milner, R.: Communication and Concurrency. PrenticeHall, Englewood Cliffs (1989)MATHGoogle Scholar
 22.Sabelfeld, A., Sands, D.: Probabilistic noninterference for multithreaded programs. In: Computer Security Foundations Workshop 2000, pp 200–214. IEEE Computer Society Press (2000)Google Scholar
Copyright information
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.