J A Bergstra

C A Middelburg

Under consideration for publication in Formal Aspects of Computing Thread algebra for poly-threading

Keywords: poly-threading, thread algebra, process algebra, execution architecture, non-distributed multi-threading, distributed multi-threading

Thread algebra for poly-threading

Introduction

In [START_REF] Bergstra | Thread extraction for polyadic instruction sequences[END_REF], we considered fragmentation of sequential programs that take the form of instruction sequences in the setting of program algebra [START_REF] Bergstra | Program algebra for sequential code[END_REF]. The objective of the current paper is to develop a theory of the behaviours exhibited by sequential programs on execution that covers the case where the programs have been split into fragments. It is a fact of life that sequential programs are often fragmented. An important reason for fragmentation of programs is that the execution architecture at hand to execute them sets bounds to the size of programs. In [START_REF] Bergstra | Program algebra for sequential code[END_REF], a start was made with a line of research in which sequential programs that take the form of instruction sequences and the behaviours exhibited by sequential programs on execution are investigated (see e.g. [START_REF] Bergstra | Decision problems for pushdown threads[END_REF][START_REF] Bergstra | Instruction sequences with indirect jumps[END_REF][START_REF] Ponse | An introduction to program and thread algebra[END_REF]). In this line of research, the view is taken that the behaviour exhibited by a sequential program on execution takes the form of a thread as considered in basic thread algebra [START_REF] Bergstra | Program algebra for sequential code[END_REF]. 1 With the current paper, we carry on this line of research. Therefore, we consider program fragment behaviours that take the form of threads as considered in basic thread algebra.

We extend basic thread algebra with the barest mechanism for sequencing of threads that are taken for program fragment behaviours. This mechanism is called poly-threading. Poly-threading is the counterpart of program overlaying [START_REF] Pankhurst | Program overlay techniques[END_REF] at the level of threads. Until virtual memory was implemented in mainstream operating systems, program overlaying was commonly used in many applications to deal with the prevailing constraints on the size of programs (see e.g. [START_REF] Stubblefield | A main program and overlay manager subsystem within a distributed function laboratory computer system[END_REF][START_REF] Carlow | Architecture of the space shuttle primary avionics software system[END_REF]). In embedded systems, it is usually important to use memory efficiently. However, many embedded systems are real-time systems and the use of virtual memory makes it insufficiently predictable whether a real-time system meets the deadlines set for it. Therefore, program overlaying is still popular in embedded systems (see e.g. [START_REF] Che | Compilation of stream programs for multicore processors that incorporate scratchpad memories[END_REF]). Moreover, with the advent of multi-core processors, there seems to be a renewed interest in program overlaying in the area of operating systems (see e.g. [M + 05]). It happens that in computer science since the introduction of program overlaying more than forty years ago no serious attention has been paid to the explanation of program overlaying at a semantic level. This state of affairs forms our motivation to have a closer look at program overlaying at the level of program behaviours.

Inherent in the behaviour exhibited by a program on execution is that it does certain steps for the purpose of interacting with some service provided by an execution environment. In the setting of thread algebra, the use mechanism is introduced in [START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF] to allow for this kind of interaction. Poly-threading supports the initialization of one of the services used every time a thread is started up. With poly-threading, a thread selection is made whenever a thread ends up with the intent to achieve the start-up of another thread. That thread selection can be made in two ways: by the terminating thread or externally. We show how thread selections of the latter kind can be internalized.

Both thread and service look to be special cases of a more general notion of process. Therefore, it is interesting to know how threads and services as considered in the extension of basic thread algebra with poly-threading relate to processes as considered in theories about concurrent processes such as ACP [START_REF] Baeten | Process Algebra[END_REF], CCS [START_REF] Milner | Communication and Concurrency[END_REF] and CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF].

We show that threads and services as considered in the extension of basic thread algebra with poly-threading introduced in this paper can be viewed as processes that are definable over ACP. Because ACP is much better known, this may be helpful in forming a better idea of the extension of basic thread algebra with poly-threading.

An analytic execution architecture is a model of a hypothetical execution environment for sequential programs that is designed for the purpose of explaining how a program may be executed. The notion of analytic execution architecture defined in [START_REF] Bergstra | Execution architectures for program algebra[END_REF] is suited to sequential programs that have not been split into fragments. We use the extension of basic thread algebra with poly-threading to describe analytic execution architectures suited to sequential programs that have been split into fragments.

In systems resulting from contemporary programming, we find non-distributed and distributed multi-threading and threads that are program fragment behaviours, the latter primarily by the advent of multi-core processors (see e.g. [START_REF] Che | Compilation of stream programs for multicore processors that incorporate scratchpad memories[END_REF]). For that reason, it is interesting to combine the theories of non-distributed and distributed strategic interleaving developed in [START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF] and [START_REF] Bergstra | Distributed strategic interleaving with load balancing[END_REF], respectively, with the extension of basic thread algebra with polythreading. We take up the combination by introducing poly-threading covering variations of the simplest form of interleaving for non-distributed and distributed multi-threading considered in [START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF][START_REF] Bergstra | Distributed strategic interleaving with load balancing[END_REF].

The line of research carried on in this paper has two main themes: the theme of instruction sequences and the theme of threads. Both [START_REF] Bergstra | Thread extraction for polyadic instruction sequences[END_REF] and the current paper are concerned with program fragmentation, but [START_REF] Bergstra | Thread extraction for polyadic instruction sequences[END_REF] elaborates on the theme of instruction sequences and the current paper elaborates on the theme of threads. It happens that there are aspects of program fragmentation that can be dealt with at the level of instruction sequences, but cannot be dealt with at the level of threads. In particular, the ability to replace special instructions in an instruction sequence fragment by different ordinary instructions every time execution is switched over to that fragment cannot be dealt with at the level of threads. Threads, which are intended for explaining the meaning of sequential programs, turn out to be too abstract to deal with program fragmentation in full. This paper is organized as follows. First, we review basic thread algebra and the use mechanism (Sections 2 and 3).

Next, we extend basic thread algebra with poly-threading and show how external thread selections in poly-threading can be internalized (Sections 4 and 5). Following this, we review ACP and relate the extension of basic thread algebra with poly-threading to ACP (Sections 6 and 7). Then, we discuss analytic execution architectures suited for programs that have been fragmented (Section 8). After that, we introduce forms of interleaving suited for non-distributed and distributed multi-threading that cover poly-threading (Sections 9, 10 and 11). Finally, we make some concluding remarks (Section 12).

Up to and including Section 8, this paper is a revision of [START_REF] Bergstra | Thread algebra for sequential poly-threading[END_REF]. In that paper, the term "sequential polythreading" stands for "poly-threading in a setting where multi-threading or any other form of concurrency is absent".

We conclude in hindsight that the use of this term is unfortunate and do not use it in the current paper.

Basic thread algebra

In this section, we review BTA, a form of process algebra which is tailored to the description of the behaviour of deterministic sequential programs under execution. The behaviours concerned are called threads.

In BTA, it is assumed that there is a fixed but arbitrary finite set of basic actions A with tau ∈ A. We write A tau for A ∪ {tau}. The members of A tau are referred to as actions.

The intuition is that each basic action performed by a thread is taken as a command to be processed by a service provided by the execution environment of the thread. The processing of a command may involve a change of state of the service concerned. At completion of the processing of the command, the service produces a reply value. This reply is either T or F and is returned to the thread concerned.

Although BTA is one-sorted, we make this sort explicit. The reason for this is that we will extend BTA with additional sorts in Sections 3 and 4.

X|E = t X |E if X = t X ∈ E RDP E ⇒ X = X|E if X ∈ V(E) R S P
The algebraic theory BTA has one sort: the sort T of threads. To build terms of sort T, BTA has the following constants and operators:

• the deadlock constant D : T;

• the termination constant S : T;

• for each a ∈ A tau , the postconditional composition operator a : T × T → T.

Terms of sort T are built as usual (see e.g. [START_REF] Sannella | Algebraic preliminaries[END_REF][START_REF] Wirsing | Algebraic specification[END_REF]). Throughout the paper, we assume that there are infinitely many variables of sort T, including x, y, z.

We introduce action prefixing as an abbreviation: a • p, where p is a term of sort T, abbreviates p a p.

Let p and q be closed terms of sort T and a ∈ A tau . Then p a q will perform action a, and after that proceed as p if the processing of a leads to the reply T (called a positive reply), and proceed as q if the processing of a leads to the reply F (called a negative reply). The action tau plays a special role. It is a concrete internal action: performing tau will never lead to a state change and always lead to a positive reply, but notwithstanding all that its presence matters.

BTA has only one axiom. This axiom is given in Table 1. Using the abbreviation introduced above, axiom T1 can be written as follows:

x tau y = tau • x.
Each closed BTA term of sort T denotes a finite thread, i.e. a thread of which the length of the sequences of actions that it can perform is bounded. Guarded recursive specifications give rise to infinite threads.

A guarded recursive specification over BTA is a set of recursion equations

E = {X = t X | X ∈ V }, where V is
a set of variables of sort T and each t X is a term of the form D, S or t a t with t and t BTA terms of sort T that contain only variables from V . We write V(E) for the set of all variables that occur on the left-hand side of an equation in E. We are only interested in models of BTA in which guarded recursive specifications have unique solutions, such as the projective limit model of BTA presented in [START_REF] Bergstra | Polarized process algebra and program equivalence[END_REF]. A thread that is the solution of a finite guarded recursive specification over BTA is called a finite-state thread.

We extend BTA with guarded recursion by adding constants for solutions of guarded recursive specifications and axioms concerning these additional constants. For each guarded recursive specification E and each X ∈ V(E), we add a constant of sort T standing for the unique solution of E for X to the constants of BTA. The constant standing for the unique solution of E for X is denoted by X|E . Moreover, we add the axioms for guarded recursion given in We will write BTA+REC for BTA extended with the constants for solutions of guarded recursive specifications and axioms RDP and RSP.

Interaction of threads with services

A thread may perform certain basic actions only for the sake of having itself affected by some service. When processing a basic action performed by a thread, a service affects that thread by returning a reply value to the thread at completion of the processing of the basic action. In this section, we introduce the use mechanism, which is concerned with this kind of interaction between threads and services. 3It is assumed that there is a fixed but arbitrary finite set F of foci and a fixed but arbitrary finite set M of methods.

Each focus plays the role of a name of a service provided by the execution environment that can be requested to process a command. Each method plays the role of a command proper. For the set A of basic actions, we take the set

{f.m | f ∈ F, m ∈ M}.
A thread performing a basic action f.m is considered to make a request to a service that is known to the thread under the name f to process command m.

We introduce yet another sort: the sort S of services. However, we will not introduce constants and operators to build terms of this sort. S is considered to stand for the set of all services. We identify services with functions H : M + → {T, F, B} that satisfy the following condition:

∀ρ ∈ M + , m ∈ M • (H(ρ) = B ⇒ H(ρ m ) = B) . 4
B stands for blocked. It is used to indicate that a request to process a command is rejected.

We write S for the set of all services and R for the set {T, F, B}. Given a service H and a method m ∈ M, the derived service of H after processing m, written ∂ ∂m H, is defined by

∂ ∂m H(ρ) = H( m ρ).
A service H can be understood as follows:

• if H( m ) = B, then the request to process m is accepted by the service, the reply is H( m ), and the service proceeds as ∂ ∂m H; • if H( m ) = B, then the request to process m is not accepted by the service.

For each f ∈ F, we introduce the use operator / f : T × S → T. Intuitively, p / f H is the thread that results from processing all basic actions performed by thread p that are of the form f.m by service H. When a basic action of the

S / f H = S TSU1 D / f H = D TSU2 tau • x / f H = tau • (x / f H) T S U 3 (x g.m y) / f H = (x / f H) g.m (y / f H) if ¬f = g TSU4 (x f.m y) / f H = tau • (x / f ∂ ∂m H) if H( m ) = T TSU5 (x f.m y) / f H = tau • (y / f ∂ ∂m H) if H( m ) = F TSU6 (x f.m y) / f H = D i f H( m ) = B TSU7
form f.m performed by thread p is processed by service H, it is turned into the internal action tau and postconditional composition is removed in favour of action prefixing on the basis of the reply value produced. The internal action tau that it is left as a trace of the processed action could be abstracted from, but this would exclude analysis to which the presence of internal activity is relevant.

The axioms for the use operators are given in Table 3. In this table, f and g stand for arbitrary foci from F and m stands for an arbitrary method from M. Axioms TSU3 and TSU4 express that the action tau and basic actions of the form g.m with f = g are not processed. Axioms TSU5 and TSU6 express that a thread is affected by a service as described above when a basic action of the form f.m performed by the thread is processed by the service. Axiom TSU7 expresses that deadlock takes place when a basic action to be processed is not accepted.

Let T stand for either BTA or BTA+REC. Then we will write T +TSU for T , taking the set {f.m | f ∈ F, m ∈ M} for A, extended with the use operators and the axioms from Table 3.

Poly-threading

BTA is a theory of the behaviours exhibited by sequential programs on execution. To cover the case where the programs have been split into fragments, we extend BTA in this section with the barest mechanism for sequencing of threads that are taken for fragments. The resulting theory is called TA pt .

Our general view on the way of achieving a joint behaviour of the program fragments in a collection of program fragments between which execution can be switched is as follows:

• there can only be a single program fragment being executed at any stage;

• the program fragment in question may make any program fragment in the collection the one being executed;

• making another program fragment the one being executed is effected by executing a special instruction for switching over execution;

• any program fragment can be taken for the one being executed initially.

In order to obtain such a joint behaviour from the behaviours of the program fragments on execution, a mechanism is needed by which the start-up of another program fragment behaviour is effectuated whenever a program fragment behaviour ends up with the intent to achieve such a start-up. In the setting of BTA, taking threads for program fragment behaviours, this requires the introduction of an additional sort, additional constants and additional operators. In doing so it is supposed that a collection of threads that corresponds to a collection of program fragments between which execution can be switched takes the form of a sequence, called a thread vector.

Like in BTA+TSU, it is assumed that there is a fixed but arbitrary finite set F of foci and a fixed but arbitrary finite set M of methods. It is also assumed that tls ∈ F and init ∈ M. The focus tls and the method init play special roles: tls is the focus of a service that is initialized each time a thread is started up by the mechanism referred to above and init is the initialization method of that service. For the set A of basic actions, we take again the set {f.m | f ∈ F, m ∈ M}.

TA pt has the sort T of BTA and in addition the sort TV of thread vectors. To build terms of sort T, TA pt has the constants and operators of BTA and in addition the following additional constants and operators:

• for each i ∈ N, the internally controlled switch-over constant Si : T;

• the externally controlled switch-over constant E : T;

• the poly-threading operator ⊥ : T × TV → T;

• for each k ∈ N + , 5 the k-ary external choice operator k : T × • • • × T k times → T.
To build terms of sort TV, TA pt has the following constants and operators:

• the empty thread vector constant : TV;

• the singleton thread vector operator : T → TV;

• the thread vector concatenation operator : TV × TV → TV.

Throughout the paper, we assume that there are infinitely many variables of sort TV, including α, β, γ.

In the context of the poly-threading operator ⊥, the constants Si and E are alternatives for the constant S which produce additional effects. Let p, p 1 , . . . , p n be closed terms of sort T. Then ⊥(p, p 1 . . . p n ) first behaves as p, but when p terminates:

• in the case where p terminates with S, it terminates;

• in the case where p terminates with Si:

it continues by behaving as

⊥(p i , p 1 . . . p n ) if 1 ≤ i ≤ n, -it deadlocks otherwise;
• in the case where p terminates with E, it continues by behaving as one of

⊥(p 1 , p 1 . . . p n ), . . . , ⊥(p n , p 1 . . . p n ) or it deadlocks.
Moreover, the basic action tls.init is performed between termination and continuation. In the case where p terminates with E, the choice between the alternatives is made externally. Nothing is stipulated about the effect that the constants

Si and E produce in the case where they occur outside the context of the poly-threading operator.

⊥(S, α) = S SPT1 ⊥(D, α) = D SPT2 ⊥(x a y, α) = ⊥(x, α) a ⊥(y, α) S P T 3 ⊥(Si, x 1 . . . xn ) = tls.init • ⊥(x i , x 1 . . . xn ) if 1 ≤ i ≤ n SPT4 ⊥(Si, x 1 . . . xn ) = D i f i = 0 ∨ i > n SPT5 ⊥(E, x 1 . . . x k ) = k (tls.init • ⊥(x 1 , x 1 . . . x k ), . . . , tls.init • ⊥(x k , x 1 . . . x k )) SPT6 ⊥(E, ) = D SPT7
The poly-threading operator concerns sequencing of threads. A thread selection involved in sequencing of threads is called an autonomous thread selection if the selection is made by the terminating thread. Otherwise, it is called a non-autonomous thread selection. The constants Si are meant for autonomous thread selections and the constant E is meant for non-autonomous thread selections. We remark that non-autonomous thread selections are immaterial to the joint behaviours of program fragments referred to above.

In the case of a non-autonomous thread selection, it comes to an external choice between a number of threads.

The external choice operator k concerns external choice between k threads. An external choice between a number of threads is a choice where the threads concerned have no control of the choice. Let p 1 , . . . , p k be closed terms of sort T. Then k (p 1 , . . . , p k ) behaves as the outcome of an external choice between p 1 , . . . , p k and D.

TA pt has the axioms of BTA and in addition the axioms given in Table 4. In this table, a stands for an arbitrary action from A tau . The additional axioms express that threads are sequenced by poly-threading as described above.

There are no axioms for the external choice operators because their basic properties cannot be expressed as equations or conditional equations. For each k ∈ N + , the basic properties of k are expressed by the following disjunction of

equations: i∈[1,k] k (x 1 , . . . , x k ) = x i ∨ k (x 1 , . . . , x k ) = D. 6
To be fully precise, we should give axioms concerning the constants and operators to build terms of the sort TV as well. We refrain from doing so because the constants and operators concerned are the usual ones for sequences.

Similar remarks apply to the sort DTV introduced later and will not be repeated.

Guarded recursion can be added to TA pt as it is added to BTA in Section 2. We will write TA pt +REC for TA pt extended with the constants for solutions of guarded recursive specifications and axioms RDP and RSP.

The use mechanism can be added to TA pt as it is added to BTA in Section 3. Let T stand for either TA pt or TA pt +REC. Then we will write T +TSU for T extended with the use operators and the axioms from Table 3.

Table 5. Axioms for postconditional switching

tau k (x 1 , . . . , x k ) = tau k (x 1 , . . . , x 1 ) ⊥(a k (x 1 , . . . , x k ), α) = a k ( ⊥(x 1 , α), . . . , ⊥(x k , α)) tau k (x 1 , . . . , x k ) / f H = tau k (x 1 / f H, . . . , x k / f H) g.m k (x 1 , . . . , x k ) / f H = g.m k (x 1 / f H, . . . , x k / f H) if ¬f = g f.m k (x 1 , . . . , x k ) / f H = tau • (x i / f ∂ ∂m H) if H( m ) = i ∧ i ∈ [1, k] f.m k (x 1 , . . . , x k ) / f H = D i f ¬H( m ) ∈ [1, k]

Internalization of non-autonomous thread selection

In the case of non-autonomous thread selection, the selection of a thread is made externally. In this section, we show how non-autonomous thread selection can be internalized. For that purpose, we first extend TA pt with postconditional switching. Postconditional switching is like postconditional composition, but covers the case where services processing basic actions produce reply values from the set N instead of reply values from the set {T, F}. Postconditional switching is convenient when internalizing non-autonomous thread selection, but it is not necessary.

For each a ∈ A tau and k ∈ N + , we introduce the k-ary postconditional switch operator a k :

T × • • • × T k times → T.
Let p 1 , . . . , p k be closed terms of sort T. Then a k (p 1 , . . . , p k ) will first perform action a, and then proceed as p 1 if the processing of a leads to the reply 1, . . . , p k if the processing of a leads to the reply k.

The axioms for the postconditional switching operators are given in Table 5. In this table, a stands for an arbitrary action from A tau , f and g stand for arbitrary foci from F, and m stands for an arbitrary method from M.

We proceed with the internalization of non-autonomous thread selections. Let p, p 1 , . . . , p k be closed terms of sort T. The idea is that ⊥(p, p 1 . . . p k ) can be internalized by:

• replacing in ⊥(p, p 1 . . . p k ) all occurrences of E by Sk+1;

• appending a thread that can make the thread selections to the thread vector.

Simultaneous with the replacement of all occurrences of E by Sk+1, all occurrences of Sk+1 must be replaced by D to prevent inadvertent selections of the appended thread. When making a thread selection, the appended thread has to request the external environment to give the position of the thread that it would have selected itself. We make the simplifying assumption that the external environment can be viewed as a service.

Let p, p 1 , . . . , p k be closed terms of sort T. Then the internalization of ⊥(p, p 1 . . .

p k ) is ⊥(ρ(p), ρ(p 1 ) . . . ρ(p k ) ext.sel k (S1, . . . , Sk) ) ,
where ρ(p ) is p with simultaneously all occurrences of E replaced by Sk+1 and all occurrences of Sk+1 replaced by D. Here, it is assumed that ext ∈ F and sel ∈ M.

Postconditional switching is not really necessary for internalization. Let the number of actions performed to select a thread is between 2 log(k) and 2 log(k) .

k 1 = k/2 , k 2 = k 1 /2 , k 3 = (k -k 1 )

Algebra of Communicating Processes

In Section 7, we will investigate the connections of threads and services with processes as considered in ACP-style process algebras. We will focus on ACP (Algebra of Communicating Processes), which was first presented in [START_REF] Bergstra | Process algebra for synchronous communication[END_REF].

In this section, we shortly review ACP. A comprehensive introduction to ACP can be found in [START_REF] Baeten | Process Algebra[END_REF][START_REF] Fokkink | Introduction to Process Algebra[END_REF].

ACP has one sort: the sort P of processes. In ACP, it is assumed that there are a fixed but arbitrary set A of actions with δ / ∈ A and a fixed but arbitrary commutative and associative function

| : A ∪ {δ} × A ∪ {δ} → A ∪ {δ} such that δ | a = δ for all a ∈ A ∪ {δ}.
The function | is regarded to give the result of synchronously performing any two actions for which this is possible, and to be δ otherwise. Henceforth, we write A δ for A ∪ {δ}.

Let p and q be closed terms of sort P, a ∈ A, and H ⊆ A. Intuitively, the constants and operators to build terms of sort P can be explained as follows:

• δ can neither perform an action nor terminate successfully;

• a first performs action a and then terminates successfully;

• p + q behaves either as p or as q, but not both;

• p • q first behaves as p and on successful termination of p it next behaves as q;

• p q behaves as the process that proceeds with p and q in parallel;

• p q behaves the same as p q, except that it starts with performing an action of p;

• p | q behaves the same as p q, except that it starts with performing an action of p and an action of q synchronously;

• ∂ H (p) behaves the same as p, except that actions from H are blocked.

The operators and | are of an auxiliary nature. They are needed to axiomatize ACP. The axioms of ACP are given in e.g. [START_REF] Fokkink | Introduction to Process Algebra[END_REF].

We write i∈I p i , where I = {i 1 , . . . , i n } and p i1 , . . . , p in are terms of sort P, for p i1 +. . .+p in . The convention is that i∈I p i stands for

δ if I = ∅.
A process is considered definable over ACP if there exists a guarded recursive specification over ACP that has that process as its solution.

A recursive specification over ACP is a set of recursion equations E = {X = t X | X ∈ V }, where V is a set of variables of sort P and each t X is a term of sort P that only contains variables from V . Let t be a term of sort P 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 term containing this occurrence of X. Let E be a recursive specification over ACP. Then E is a guarded recursive specification if, in each equation X = t X ∈ E, all occurrences of variables in t X are guarded or t X can be rewritten to such a term using the axioms of ACP in either direction and/or the equations in E except the equation X = t X from left to right. We only consider models of ACP in which guarded recursive specifications have unique solutions, such as the projective limit model and the finitely branching graph model presented in [START_REF] Baeten | Process Algebra[END_REF].

For each guarded recursive specification E and each variable X that occurs as the left-hand side of an equation in E, we introduce a constant of sort P standing for the unique solution of E for X. This constant is denoted by X|E .

The axioms for guarded recursion have the same shape as in the case of BTA (see Table 2), but now X, t X and E stand for an arbitrary variable of sort P, an arbitrary ACP term of sort P and an arbitrary guarded recursive specification over ACP, respectively.

In order to express the use operators, we need an extension of ACP with action renaming operators. Intuitively, the action renaming operator ρ f , where f : A → A, can be explained as follows: ρ f (p) behaves as p with each action replaced according to f . The axioms for action renaming are given in e.g. [START_REF] Fokkink | Introduction to Process Algebra[END_REF]. We write ρ a →a for the renaming operator ρ g with g defined by g(a ) = a and g(a) = a if a = a .

Threads, services and ACP-definable processes

Because it may be helpful in forming a better idea of TA pt +REC+TSU, we relate in this section threads and services as considered in TA pt +REC+TSU to processes that are definable over ACP with action renaming.

For that purpose, A and | are taken as follows:

A = {s f (d) | f ∈ F, d ∈ M ∪ R} ∪ {r f (d) | f ∈ F, d ∈ M ∪ R} ∪ {s ext (n) | n ∈ N} ∪ {r ext (n) | n ∈ N} ∪ {stop, stop, stop * , i} ∪ {s serv (r) | r ∈ R} ∪ {r serv (m) | m ∈ M} ; for all a ∈ A, f ∈ F, d ∈ M ∪ R, m ∈ M, r ∈ R and n ∈ N: s f (d) | r f (d) = i , s f (d) | a = δ if a = r f (d) , a | r f (d) = δ if a = s f (d) , s ext (n) | r ext (n) = i , s ext (n) | a = δ if a = r ext (n) , a | r ext (n) = δ if a = s ext (n) , stop | stop = stop * , stop | a = δ if a = stop , a | stop = δ if a = stop , i | a = δ , s serv (r) | a = δ , a | r serv (m) = δ .
The actions of the forms s f (d) and r f (d) are used for communication between threads and services, the actions of the forms s ext (n) and r ext (n) are used for communication between threads and their environment, the actions stop and stop are used for synchronization between threads and services on termination, and the actions stop * and i are the actions that remain as the result of synchronizations on termination and communications, respectively. The actions of the forms s serv (r) and r serv (m) are actions that are intended to be replaced by actions for communication between threads and services.

For each f ∈ F, the set A f ⊆ A and the function R f : A → A are defined as follows:

A f = {s f (d) | d ∈ M ∪ R} ∪ {r f (d) | d ∈ M ∪ R} ; Table 6. Definition of translation functions [[X]](α) = X [[S]](α) = stop [[D]](α) = i • δ [[t 1 tau t 2 ]](α) = i • i • [[t 1 ]](α) [[t 1 f.m t 2 ]](α) = s f (m) • (r f (T) • [[t 1 ]](α) + r f (F) • [[t 2 ]](α)) [[Si]](α) = tls.init • [[α[i]]](α) if 1 ≤ i ≤ len(α) [[Si]](α) = i • δ if i = 0 ∨ i > len(α) [[E]](α) = È i∈[1,len(α)] rext(i) • tls.init • [[α[i]]](α) + i • δ [[ ⊥(t, α )]](α) = [[t]](α ) [[ k (t 1 , . . . , t k )]](α) = È i∈[1,k] rext(i) • [[t i ]](α) + i • δ [[ X|E ]](α) = X|{X = [[t]](α) | X = t ∈ E} [[t / f H]](α) = ρ stop * →stop (∂ {stop,stop} (∂ A f ([[t]](α) ρ R f ([[H]])))) [[H]] = X H |{X H = È m∈M rserv(m) • sserv(H ( m )) • X ∂ ∂m H + stop | H ∈ ∆(H)}
for all a ∈ A, m ∈ M and r ∈ R:

R f (s serv (r)) = s f (r) , R f (r serv (m)) = r f (m) , R f (a) = a if r ∈R a = s serv (r ) ∧ m ∈M a = r serv (m ) .
The sets A f and the functions R f play a part in expressing the use operators in terms of the operators of ACP with action renaming. The sets A f are used to encapsulate actions for communication between threads and services from communication with actions coming from the environment. The functions R f are used to replace actions of the forms s serv (r) and r serv (m) by actions for communication between threads and services.

For convenience, we introduce a special notation. Let α be a term of sort TV, let p 1 , . . . , p n be terms of sort T such that α = p 1 . . . p n , and let i ∈ [1, n]. Then we write α[i] for p i .

We proceed with relating threads and services as considered in TA pt +REC+TSU to processes definable over ACP with action renaming. The underlying idea is that threads and services can be viewed as processes that are definable over ACP with action renaming. We define those processes by means of a translation function [[ ]] from the set of all terms of sort T to the set of all functions from the set of all terms of sort TV to the set of all terms of sort P and a translation function [[ ]] from the set of all services to the set of all terms of sort P. These translation functions are defined inductively by the equations given in Table 6, where ∆(H) is inductively defined as follows:

• H ∈ ∆(H); • if m ∈ M and H ∈ ∆(H), then ∂ ∂m H ∈ ∆(H).

Let p be a term of sort T. Then the process algebraic interpretation of p is [[p]]( ). Henceforth, we write [[ ]] for the translation function [[ ]]( ).

The translation function [[ ]]

preserves the axioms of TA pt +REC+TSU. Roughly speaking, this means that the translations of these axioms are derivable from the axioms of ACP with action renaming and guarded recursion.

Before we make this fully precise, we have a closer look at the axioms of TA pt +REC+TSU.

A proper axiom is an equation or a conditional equation. In Tables 1-4, we do not only find proper axioms. In addition to proper axioms, we find: (i) axiom schemas without side conditions; (ii) axiom schemas with syntactic side conditions; (iii) axiom schemas with semantic side conditions. The axioms of TA pt +REC+TSU are obtained by replacing each axiom schema by all its instances. Owing to the presence of axiom schemas with semantic side conditions, the axioms of TA pt +REC+TSU include proper axioms and axioms with semantic side conditions. The instances of TSU5, TSU6, and TSU7 are the only axioms of TA pt +REC+TSU with semantic side conditions. These semantic side conditions concerned are of the form H( m ) = r.

Consider the set that consists of:

• all equations t 1 = t 2 , where t 1 and t 2 are terms of sort T;

• all conditional equations E ⇒ t 1 = t 2 , where t 1 and t 2 are terms of sort T and E is a set of equations t 1 = t 2

where t 1 and t 2 are terms of sort T.

We define a translation function [[ ]]

from this set to the set of all equations of ACP with action renaming and guarded recursion as follows:

[[t 1 = t 2 ]] = [[t 1 ]] = [[t 2 ]] , [[E ⇒ t 1 = t 2 ]] = {[[t 1 ]] = [[t 2 ]] | t 1 = t 2 ∈ E} ⇒ [[t 1 ]] = [[t 2 ]] .

Theorem (Preservation).

1. Let φ be a proper axiom of TA pt +REC+TSU. Then [[φ]] is derivable from the axioms of ACP with action renaming and guarded recursion.

2. Let φ if ψ be an axiom of TA pt +REC+TSU with semantic side condition. Then [[φ]] is derivable from the axioms of ACP with action renaming and guarded recursion under the assumption that ψ holds.

Proof. The proof is straightforward. We sketch the proof for axiom TSU5, writing E H for the guarded recursive

specification {X H = m∈M r serv (m) • s serv (H ( m )) • X ∂ ∂m H + stop | H ∈ ∆(H)}. By the definition of the translation function [[ ]], it must be shown that [[(x f.m y) / f H]] = [[tau • (x / f ∂ ∂m H)]
] is derivable under the assumption that H( m ) = T holds. In outline, this goes as follows:

[[(x f.m y) / f H]] = ρ stop * →stop (∂ {stop,stop} (∂ A f (s f (m) • (r f (T) • x + r f (F) • y) ρ R f ( X H |E H )))) = i • i • ρ stop * →stop (∂ {stop,stop} (∂ A f (x ρ R f ( X ∂ ∂m H |E H )))) = [[tau • (x / f ∂ ∂m H)]] .
In the first and third step, we apply defining equations of [[ ]]. In the second step, we apply axioms of ACP with action renaming and guarded recursion, and use the assumption that H( m ) = T.

The gist of the preservation theorem is that the translation function [[ ]] represents a theory interpretation. In logic, however, the concept of a theory interpretation does not take semantic side conditions into account.

Execution architectures for fragmented programs

An analytic execution architecture in the sense of [START_REF] Bergstra | Execution architectures for program algebra[END_REF] is a model of a hypothetical execution environment for sequential programs that is designed for the purpose of explaining how a program may be executed. An analytic execution architecture makes explicit the interaction of a program with the components of its execution environment.

The notion of analytic execution architecture defined in [START_REF] Bergstra | Execution architectures for program algebra[END_REF] is suited to sequential programs that have not been split into fragments. In this section, we discuss analytic execution architectures suited to sequential programs that have been split into fragments in the current setting. Thus, we illustrate an application of the thread algebra for poly-threading developed so far.

The notion of analytic execution architecture from [START_REF] Bergstra | Execution architectures for program algebra[END_REF] is defined in the setting of program algebra. In [START_REF] Bergstra | Program algebra for sequential code[END_REF], a thread extraction operation | | is defined which gives, for each program considered in program algebra, the thread that is taken for the behaviour exhibited by the program on execution. In the case of programs that have been split into fragments, additional instructions for switching over execution to another program fragment are needed. We assume that a collection of program fragments between which execution can be switched takes the form of a sequence, called an program fragment vector, and that there is an additional instruction ###i for each i ∈ N. Switching over execution to the i-th program fragment in the program fragment vector is effected by executing the instruction ###i.

If i equals 0 or i is greater than the length of the program fragment vector, execution of ###i results in deadlock.

The instruction ###i is reminiscent of the system call exec() of Unix-like operating systems. We extend thread extraction as follows:

|###i| = Si , |###i ; x| = Si .
An analytic execution architecture for programs that have been split into fragments consists of a component containing a program fragment, a component containing a program fragment vector and a number of service components.

The component containing a program fragment is capable of processing instructions one at a time, issuing appropriate requests to service components and awaiting replies from service components as described in [START_REF] Bergstra | Execution architectures for program algebra[END_REF] in so far as instructions other than switch-over instructions are concerned. This implies that, for each service component, there is a channel for communication between the program fragment component and that service component and that foci are used as names of those channels. In the case of a switch-over instruction, the component containing a program fragment is capable of loading the program fragment to which execution must be switched from the component containing a program fragment vector.

The analytic execution architecture made up of a component containing the program fragment P , a component containing the program fragment vector α = P 1 . . . P n , and service components H 1 , . . . , H k with channels named f 1 , . . . , f k , respectively, is described by the thread

⊥(|P |, |P 1 | . . . |P n | ) / f1 H 1 . . . / f k H k .
In the case where instructions of the form ###i do not occur in P ,

[[ ⊥(|P |, |P 1 | . . . |P n | ) / f1 H 1 . . . / f k H k ]]
agrees with the process-algebraic description given in [START_REF] Bergstra | Execution architectures for program algebra[END_REF] of the analytic execution architecture made up of a component containing the program P and service components H 1 , . . . , H k with channels named f 1 , . . . , f k , respectively.

Poly-threaded strategic interleaving

In this section, we take up the extension of TA pt with a form of interleaving suited for multi-threading. Multi-threading refers to the concurrent existence of several threads in a program under execution. Multi-threading is provided by contemporary programming languages such as Java [START_REF] Gosling | The Java Language Specification[END_REF] and C# [START_REF] Hejlsberg | C# Language Specification[END_REF]. Arbitrary interleaving, on which ACP [START_REF] Baeten | Process Algebra[END_REF], CCS [START_REF] Milner | Communication and Concurrency[END_REF] and CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] are based, is not an appropriate abstraction when dealing with multithreading. In the case of multi-threading, some deterministic interleaving strategy is used. In [START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF], we introduced a number of plausible deterministic interleaving strategies for multi-threading. We proposed to use the phrase "strategic interleaving" for the more constrained form of interleaving obtained by using such a strategy. In this section, we consider a poly-threading covering variation of the simplest interleaving strategy introduced in [BM07b], namely pure cyclic interleaving.

As in [START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF], it is assumed that the collection of threads to be interleaved takes the form of a thread vector. In the poly-threaded case, cyclic interleaving basically operates as follows: at each stage of the interleaving, the first thread in the thread vector gets a turn to perform a basic action or to switch over to another thread and then the thread vector undergoes cyclic permutation. We mean by cyclic permutation of a thread vector that the first thread in the thread vector becomes the last one and all others move one position to the left. If one thread in the thread vector deadlocks, the whole does not deadlock till all others have terminated or deadlocked. An important property of cyclic interleaving is that it is fair, i.e. there will always come a next turn for all active threads. Other plausible interleaving strategies are treated in [START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF]. They can also be adapted to the poly-threaded case.

The extension of TA pt with cyclic interleaving is called TA pt si . It has the sorts T and TV of TA pt . To build terms of sort T, TA pt si has the constants and operators of TA pt to build terms of sort T and in addition the following operator:

• the poly-threaded cyclic strategic interleaving operator ⊥ : TV × TV → T.

To build terms of sort TV, TA pt si has the constants and operators of TA pt to build terms of sort TV. TA pt si has the axioms of TA pt and in addition the axioms given in Tables 7 and8. In these tables, a stands for an arbitrary action from A tau . The axioms from Table 7 express that threads are interleaved as described above. In these axioms, the auxiliary deadlock at termination operator S D occurs. The axioms from Table 8 show that this operator serves to turn termination into deadlock.

( , α) = S PCI1 ⊥ ( S β, α) = ⊥ (β, α) PCI2 ⊥ ( D β, α) = S D ( ⊥ (β, α)) PCI3 ⊥ ( x a y β, α) = ⊥ (β x , α) a ⊥ (β y , α) P C I 4 ⊥ ( Si β, x 1 . . . xn ) = tls.init • ⊥ (β x i , x 1 . . . xn ) if 1 ≤ i ≤ n PCI5 ⊥ ( Si β, x 1 . . . xn ) = S D ( ⊥ (β, x 1 . . . xn )) if i = 0 ∨ i > n PCI6 ⊥ ( E β, x 1 . . . x k ) = k (tls.init • ⊥ (β x 1 , x 1 . . . x k ), . . . , tls.init • ⊥ (β x k , x 1 . . . x k )) PCI7 ⊥ ( E β, ) = S D ( ⊥ (β, )) PCI8
Table 8. Axioms for deadlock at termination

S D (S) = D S2D1 S D (D) = D S2D2 S D (x a y) = S D (x) a S D (y) S 2 D 3 S D (Si) = Si S2D4 S D (E) = E S2D5 S D ( k (x 1 , . . . , x k )) = k (S D (x 1 ), . . . , S D (x k )) S2D6
Guarded recursion and the use mechanism can be added to TA pt si as they are added to BTA in Sections 2 and 3, respectively.

The axioms for poly-threaded cyclic interleaving given in Table 7 constitute a definition by recursion on the sum of the depths of all threads in the first thread vector with case distinction on the structure of the first thread in that thread vector and, in the case of E, with case distinction on the length of the second thread vector. Hence, it is obvious that the axioms are consistent and that every closed term of the sort T is derivably equal to one that does not contain the poly-threaded cyclic strategic interleaving operator. Similar remarks apply to the poly-threaded cyclic distributed strategic interleaving operators introduced in subsequent sections and will not be repeated.

Poly-threaded distributed strategic interleaving

In this section, we take up the extension of TA pt with a form of interleaving suited for distributed multi-threading. This extension concerns a plausible poly-threading covering variation of the simplest form of interleaving for distributed multi-threading considered in [START_REF] Bergstra | Distributed strategic interleaving with load balancing[END_REF]. The variation in question may be considered a very simple approximation of the form of interleaving that is found in systems built on multi-core processors and a fair form of scheduling (presumably realized by means of a global scheduler and a local scheduler per core). The simplification is considerable indeed, but we believe that this is inevitable to obtain a manageable theory.

In order to deal with threads that are distributed over the nodes of a network, it is assumed that there is a fixed but arbitrary finite set L of locations such that L ⊆ N. The set LA of located basic actions is defined by LA = {l.a | l ∈ L∧a ∈ A}. Henceforth, basic actions will also be called unlocated basic actions. The members of LA∪{l.tau | l ∈ L} are referred to as located actions.

Performing an unlocated action a is taken as performing a at a location still to be fixed by the distributed interleaving strategy. Performing a located action l.a is taken as performing a at location l.

Threads that perform unlocated actions only are called unlocated threads and threads that perform located actions only are called located threads. It is assumed that the collection of all threads that exist concurrently at the same location takes the form of a sequence of unlocated threads, called the local thread vector at the location concerned.

It is also assumed that the collection of local thread vectors that exist concurrently at the different locations takes the form of a sequence of pairs, one for each location, consisting of a location and the local thread vector at that location. Such a sequence is called a distributed thread vector.

In the distributed case, cyclic interleaving basically operates the same as in the non-distributed case. In the distributed case, we mean by cyclic permutation of a distributed thread vector that the first thread in the first local thread vector becomes the last thread in the first local thread vector, all other threads in the first local thread vector move one position to the left, the resulting local thread vector becomes the last local thread vector in the distributed thread vector, and all other local thread vectors in the distributed thread vector move one position to the left.

When discussing interleaving strategies on distributed thread vectors, we use the term "current thread" to refer to the first thread in the first local thread vector in a distributed thread vector and we use the term "current location" to refer to the location at which the first local thread vector in a distributed thread vector is.

The extension of TA pt with cyclic distributed interleaving is called TA pt dsi . It has the sorts T and TV of TA pt and in addition the following sorts:

• the sort LT of located threads;

• the sort DTV of distributed thread vectors.

To build terms of sort T, TA pt dsi has the constants and operators of BTA and in addition the following operators:

• for each n ∈ N, the migration postconditional composition operator mg(n) : T × T → T.

To build terms of sort TV, TA pt dsi has the constants and operators of TA pt to build terms of sort TV. To build terms of sort LT, TA pt dsi has the following constants and operators:

• the deadlock constant D : LT;

• the termination constant S : LT;

• for each l ∈ L and a ∈ A tau , the postconditional composition operator l.a : LT × LT → LT;

• the deadlock at termination operator S D : LT → LT;

• the poly-threaded cyclic distributed strategic interleaving operator ⊥ : DTV × TV → LT.

app l (x, [γ] l δ) = [γ x ] l δ if l = l app l (x, [γ] l δ) = [γ] l app l (x, δ) if l = l
To build terms of sort DTV, TA pt dsi has the following constants and operators:

• the empty distributed thread vector constant : DTV;

• for each l ∈ L, the singleton distributed thread vector operator [ ] l : TV → DTV;

• the distributed thread vector concatenation operator : DTV × DTV → DTV.

Throughout the paper, we assume that there are infinitely many variables of sort LT, including u, v, w, and infinitely many variables of sort DTV, including δ.

We introduce located action prefixing as an abbreviation: l.a•p, where p is a term of sort LT, abbreviates p l.a p.

The overloading of D, S, and could be resolved, but we refrain from doing so because it is always clear from the context which constant or operator is meant.

Essentially, the sort DTV includes all sequences of pairs consisting of a location and a local thread vector. 7 The ones that contain a unique pair for each location are the proper distributed thread vectors in the sense that the cyclic distributed interleaving strategy outlined above is intended for them. Improper distributed thread vectors that do not contain duplicate pairs for some location are needed in the axiomatization of this strategy. Improper distributed thread vectors that do contain duplicate pairs for some location appear to have more than one local thread vector at the location concerned. Their exclusion would make it necessary for concatenation of distributed thread vectors to be turned into a partial operator. The cyclic distributed interleaving strategy never turns a proper distributed thread vector into an improper one or the other way round.

The poly-threaded cyclic distributed strategic interleaving operator serves for interleaving of the threads in a proper distributed thread vector according to the strategy outlined above, but with support of explicit thread migration. In the case where a local thread vector of the form p mg(n) q γ with n ∈ L is encountered as the first local thread vector, γ becomes the last local thread vector in the distributed thread vector and p is appended to the local thread vector at location n. If n ∈ L, then γ q becomes the last local thread vector in the distributed thread vector.

In the axioms for cyclic distributed interleaving discussed below, binary functions app l (where l ∈ L) from unlocated threads and distributed thread vectors to distributed thread vectors are used. For each l ∈ L, app l maps each unlocated thread x and distributed thread vector δ to the distributed thread vector obtained by appending x to the local thread vector at location l in δ. The functions app l are defined in Table 9.

TA pt dsi has the axioms of TA pt and in addition the axioms given in Tables 10, 11 and 12. In these tables, a stands

( , α) = S PCDI1 ⊥ ([ ] l 1 . . . [ ] l k , α) = S PCDI2 ⊥ ([ ] l δ, α) = ⊥ (δ [ ] l , α) P C D I 3 ⊥ ([ S γ] l δ, α) = ⊥ (δ [γ] l , α) P C D I 4 ⊥ ([ D γ] l δ, α) = S D ( ⊥ (δ [γ] l , α)) PCDI5 ⊥ ([ x a y γ] l δ, α) = ⊥ (δ [γ x ] l , α) l.a ⊥ (δ [γ y ] l , α) P C D I 6 ⊥ ([ Si γ] l δ, x 1 . . . xn ) = l.tls.init • ⊥ (δ [γ x i ] l , x 1 . . . xn ) if 1 ≤ i ≤ n PCDI7 ⊥ ([ Si γ] l δ, x 1 . . . xn ) = S D ( ⊥ (δ [γ] l , x 1 . . . xn )) if i = 0 ∨ i > n PCDI8 ⊥ ([ E γ] l δ, x 1 . . . x k ) = k (l.tls.init • ⊥ (δ [γ x 1 ] l , x 1 . . . x k ), . . . , l.tls.init • ⊥ (δ [γ x k ] l , x 1 . . . x k )) PCDI9 ⊥ ([ E γ] l δ, ) = S D ( ⊥ (δ [γ] l , )) PCDI10 ⊥ ([ x mg(n) y γ] l δ, α) = l.tau • ⊥ (app n (x, δ [γ] l ), α) if n ∈ L PCDI11 ⊥ ([ x mg(n) y γ] l δ, α) = l.tau • ⊥ (δ [γ y ] l , α) if n ∈ L PCDI12
Table 12. Axioms for deadlock at termination

S D (S) = D LS2D1 S D (D) = D LS2D2 S D (u a v) = S D (u) a S D (v) L S 2 D 3 S D (Si) = Si LS2D4 S D (E) = E LS2D5 S D ( k (u 1 , . . . , u k )) = k (S D (u 1 ), . . . , S D (u k )) LS2D6
for an arbitrary action from A tau . The axioms from Table 11 express that threads are interleaved as described above.

The axioms from Tables 10 and 12 are the axioms from Tables 1 and 8 adapted to located threads.

Guarded recursion and the use mechanism can be added to TA pt dsi as they are added to BTA in Sections 2 and 3, respectively.

Fragment searching by implicit migration

In Section 10, it was assumed that the same program fragment behaviours are available at each location. In the case where this assumption does not hold, distributed interleaving strategies with implicit migration of threads to achieve availability of fragments needed by the threads are plausible. We say that such distributed interleaving strategies take care of fragment searching. In this section, we introduce a variation of the distributed interleaving strategy from Section 10 with fragment searching. This results in a theory called TA pt dsi,fs . It is assumed that there is a fixed but arbitrary set I of fragment indices such that I = [1, n] for some n ∈ N.

In the case of the distributed interleaving strategy with fragment searching, immediately after the current thread has performed an action, implicit migration of that thread to another location may take place. Whether migration really takes place, depends on the fragments present at the current location. The current thread is implicitly migrated if the following condition is fulfilled: on its next turn, the current thread ought to switch over to a fragment that is not present at the current location. If this conditions is fulfilled, then the current thread will be migrated to the first among the locations where the fragment concerned is present.

To deal with that, we have to enrich distributed thread vectors. The new distributed thread vectors are sequences of triples, one for each location, consisting of a location, the local thread vector at that location, and the set of all indices of fragments that are present at that location.

TA pt dsi,fs has the same sorts as TA pt dsi . To build terms of the sorts T, TV and LT, TA pt dsi,fs has the same constants and operators as TA pt dsi . To build terms of sort DTV, TA pt dsi,fs has the following constants and operators:

• the empty distributed thread vector constant : DTV;

• for each l ∈ L and I ⊆ I, the singleton distributed thread vector operator [ ] Essentially, the sort TV includes all sequences of unlocated threads. These sequences may serve as local thread vectors and as fragment vectors. The sequences that contain a thread for each fragment index are proper fragment vectors. In the case of fragment vectors that contain more threads, there appear to be inaccessible fragments and in the case of fragment vectors that contain less threads, there appear to be disabled fragments. Inaccessible fragments have no influence on the effectiveness of cyclic distributed interleaving with fragment searching. However, disabled fragments may lead to implicit migration to a location where a switch-over on the next turn is not possible as well. Should this case arise, the next turn will yield deadlock.

In the axioms for cyclic distributed interleaving with fragment searching discussed below, binary functions app l Table 13. Definition of the functions app l app l (x, ) = (where l ∈ L) from unlocated threads and distributed thread vectors to distributed thread vectors are used which are similar to the functions app l used in the axioms for cyclic distributed interleaving without fragment searching given in Section 10. The functions app l are defined in Table 13.

Moreover, a unary function pv on distributed thread vectors is used which permutes distributed thread vectors cyclicly with implicit migration as outlined above. The function pv is defined using two auxiliary functions:

• a function iml mapping each fragment index i, distributed thread vector δ and location l to the first location in δ at which the fragment with index i is present if the fragment concerned is present anywhere, and location l otherwise;

• a function iml mapping each non-empty distributed thread vector δ to the first location in δ at which the fragment is present to which the current thread ought to switch over on its next turn if the current thread is in that circumstance and the fragment concerned is present somewhere, and the current location otherwise.

The function pv , as well as the auxiliary functions iml and iml , are defined in Table 14.

TA pt dsi,fs has the axioms of TA pt and in addition the axioms given in Tables 10, 15 and 12. Guarded recursion and the use mechanism can be added to TA pt dsi,fs as they are added to BTA in Sections 2 and 3, respectively.

Conclusions

We have developed a theory of the behaviours exhibited by sequential programs on execution that covers the case where the programs have been split into fragments and have used it to describe analytic execution architectures suited for such programs. It happens that the resulting description is terse. We have also shown that threads and services as considered in this theory can be viewed as processes that are definable over ACP. Threads and services are introduced for pragmatic reasons only: describing them as general processes is awkward. For example, the description of analytic execution architectures suited for programs that have been split into fragments would no longer be terse if ACP had been used.

We have also taken up the extension of the theory developed to the case where the steps of fragmented program behaviours are interleaved in the ways of non-distributed and distributed multi-threading. This work can be further elaborated on the lines of [START_REF] Bergstra | Distributed strategic interleaving with load balancing[END_REF] to cover issues such as prevention from migration for threads that keep locks on shared services, load balancing by means of implicit migration, and the use of implicit migration to achieve availability of services needed by threads.

The object pursued with the line of research that we have carried on with this paper is the development of a theoretical understanding of the concept of a sequential program and the concept of a sequential program behaviour.

We regard the work presented in this paper primarily as a step in the development of a theoretical understanding of the concept of a sequential program behaviour in the presence of program overlaying. We think that such theoretical understanding is important to the development of successful operating systems for real-time embedded systems.

  Correspondence and offprint requests to: C. A. Middelburg, Informatics Institute, Faculty of Science, University of Amsterdam, Science Park 904, 1098 XH Amsterdam, the Netherlands. Tel: +31 20 525 5239, fax: +31 20 525 7490, e-mail: C.A.Middelburg@uva.nl.

Il:

  TV → DTV; • the distributed thread vector concatenation operator : DTV × DTV → DTV. That is, the operator [ ] l is replaced by the operators [ ] I l .

  app l (x, [γ] I l δ) = [γ x ] I l δ if l = l app l (x, [γ] I l δ) = [γ] I l app l (x, δ) if l = lTable14. Definition of the functions iml , iml and pviml (i, , l ) = l iml (i, [γ] I l δ, l ) = l if i ∈ I iml (i, [γ] I l δ, l ) = iml (i, δ, l ) if i ∈ I iml([ ] l ⇒ pv ([ x γ] I l δ) = app l (x, δ [γ] I l )

  l.tls.init • ⊥ (pv ([ x i γ] I l δ), x 1 . . . xn ) if i ∈ I ∩ [1, n] PCDIfs7 ⊥ ([ Si γ] I l δ, x 1 . . . xn ) = S D ( ⊥ (δ [γ] I l , x 1 . . . xn )) if i ∈ I ∩ [1, n] PCDIfs8 ⊥ ([ E γ] I l δ, x 1 . . . x k ) = k (l.tls.init • ⊥ (pv ([ x 1 γ] I l δ), x 1 . . . x k ), . . . , l.tls.init • ⊥ (pv ([ x k γ] = S D ( ⊥ (δ [γ] I l , )) PCDIfs10 ⊥ ([ x mg(n) y γ] I l δ, α) = l.tau • ⊥ (app n (x, δ [γ] I l ), α) if n ∈ L PCDIfs11 ⊥ ([ x mg(n) y γ] I l δ, α) = l.tau • ⊥ (pv ([ y γ] I l δ), α) if n ∈ L PCDIfs12

Table 1 .

 1 Axiom of BTAx tau y = x tau x T1

Table 2 .

 2 Axioms for guarded recursion

  Table2to BTA, where we write t X |E for t X with, for all Y ∈ V(E), all occurrences of Y in t X replaced by Y |E . 2 In this table, X, t X and E stand for an arbitrary variable of sort T, an arbitrary BTA term of sort T and an arbitrary guarded recursive specification over BTA, respectively. Side conditions are added to restrict the variables, terms and guarded recursive specifications for which X, t X and E stand.

Table 3 .

 3 Axioms for use

Table 4 .

 4 Axioms for poly-threading

  k3 } and {p k3+1 , . . . , p k }, depending on the outcome of the previous selection, etcetera. In this way,

/2 , . . . . Using postconditional composition, first a selection can be made between {p 1 , . . . , p k1 } and {p k1+1 , . . . , p k }, next a selection can be made between {p 1 , . . . , p k2 } and {p k2+1 , . . . , p k1 } or between {p k1+1 , . . . , p

Table 7 .

 7 Axioms for poly-threaded cyclic interleaving

	⊥

Table 9 .

 9 Definition of the functions app l

	app l (x, ) =

Table 10 .

 10 Axioms for postconditional composition u l.tau v = u l.tau u LT1

Table 11 .

 11 Axioms for poly-threaded cyclic distributed interleaving

	⊥

Table 15 .

 15 Axioms for cyclic distributed interleaving with fragment searching

In[START_REF] Bergstra | Program algebra for sequential code[END_REF], basic thread algebra is introduced under the name basic polarized process algebra. Prompted by the development of thread algebra[START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF], which is a design on top of it, basic polarized process algebra has been renamed to basic thread algebra.

Throughout the paper, we use the symbol ⇒ for implication. We use the precedence conventions that the equality symbol binds stronger than the implication symbol.

This version of the use mechanism was first introduced in[START_REF] Bergstra | Thread algebra for strategic interleaving[END_REF]. In later papers, it is also called thread-service composition.

We write D * for the set of all finite sequences with elements from set D and D + for the set of all non-empty finite sequences with elements from set D. We use the following notation for finite sequences:for the empty sequence, d for the sequence having d as sole element, σ σ for the concatenation of finite sequences σ and σ , and len(σ) for the length of finite sequence σ.

We write N + for the set {n ∈ N | n > 0}. Throughout the paper, we use the convention that k and n stand for arbitrary elements of N + and N, respectively.

We use the notation [n, m], where n, m ∈ N, for the set {i ∈ N | n ≤ i ≤ m}.

Acknowledgements

This research was partly carried out in the framework of the Jacquard-project Symbiosis, which is funded by the Netherlands Organisation for Scientific Research (NWO). We thank an anonymous referee for his/her valuable suggestions concerning the presentation of the paper.