Static and Dynamic Processor Allocation

for Higher-Order Concurrent Languages^{∗}

Hanne Riis Nielson, Flemming Nielson

Computer Science Department, Aarhus University, Denmark.

          e-mail:{hrnielson,fnielson}@daimi.aau.dk

Abstract. Starting from the process algebra for Concurrent ML we develop two program analyses that facilitate the intelligent placement of processes on processors. Both analyses are obtained by augmenting an inference system for counting the number of channels created, the number of input and output operations performed, and the number of processes spawned by the execution of a Concurrent ML program. One analysis provides information useful for making a static decision about processor allocation; to this end it accumulates the communication cost for all processes with the same label. The other analysis provides information useful for making a dynamic decision about processor allocation; to this end it determines the maximum communication cost among processes with the same label. We prove the soundness of the inference system and the two analyses and demonstrate how to implement them; the latter amounts to transforming the syntax-directed inference problems to instances of syntax-free equation solving problems.

1 Introduction

Higher-order concurrent languages as CML [16] and FACILE [5] offer primitives for the dynamic creation of processes and channels. A distributed implementation of these languages immediately raises the problem of processor allocation. The efficiency of the implementation will depend upon how well the network configuration matches the communication topology of the program – and here it is important which processes reside on which processors. When deciding this it will be useful to know:

• Which channels will be used by the process for input and output operations and how many times will the operations be performed?

• Which channels and processes will be created by the process and how many instances will be generated?

As an example, two processes that frequently communicate with one another should be allocated on processors in the network so as to ensure a low communication overhead.

∗This is a preliminary version of a paper accepted for TAPSOFT’95; the full version appears as DAIMI-PB 483 and is also available on http://www.daimi.aau.dk/∼bra8130/LOMAPS.html

In CML and FACILE processes and channels are created dynamically and this leads naturally to a distinction between two different processor allocation schemes:

• Static processor allocation: At compile-time it is decided where all instances of a process will reside at run-time.

• Dynamic processor allocation: At run-time it is decided where the individual instances of a process will reside.

The first scheme is the simpler one and it is used in the current distributed implementation of FACILE; finer grain control over parallelism may be achieved using the second scheme [18].

What has been accomplished. In this paper we present analyses providing information for static and dynamic processor allocation of CML programs. We shall follow the approach of [13] and develop the analyses in two stages:

• Extract the communication behaviour of the CML program.

• Analyse the behaviour.

The two analyses only differ in the second stage.

The first stage follows [13] in developing a type and behaviour inference system for expressing the communication capabilities of programs in CML. This formulation takes full account of the polymorphism present in ML and algorithms for the automatic extraction of behaviours from CML programs are developed in [14, 1]. As was already indicated in [12] the behaviours may be regarded as terms in a process algebra (like CCS or CSP); however the process algebra of behaviours is specifically designed so as to capture those aspects of communication that are relevant for the efficient implementation of programs in CML.

The second stage of the two analyses are developed in detail in the present paper. To prepare for this we first develop an analysis that uses simple ideas from abstract interpretation to count for each behaviour the number of channels created, the number of input and output operations performed and the number of processes spawned. To provide information for static and dynamic processor allocation we then differentiate the information with respect to labels associated with the fork operations of the CML program; these labels will identify all instances of a given process and for each label we count the number of channels created, the number of input and output operations performed and the number of processes spawned. The central observation is now that for the static allocation scheme we accumulate the requirements of the individual instances whereas for the dynamic allocation scheme we take the maximum of the individual instance requirements.

In this paper we prove the correctness of the second stage of the analysis. The analyses are specified as inference systems and the correctness proof is based on a structural operational semantics for behaviours and an appropriate abstraction of the non-negative natural numbers. The correctness of the complete analysis then follows from the subject reduction result of [13] that allows us to lift safety (as opposed to liveness) results from the behaviours to safety results for CML programs.

We also address the implementation of the second stage of the analysis. Here the idea is to transform the problem as specified by the syntax-directed inference system into a syntax-free equation solving problem where standard techniques from data flow analysis can be used to obtain fast implementations. (As already mentioned the implementation of the first stage is the topic of [14, 1].)

Comparison with other work. First we want to stress that our approach to processor allocation is that of static program analysis rather than, say, heuristics based on profiling as is often found in the literature on implementation of concurrent languages.

In the literature there are only few program analyses for combined functional and concurrent languages. An extension of SML with Linda communication primitives is studied in [3] and, based on the corresponding process algebra, an analysis is presented that provides useful information for the placement of processes on a finite number of processors. A functional language with communication via shared variables is studied in [9] and its communication patterns are analysed, again with the goal of producing useful information for processor (and storage) allocation. Also a couple of program analyses have been developed for concurrent languages with an imperative facet. The papers [4, 8, 15] all present reachability analyses for concurrent programs with a statically determined communication topology; only [15] shows how this restriction can be lifted to allow communication in the style of the π-calculus. Finally,

[11] presents an analysis determining the number of communications on each channel connecting two processes in a CSP-like language.

As mentioned our analysis is specified in two stages. The first stage is formalised in [13, 14]; similar considerations were carried out by Havelund and Larsen leading to a comparable process algebra [6] but with no formal study of the link to CML nor with any algorithm for automatically extracting behaviours. The same overall idea is present in [3] but again with no formal study of the link between the process algebra and the programming language.

The second stage of the analysis extracts much more detailed information from the behaviours and this leads to a much more complex notion of correctness than in [13]. Furthermore, the analysis is parameterised on the choice of value space thereby incorporating ideas from abstract interpretation.

2 Behaviours

Full details of the syntax of CML are not necessary for the developments of the present paper. It will suffice to introduce a running example and to use it to motivate the process algebra of CML.

Example 2.1 Suppose we want to define a program pipe [f1,f2,f3] in out that constructs a pipeline of processes: the sequence of inputs is taken over channel in, the sequence of outputs is produced over channel out and the functions f1, f2, f3 (and the identity function id defined by fn x => x) are applied in turn. To achieve concurrency we want separate processes for each of the functions f1, f2, f3 (and id). This system might be depicted graphically as follows:

  [figure: f1; f2; f3; id; in; ch1; ch2; ch3; out; fail; fail; fail; fail]

Here ch1, ch2, and ch3 are new internal channels for interconnecting the processes; and fail is a channel over which failure of operation may be reported.

Taking the second process as an example it may be created by the CML expression node f2 ch1 ch2 where the function node is given by

     fn f => fn in => fn out =>
     fork_{π} (rec loop d =>
           sync (choose [wrap (receive in,
                               fn x => sync (send (out, f x));
                                      loop d),
                         send(fail,())]))

Here f is the function to be applied, in is the input channel and out is the output channel. The function fork_{π} creates a new process labelled π that performs as described by the recursive function loop that takes the dummy parameter d. In each recursive call the function may either report failure by send(fail,()) or it may perform one step of the processing: receive the input by means of receive in, take the value x received and transmit the modified value f x by means of send(out,f x) after which the process repeats itself by means of loop d. The primitive choose allows to perform an unspecified choice between the two communication possibilities and wrap allows to modify a communication by postprocessing the value received or transmitted. The sync primitive enforces synchronisation at the right points and we refer to [16] for a discussion of the language design issues involved in this; once we have arrived at the process algebra such considerations will be of little importance to us.

The overall construction of the network of processes is then the task of the pipe function defined by

     rec pipe fs => fn in => fn out =>
     if isnil fs
     then node (fn x => x) in out
     else let ch = channel ()
          in (node (hd fs) in ch; pipe (tl fs) ch out)

Here fs is the list of functions to be applied, in is the input channel, and out is the output channel. If the list of functions is empty we connect in and out by means of a process that applies the identity function; otherwise we create a new internal channel by means of channel () and then we create the process for the first function in the list and then recurse on the remainder of the list.

The process algebra of CML [13] allows to give succinct representations of the communications taking place in CML programs. The terms of the process algebra are called behaviours, denoted b ∈ Beh, and are given by

b ::= ϵ | L!t | L?t | t chan_{L} | β | fork_{L} b | b_{1}; b_{2} | b_{1} + b_{2} | recβ. b

where L⊆Labels is a non-empty and finite set of program labels. The behaviour ϵ is associated with the pure functional computations of CML. The behaviours L!t and L?t are associated with sending and receiving values of type t over channels with label in L, the behaviour t chan_{L} is associated with creating a new channel with label in L and over which values of type t can be communicated, and the behaviour fork_{L} b is associated with creating a new process with behaviour b and with label in L. Together these behaviours constitute the atomic behaviours, denoted p ∈ ABeh, as may be expressed by setting

p ::= ϵ | L!t | L?t | t chan_{L} | fork_{L} b

Finally, behaviours may be composed by sequencing (as in b_{1}; b_{2}) and internal choice (as in b_{1} + b_{2}) and we use behaviour variables together with an explicit rec construct to express recursive behaviours.

The structure of the types, denoted t ∈ Typ, shall be of little concern to us in this paper and we shall therefore leave it mostly unspecified (but see [13]); however, we need to state that α chan_{L} is the type of a channel with label in L over which elements of type α may be communicated. Since types might conceivably contain behaviours the notion of free variables needs to be replaced by a notion of exposed variables: we shall say that a behaviour variable β is exposed in a behaviour b if it has a free occurrence that is not a subterm of any type mentioned in b.

Example 2.2 Assuming that fail is a channel of type unit chan_{L} the type inference system of [13] can be used to prove that pipe has type

(α →^{β} α) list →^{ϵ} α chan_{L_{1}} →^{ϵ} α chan_{L_{2}} →^{b} unit

where b is

recβ′.(fork_{π}(recβ′′.(L_{1}?α; ϵ; L_{2}!α; β′′ + L!unit))
+α chan_{L_{1}}; fork_{π}(recβ′′.(L_{1}?α; β; L_{2}!α; β′′ + L!unit)); β′)

Thus the behaviour expresses directly that the pipe function is recursively defined and that it either spawns a single process or creates a channel, spawns a process and recurses. The spawned processes will all be recursive and they will either report failure over a channel in L and terminate, or else input over a channel in L_{1}, do something (as expressed by ϵ and β), output over a channel in L_{2} and recurse.

The semantics of behaviours is defined by a transition relation of the form

P B ⟹_{ps}^{a} P B′

where P B and P B′ are mappings from process identifiers to closed behaviours and the special symbol √ denoting termination. Furthermore, a is an action that takes place and ps is a list of the processes that take part in the action. The actions rather closely correspond to atomic behaviours and are given by

a ::= ϵ | L!t?L | t chan_{L} | fork_{L} b

If the transition P B ⟹_{ps}^{a} P B′ has a = ϵ this means that one of the behaviours in P B performed some internal computation that did not involve communication; in other words it performed the atomic behaviour ϵ. If a = L!t?L this means that two disctinct behaviours performed a communication: one performed the atomic behaviour L!t and the other the atomic behaviour L?t. Finally if a = chan_{L} or a = fork_{L} this means that one of the behaviours in P B allocated a new channel or forked a new process. Since we have covered all possibilities of atomic behaviours we have also covered all possibilities of actions. We refer to [13] for the precise details of the semantics as these are of little importance for the development of the analyses.

3 Value Spaces

In the analyses we want to predict the number of times certain events may happen. The precision as well as the complexity of the analyses will depend upon how we count so we shall parameterise the formulation of the analyses on our notion of counting.

This amounts to abstracting the non-negative integers N by a complete lattice (Abs, ⊑). As usual we write ⊥ for the least element, ⊤ for the greatest element, ⨆ and ⊔ for least upper bounds by a function and ⊓ for greatest lower bounds. The abstraction is expressed

R : N →_{m} Abs that is strict (has R(0) = ⊥) and monotone (has R(n_{1}) ⊑ R(n_{2}) whenever n_{1} ≤ n_{2}); hence the ordering on the natural numbers is reflected in the abstract values. Three elements of Abs are of particular interest and we shall introduce special syntax for them:

o = R(0) = ⊥  i = R(1)  m = ⊤

We cannot expect our notion of counting to be precisely reflected by Abs; indeed it is likely that we shall allow to identify for example R(2) and R(3) and perhaps even R(1) and R(2). However, we shall ensure throughout that no identifications involve R(0) by demanding that R^{−1}(o) = {0} so that o really represents “did not happen”.

We shall be interested in two binary operations on the non-negative integers. One is the operation of maximum: max{n_{1}, n_{2}} is the larger of n_{1} and n_{2}. In Abs we shall use the binary least upper bound operation to express the maximum operation. Indeed R(max{n_{1}, n_{2}}) = R(n_{1})⊔ R(n_{2}) holds by monotonicity of R as do the laws n_{1} ⊑ n_{1}⊔n_{2}, n_{2} ⊑ n_{1}⊔n_{2} and n⊔n = n. As a consequence n_{1}⊔n_{2} = o iff both n_{1} and n_{2} equal o.

The other operation is addition: n_{1} + n_{2} is the sum of n_{1} and n_{2}. In Abs we shall have to define a function ⊕ and demand that (Abs, ⊕, o) is an Abelian monoid with ⊕ monotone. This ensures that we have the associative law n_{1} ⊕ (n_{2} ⊕ n_{3}) = (n_{1} ⊕ n_{2}) ⊕ n_{3}, the absorption laws n ⊕ o = o ⊕ n = n, the commutative law n_{1} ⊕ n_{2} = n_{2} ⊕ n_{1} and by monotonicity we have also the laws n_{1} ⊑ n_{1} ⊕ n_{2} and n_{2} ⊑ n_{1} ⊕ n_{2}. As a consequence n_{1} ⊕ n_{2} = o iff both n_{1} and n_{2} equal o. To ensure that ⊕ models addition on the integers we impose the condition ∀n_{1}, n_{2}. R(n_{1} + n_{2}) ⊑ R(n_{1}) ⊕ R(n_{2}) that is common in abstract interpretation.

Definition 3.1 A value space is a structure (Abs, ⊑, o, i, m, ⊕, R) as detailed above. It is an atomic value space if i is an atom (that is o ⊑ n ⊑ i implies that o = n or i = n). Example 3.2 One possibility is to use A3 = {o, i, m} and define ⊑ by o ⊑ i ⊑ m. The abstraction function R will then map 0 to o, 1 to i and all other numbers to m. The operations ⊔ and ⊕ can then be given by the following tables:

⊔ o i m
o o i m
i i i m
m m m m

⊕ o i m
o o i m
i i m m
m m m m

This defines an atomic value space. For two value spaces (Abs′, ⊑′, o′, i′, m′, ⊕′, R′) and (Abs′′, ⊑′′, o′′, i′′, m′′, ⊕′′, R′′) we may construct their cartesian product (Abs, ⊑, o, i, m, ⊕, R) by setting Abs = Abs′ × Abs′′ and by defining ⊑, o, i, m, ⊕ and R componentwise. This defines a value space but it is not atomic even if Abs′ and Abs′′ both are. As a consequence i = (i′, i′′) will be of no concern to us; instead we use (o′, i′′) and (i′, o′′) as appropriate.

For a value space (Abs′, ⊑′, o′, i′, m′, ⊕′, R′) and a non-empty set E of events we may construct the indexed value space (or function space) (Abs, ⊑, o, i, m, ⊕, R) by setting Abs = E → Abs′ (the set of total functions from E to Abs′) and by defining ⊑, o, i, m, ⊕ and R componentwise. This defines a value space that is almost never atomic; as a consequence i = λe.i′ will be of no concern to us.

For indexed value spaces we may represent (f ∈ E → Abs) by (rep(f) ∈ E ↪ Abs\{o}) where E ↪ Abs\{o} denotes the set of partial functions from E to Abs\{o}; here rep(f) maps e to n iff f(e) = n and n ≠ o. In practice we want to restrict E to be a finite set in order to obtain finite representations; we write (f ∈ E →_{f} Abs) to indicate that f is o on all but a finite number of arguments so that such a representation is possible.

4 Counting the Behaviours

For a given behaviour b and value space Abs we may ask the following four questions:

benv ⊢ ϵ : [ ]
benv ⊢ L!t : [L ↦ (o, o, i, o)]  benv ⊢ L?t : [L ↦ (o, i, o, o)]
benv ⊢ t chan_{L} : [L ↦ (i, o, o, o)] \frac{benv ⊢ b : A}{benv ⊢ fork_{L} b : [L ↦ (o, o, o, i)] ⊕ A}
\frac{benv ⊢ b_{1} : A_{1} benv ⊢ b_{2} : A_{2}}{benv ⊢ b_{1}; b_{2} : A_{1} ⊕ A_{2}}  \frac{benv ⊢ b_{1} : A_{1} benv ⊢ b_{2} : A_{2}}{benv ⊢ b_{1} + b_{2} : A_{1}⊔A_{2}}
\frac{benv[β ↦ A] ⊢ b : A}{benv ⊢ rec β. b : A}  benv ⊢ β : A if benv(β) = A

Table 1: Analysis of behaviours

how many times are channels labelled by L created?

how many times do channels labelled by L participate in input? how many times do channels labelled by L participate in output? and how many times are processes labelled by L generated?

To answer these questions we define an inference system with formulae

benv ⊢ b : A

where LabSet = P_{f}(Labels) is the set of finite and non-empty subsets of Labels and A ∈ LabSet →_{f} Abs records the required information.

In this section we shall define the inference system for answering all four questions simultaneously. Hence we let Abs be the four-fold cartesian product Ab^{4} of an atomic value space Ab; we shall leave the formulation parameterised on the choice of Ab but a useful candidate is the three-element value space A3 of Example 3.2 and this will be the choice in all examples.

The idea is that A(L) = (n_{c}, n_{i}, n_{o}, n_{f}) means that channels labelled by L are created at most n_{c} times, that channels labelled by L participate in at most n_{i} input operations, that channels labelled by L participate in at most n_{o} output operations, and that processes labelled by L are generated at most n_{f} times. The behaviour environment benv then associates each behaviour variable with an element of LabSet →_{f} Abs.

The analysis is defined in Table 1. We use [ ] as a shorthand for λL.(o, o, o, o)

and [L ↦ n⃗] as a shorthand for λL′. \{ \begin{matrix}(o, o, o, o) & if L′ ≠ L \\ n⃗ & if L′ = L \end{matrix} \}. Note that i

denotes the designated “one”-element in each copy of Ab since it is the atoms (i, o, o, o), (o, i, o, o), (o, o, i, o), and (o, o, o, i) that are useful for increasing the count. In the rule for fork_{L} we are deliberately incorporating the effects of the forked process; to avoid doing so simply remove the “⊕A” component. The rules for sequencing, choice, and behaviour variables are straightforward given the developments of the previous section.

Note that the rule for recursion expresses a fixed point property and so allows some slackness; it would be inelegant to specify a least (or greatest) fixed point property whereas a post-fixed point^{1} could easily be accomodated by incorporating a notion of subsumption into the rule. We decided not to incorporate a general subsumption rule and to aim for specifying as unique results as the rule for recursion allows.

Example 4.1 For the pipe function of Examples 2.1 and 2.2 the analysis will give the following information (read “m” as “many”):

L_{1}: m channels created and m inputs performed
L_{2}: m outputs performed
L: m outputs performed
π: m processes created

While this is evidently correct it also seems pretty uninformative; yet we shall see that this simple analysis suffices for developing more informative analyses for static and dynamic processor allocation.

To formally express the correctness of the analysis we need a few definitions. Given a list X of actions define:

COUNT(X) = λL.(CC(X, L), CI(X, L), CO(X, L), CF (X, L))

CC(X, L): the number of elements of the form t chan_{L} in X,
CI(X, L): the number of elements of the form L′!t?L in X,
CO(X, L): the number of elements of the form L!t?L′ in X, and
CF (X, L): the number of elements of the form fork_{L} b in X.

The formal version of our explanations above about the intentions with the analysis then amounts to the following soundness result:

Theorem 4.2 If ∅ ⊢ b : A and [pi_{0} ↦ b] ⟹_{ps_{1}}^{a_{1}} … ⟹_{ps_{k}}^{a_{k}} P B then we have

R^{∗}(COUNT[a_{1}, ⋯, a_{k}]) ⊑ A.

where R^{∗}(C)(L) = (R(c), R(i), R(o), R(f)) if C(L) = (c, i, o, f).

5 Implementation

It is well-known that compositional specifications of program analyses (whether as abstract interpretations or annotated type systems) are not the most efficient way of obtaining the actual solutions. We therefore demonstrate how the inference problem may be transformed to an equation solving problem that is independent of the syntax of our process algebra and where standard algorithmic techniques may be applied. This approach also carries over to the inference systems for processor allocation developed subsequently.

The first step is to generate the set of equations. To show that this does not affect the set of solutions we shall be careful to avoid undesirable “crossover” between equations generated from disjoint syntactic components of the behaviour. One possible cause for such “cross-over” is that behaviour variables E[[B : ϖ : ϵ]] = {⟨ϖ⟩ = [ ] }

1We take a post-fixed point of a function f to be an argument n such that f(n) ⊑ n.

E[[B : ϖ : L!t]] = {⟨ϖ⟩ = [L ↦ (o, o, i, o)] }

E[[B : ϖ : L?t]] = {⟨ϖ⟩ = [L ↦ (o, i, o, o)] }

E[[B : ϖ : t chan_{L}]] = {⟨ϖ⟩ = [L ↦ (i, o, o, o)] }

E[[B : ϖ : fork_{L} b]] = {⟨ϖ⟩ = [L ↦ (o, o, o, i)] ⊕ ⟨ϖ1⟩ } ∪ E[[B : ϖ1 : b]]

E[[B : ϖ : b_{1}; b_{2}]] = {⟨ϖ⟩ = ⟨ϖ1⟩ ⊕ ⟨ϖ2⟩ } ∪ E[[B : ϖ1 : b_{1}]] ∪ E[[B : ϖ2 : b_{2}]]

E[[B : ϖ : b_{1} + b_{2}]] = {⟨ϖ⟩ = ⟨ϖ1⟩⊔⟨ϖ2⟩ } ∪ E[[B : ϖ1 : b_{1}]] ∪ E[[B : ϖ2 : b_{2}]]

E[[B : ϖ : β]] = {⟨ϖ⟩ = ⟨β⟩ }

E[[B : ϖ : rec β. b]] = CLOSEβ^{ϖ}( {⟨ϖ⟩ = ⟨ϖ1⟩, ⟨ϖ⟩ = ⟨β⟩ } ∪ E[[B : ϖ1 : b]] )

Table 2: Constructing the equation system

may be bound in more than one rec; one classical solution to this is to require that the overall behaviour be alpha-renamed such that this does not occur; the solution we adopt avoids this requirement by suitable modification of the equation system. Another possible cause for “cross-over” is that disjoint syntactic components of the overall behaviour may nonetheless have components that syntactically appear the same; we avoid this problem by the standard use of tree-addresses (denoted ϖ).

The function E for generating the equations for the overall behaviour B achieves this by the call E[[B : ε : b]] where ε denotes the empty tree-address. In general B : ϖ : b indicates that the subtree of B rooted at ϖ is of the form b and the result of E[[B : ϖ : b]] is the set of equations produced for b. The formal definition is given in Table 2.

The key idea is that E[[B : ϖ : b]] operates with flow variables of the form ⟨ϖ′⟩ and ⟨β′⟩. We maintain the invariant that all ϖ′ occurring in E[[B : ϖ : b]] are (possibly empty) prolongations of ϖ and that all β′ occurring in E[[B : ϖ : b]] are exposed in b. To maintain this invariant in the case of recursion we define

CLOSEβ^{ϖ}(E) = { (L[⟨ϖ⟩/⟨β⟩] = R[⟨ϖ⟩/⟨β⟩]) | (L = R) ∈ E }

(although it would actually suffice to apply the substitution [⟨ϖ⟩/⟨β⟩] on the righthand sides of equations and it would be correct to remove the trivial equation produced).

Terms of the equations are formal terms over the flow variables (that range over the complete lattice LabSet → Abs), the operations ⊕ and ⊔ and the constants (that are elements of the complete lattice LabSet → Abs). Thus all terms are monotonic in their free flow variables. A solution to a set E of equations is a partial function σ from flow variables to LabSet → Abs such that all flow variables in E are in the domain of σ and such that all equations (L = R) of E have σ(L) = σ(R) where σ is extended to formal terms in the obvious way. We write σ ⊧ E whenever this is the case.

Theorem 5.1 [ ] ⊢ b : A iff ∃σ. σ ⊧ E[[b : ε : b]] ∧ σ(⟨ε⟩) = A.

Corollary 5.2 The least (or greatest) A such that [ ] ⊢ b : A is σ(⟨ε⟩) for the least (or greatest) σ such that σ ⊧ E[[b : ε : b]].

We have now transformed our inference problem to a form where the standard algorithmic techniques can be exploited. These include simplifications of the equation system, partitioning the equation system into strongly connected components processed in (reverse) topological order, widening to ensure convergence when Abs does not have finite height etc.; a good overview of useful techniques may be found in [2, 7, 10, 17]. Also the flow variables may be decomposed to families of flow variables over simpler value spaces.

6 Static Processor Allocation

The idea behind the static processor allocation is that all processes with the same label will be placed on the same processor and we would therefore like to know what requirements this puts on the processor. To obtain such information we shall extend the simple counting analysis of Section 4 to associate information with the process labels mentioned in a given behaviour b. For each process label L_{a} we therefore ask the four questions of Section 4 accumulating the total information for all processes with label L_{a}: how many times are channels labelled by L created, how many times do channels labelled by L participate in input, how many times do channels labelled by L participate in output, and how many times are processes labelled by L generated?

Example 6.1 Let us return to the pipe function of Examples 2.1 and 2.2 and suppose that we want to perform static processor allocation. This means that all instances of the processes labelled π will reside on the same processor. The analysis should therefore estimate the total requirements of these processes as follows:

main: L_{1}: m channels created π: L_{1}: m inputs performed
π: m processes created  L_{2}: m outputs performed
L: m outputs performed

Note that even though each process labelled by π can only communicate once over L we can generate many such processes and their combined behaviour is to communicate many times over L. It follows from this analysis that the main program does not in itself communicate over L_{2} or L and that the processes do not by themselves spawn new processes.

Now suppose we have a network of processors that may be explained graphically as follows:

[figure: P2; P3; P1]

One way to place our processes is to place the main program on P1 and all the processes labelled π on P2. This requires support for multitasking on P2 and for multiplexing (over L_{1}) on P1 and P2.

The analysis (specified in Table 3) is obtained by modifying the inference system of Section 4 to have formulae

benv ⊢ b : A & P

where A ∈ LabSet →_{f} Abs as before and the new ingredient is

P : LabSet →_{f} (LabSet →_{f} Abs)

The idea is that if some process is labelled L_{a} then P (L_{a}) describes the total requirements of all processes labelled by L_{a}. The behaviour environment benv is an extension of that of Section 4 in that it associates pairs A & P with the behaviour variables. Note that in the rule for fork_{L} we have removed the “⊕A” component from the local effect; instead it is incorporated in the global effect for L.

To express the correctness of the analysis we need to keep track of the relationship between the process identifiers and the associated labels. So let penv be a mapping from process identifiers to elements L_{a} of LabSet. We shall say that penv respects the derivation sequence P B ⟹_{ps_{1}}^{a_{1}} … ⟹_{ps_{k}}^{a_{k}} P B′ if whenever (a_{i}, ps_{i}) have the form (fork_{L} b, (pi_{1}, pi_{2})) then penv(pi_{2}) = L; this ensures that the newly created process (pi_{2}) indeed has a label (in L) as reported by the semantics.

We can now redefine the function COUNT of Section 4. Given a list X of pairs of actions and lists of process identifiers define

COUNT^{penv}(X) = λL_{a}.λL.(CC_{L_{a}}(X , L), CI_{L_{a}}(X , L), CO_{L_{a}}(X , L), CF_{L_{a}}(X , L))

CC_{L_{a}}(X , L): the number of elements of the form (t chan_{L}, pi) in X
where penv(pi) = L_{a},
CI_{L_{a}}(X , L): the number of elements of the form (L′!t?L, (pi′, pi)) in X,
where penv(pi) = L_{a},
CO_{L_{a}}(X , L): the number of elements of the form (L!t?L′, (pi, pi′)) in X,
where penv(pi) = L_{a}, and
CF_{L_{a}}(X , L): the number of elements of the form (fork_{L}b, (pi, pi′)) in X
where penv(pi) = L_{a}.

Soundness of the analysis then amounts to:

benv ⊢ ϵ : [ ] & [ ]
benv ⊢ L!t : [L ↦ (o, o, i, o)] & [ ]
benv ⊢ L?t : [L ↦ (o, i, o, o)] & [ ]
benv ⊢ t chan_{L} : [L ↦ (i, o, o, o)] & [ ]

\frac{benv ⊢ b : A & P}{benv ⊢ fork_{L} b : [L ↦ (o, o, o, i)] & ([L ↦ A] ⊕ P)}

\frac{benv ⊢ b_{1} : A_{1} & P_{1} benv ⊢ b_{2} : A_{2} & P_{2}}{benv ⊢ b_{1}; b_{2} : A_{1} ⊕ A_{2} & P_{1} ⊕ P_{2}}

\frac{benv ⊢ b_{1} : A_{1} & P_{1} benv ⊢ b_{2} : A_{2} & P_{2}}{benv ⊢ b_{1} + b_{2} : A_{1}⊔A_{2} & P_{1}⊔P_{2}}

\frac{benv[β ↦ A & P] ⊢ b : A & P}{benv ⊢ rec β. b : A & P}

benv ⊢ β : A & P if benv(β) = A & P

Table 3: Analysis for static process allocation

Theorem 6.2 Assume that ∅ ⊢ b : A & P and [pi_{0} ↦ b] ⟹_{ps_{1}}^{a_{1}} … ⟹_{ps_{k}}^{a_{k}} P B and let penv be a mapping from process identifiers to elements of LabSet respecting the above derivation sequence and such that penv(pi_{0}) = L_{0}. We then have

R^{∗}(COUNT^{penv}[(a_{1}, ps_{1}), ⋯, (a_{k}, ps_{k})]) ⊑ (P ⊕ [L_{0} ↦ A])

where R^{∗}(C)(L_{a})(L) = (R(c), R(i), R(o), R(f)) if C(L_{a})(L) = (c, i, o, f).

Note that the lefthand side of the inequality counts the number of operations for all processes whose labels is given (by L_{a}); hence our information is useful for static processor allocation.

To obtain an efficient implementation of the analysis it is once more profitable to generate an equation system. This is hardly any different from the approach of Section 5 except that by now there is even greater scope for decomposing the flow variables into families of flow variables over simpler value spaces.

7 Dynamic Processor Allocation

The idea behind the dynamic processor allocation is that the decision of how to place processes on processors is taken dynamically. Again we will be interested in knowing which requirements this puts on the processor but in contrast to the previous section we are only concerned with a single process rather than all processes with a given label. We shall now modify the analysis of Section 6 to associate worst-case information with the process labels rather than accumulating the total information. For each process label L_{a} we therefore ask the four

\frac{benv ⊢ b : A & P}{benv ⊢ fork_{L} b : [L ↦ (o, o, o, i)] & ([L ↦ A]⊔P)}

\frac{benv ⊢ b_{1} : A_{1} & P_{1} benv ⊢ b_{2} : A_{2} & P_{2}}{benv ⊢ b_{1}; b_{2} : A_{1} ⊕ A_{2} & P_{1}⊔P_{2}}

\frac{benv[β ↦ A] ⊢ b : A & P}{benv ⊢ rec β. b : A & P}

benv ⊢ β : A & [ ] if benv(β) = A

Table 4: Analysis for dynamic process allocation

questions of Section 4 taking the maximum information over all processes with label L_{a}: how many times are channels labelled by L created, how many times do channels labelled by L participate in input, how many times do channels labelled by L participate in output, and how many times are processes labelled by L generated?

Example 7.1 Let us return to the pipe function of Examples 2.1 and 2.2 and suppose that we want to perform dynamic processor allocation. This means that all the processes labelled π need not reside on the same processor. The analysis should therefore estimate the maximal requirements of the instances of these processes as follows:

main: L_{1}: m channels created π: L_{1}: m inputs performed
π: m processes created  L_{2}: m outputs performed
L: i output performed

Note that now we do record that each individual process labelled by π actually only communicates over L at most once.

Returning to the processor network of Example 6.1 we may allocate the main program on P1 and the remaining processes on P2 and P3 (and possibly P1 as well): say f1 and f3 on P2 and f2 and id on P3. Facilities for multitasking are needed on P2 and P3 and facilities for multiplexing on all of P1, P2 and P3.

The inference system still has formulae

benv ⊢ b : A & P

where A and P are as in Section 6 and now benv is as in Section 4: it does not incorporate the P component^{2}. Most of the axioms and rules are as in Table 3; the modifications are listed in Table 4.

A difference from Section 6 is that now we need to keep track of the individual process identifiers. We therefore redefine the function COUNT^{penv} as follows:

2It could be as in Section 6 as well because we now combine P components using ⊔ rather than ⊕.

COUNT^{penv}(X) = λL_{a}.λL.((CC_{P I}(X , L), CI_{P I}(X , L), CO_{P I}(X , L), CF_{P I}(X , L)) where P I = penv^{−1}(L_{a}))

CC_{P I}(X , L): the maximum over all pi ∈ P I of the number of elements
of the form (t chan_{L}, pi) in X,
CI_{P I}(X , L): the maximum over all pi ∈ P I of the number of elements
of the form (L′!t?L, (pi′, pi)) in X,
CO_{P I}(X , L): the maximum over all pi ∈ P I of the number of elements
of the form (L!t?L′, (pi, pi′)) in X, and
CF_{P I}(X , L): the maximum over all pi ∈ P I of the number of elements
of the form (fork_{L}b, (pi, pi′)) in X.

Soundness of the analysis then amounts to:

Theorem 7.2 Assume that ∅ ⊢ b : A & P and [pi_{0} ↦ b] ⟹_{ps_{1}}^{a_{1}} … ⟹_{ps_{k}}^{a_{k}} P B and let penv be a mapping from process identifiers to elements of LabSet respecting the above derivation sequence and such that penv(pi_{0}) = L_{0}. We then have

R^{∗}(COUNT^{penv}[(a_{1}, ps_{1}), ⋯, (a_{k}, ps_{k})]) ⊑ (P ⊔[L_{0} ↦ A])

where R^{∗} is as in Theorem 6.2.

Note that the lefthand side of the inequality gives the maximum number of operations over all processes with a given label; hence our information is useful for dynamic processor allocation.

To obtain an efficient implementation of the analysis it is once more profitable to generate an equation system and the remarks at the end of the previous section still apply.

8 Conclusion

The specifications of the analyses for static and dynamic allocation have much in common; the major difference of course being that for static processor allocation we accumulate the total numbers whereas for dynamic processor allocation we calculate the maximum; a minor difference being that for the static analysis it was crucial to let behaviour environments include the P component whereas for the dynamic analysis this was hardly of any importance.

This difference in approach is reminiscent of the difference between the formulation of MFP-style and MOP-style analyses: in the former the effects of paths (corresponding to process identifiers with the same label set) are merged along the way whereas in the latter the paths (corresponding to the process identifiers) have to be kept separate and their effects can only be merged when the propagation of effects has taken place.

Acknowledgements. We would like to thank Torben Amtoft for many interesting discussions. This research has been funded in part by the LOMAPS (ESPRIT BRA) and DART (Danish Science Research Council) projects.

References

[1] T.Amtoft, F.Nielson, H.R.Nielson: Type and behaviour reconstruction for higherorder concurrent programs. This proceedings.

[2] J.Cai, R.Paige: Program Derivation by Fixed Point Computation. Science of Computer Programming 11, pp. 197–261, 1989.

[3] R. Cridlig, E.Goubault: Semantics and analysis of Linda-based languages. Proc. Static Analysis, Springer Lecture Notes in Computer Science 724, 1993.

[4] C.E.McDowell: A practical algorithm for static analysis of parallel programs. Journal of parallel and distributed computing 6, 1989.

[5] A.Giacalone, P.Mishra, S.Prasad: Operational and Algebraic Semantics for Facile: a Symmetric Integration of Concurrent and Functional Programming. Proc. ICALP’90, Springer Lecture Notes in Computer Science 443, 1990.

[6] K.Havelund, K.G.Larsen: The Fork Calculus. Proc. ICALP’93, Springer Lecture Notes in Computer Science 700, 1993.

[7] M.S.Hecht: Flow Analysis of Computer Programs, North-Holland, 1977.

[8] Y.-C.Hung, G.-H.Chen: Reverse reachability analysis: a new technique for deadlock detection on communicating finite state machines. Software — Practice and Experience 23, 1993.

[9] S.Jagannathan, S.Week: Analysing stores and references in a parallel symbolic language. Proc. L&FP, 1994.

[10] M.Jourdan, D.Parigot: Techniques for Improving Grammar Flow Analysis. Proc. ESOP’90, Springer Lecture Notes in Computer Science 432, pp. 240–255, 1990.

[11] N. Mercouroff: An algorithm for analysing communicating processes. Proc. of MFPS, Springer Lecture Notes in Computer Science 598, 1992.

[12] F.Nielson, H.R.Nielson: From CML to Process Algebras. Proc. CONCUR’93, Springer Lecture Notes in Computer Science 715, 1993.

[13] H.R.Nielson, F.Nielson: Higher-Order Concurrent Programs with Finite Communication Topology. Proc. POPL’94, pp. 84–97, ACM Press, 1994.

[14] F.Nielson, H.R.Nielson: Constraints for Polymorphic Behaviours for Concurrent ML. Proc. CCL’94, Springer Lecture Notes in Computer Science 845, 1994.

[15] J.H.Reif, S.A.Smolka: Dataflow analysis of distributed communicating processes. International Journal of Parallel Programs 19, 1990.

[16] J.R.Reppy: Concurrent ML: Design, Application and Semantics. Springer Lecture Notes in Computer Science 693, pp. 165–198, 1993.

[17] R.Tarjan: Iterative Algorithms for Global Flow Analysis. In J.Traub (ed.), Algorithms and Complexity, pp. 91–102, Academic Press, 1976.

[18] B.Thomsen. Personal communication, May 1994.