Elena Giachino
email: giachino@cs.unibo.it

Cosimo Laneve
email: laneve@cs.unibo.it

Towards the typing of resource deployment ⋆

In cloud computing, resources as files, databases, applications, and virtual machines may either scale or move from one machine to another in response to load increases and decreases (resource deployment). We study a type-based technique for analysing the deployments of resources in cloud computing. In particular, we design a type system for a concurrent object-oriented language with dynamic resource creations and movements. The type of a program is behavioural, namely it expresses the resource deployments over periods of (logical) time. Our technique admits the inference of types and may underlie the optimisation of the costs and consumption of resources.

Introduction

One of the prominent features of cloud computing is elasticity, namely the property of letting (almost infinite) computing resources available on demand, thereby eliminating the need for up-front commitments by users. This elasticity may be a convenient opportunity if resources may go and shrink automatically at a fine-grain when user's needs change. However, current cloud technologies do not match this fine-grain requirement. For example, Google AppEngine automatically scales in response to load increases and decreases, but it charges clients by the cycles (type of operations) used; Amazon Web Service charges clients by the hour for the number of virtual machines used, even if a machine is idle [START_REF] Armbrust | A view of cloud computing[END_REF].

Fine-grained resource management is an area where competition between cloud computing providers may unlock new opportunities by committing to more precise cost bounds. In turn, such cost bounds should encourage programmers to pay attention to resource managements (that is, releasing and acquiring resources only when necessary) and allow more direct measurement of operational and development inefficiencies.

In order to let resources, such as files or databases or applications or memories or virtual machines, be deployed in cloud machines, the languages for programming the cloud must include explicit operations for creating, deleting, and moving resourcesresource deployment operations -and corresponding software development kits should include tools for analysing resource usages. It is worth to observe that the leveraging of resource management to the programming language might also open opportunities to implement Service Level Agreements (SLAs) validation via automated test infrastructure, thus offering the opportunity for third-party validation of SLAs and assessing penalties appropriately.

We study resource deployment (in cloud computing) by extending a simple concurrent object-oriented model with lightweight primitives for dynamic resource management. In our model, resources are groups of objects that can be dynamically created and can be moved from one (virtual ) machine to another, called deployment components. We then define a technique for analysing and displaying resource loads in deployment components that is amenable to be prototyped.

The object-oriented language is overviewed in Section 2 by discussing in detail a few examples. In Section 3, we discuss the type system for analysing the resource deployments. Our technique is based on so-called behavioural types that abstractly describe systems' behaviours. In particular, the types we consider record the creations of resources and their movements among deployment components. They are similar to those ranging from languages for session types [START_REF] Gay | Subtyping for session types in the π-calculus[END_REF] to process contracts [START_REF] Laneve | The must preorder revisited[END_REF] and to calculi of processes as Milner's CCS or picalculus [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Milner | A calculus of mobile processes[END_REF]. In our mind, behavioural types are intended to represent a part of SLA that may be validated in a formal way and that support compositional analysis. Therefore they may play a fundamental role in the negotiation phase of cloud computing tradings.

The behavioural types presented in Section 3 are a simple model that may be displayed by highlighting the resource load of deployment components using existing tools. We examine this issue in Section 4. Related works are discussed in Section 5.

The aim of this contribution is to overview our type system for analysing resource deployments. Therefore the style is informal and problems and (our) solutions are discussed by means of examples. The details of the technique, such as the system for deriving behavioural types automatically and the correctness results, can be found in the forthcoming full paper.

dcABS in a nutshell

Our study targets an ABS-like language. ABS [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF] is a basic abstract, executable, object-oriented modelling language with a formal semantics. In this language, method invocations are asynchronous: the caller continues after the invocation and the called code runs on a different task. Tasks are cooperatively scheduled: every group of objects, called cog, has at most one active task at each time. Tasks running on different cogs may be evaluated in parallel, while those running on the same cog must compete for the lock and interleave their evaluation. The active task of a cog explicitly returns the control in order to let other tasks progress. Synchronisations between caller and callee is explicitly performed when callee's result is strictly necessary by using future variables (see [START_REF] De Boer | A complete guide to the future[END_REF] and the references in there).

In our language, which is called dcABS, programmers may define a fixed number of (virtual) cloud computing machines, called deployment components (de- Table 1. A simple dcABS program ployment component do not scale), and may use a very basic management of resources that enables cogs movements from one deployment component to another (cogs represents generic resources, such as group of computing entities, databases, virtual memories and the corresponding management processes). In dcABS, we also assume that method invocations are synchronised in the same method body where they occur, except for the main statement. This constraint largely simplifies the analysis and augment its precision because it reduces the nondeterminism.

We illustrate the main features of dcABS by means of examples. The details of the syntax and semantics of dcABS can be found in the (forthcoming) full paper. Table 1 displays a simple dcABS program. Programs consist of three parts: (i) a collection of class definitions, (ii) a declaration of the deployment components that are available, and (iii) a main statement to evaluate. Classes contain field and method declarations. In the above table, there is one class definition that covers lines 2-6, the deployment components are declared at line 9, and the main statement covers lines 12-20. The evaluation of the main statement is performed in the special cog start that is located on the deployment component that is declared first; in our example this is d0. Lines 15, 16 and 18 display method invocations. As mentioned above, in dcABS invocations are asynchronous: the caller continues executing in parallel with the called method, which runs in a dedicated task within the cog where the receiver object resides. For example, line 15 corresponds to spawning the instance of the body of method m in a new task that is going to run in the cog of the object referred by x1. A future reference to the returned value is stored in the variable f1 that has type Fut<Bool>. This means that the value is not ready yet and, when it will be produced (in the future), it will have type Bool. Line 17 enforces the retrieval of such value by accessing to the corresponding future reference and waiting for its availability, by means of the operation get. Since method invocations are asynchronous, the two invocations in lines 15 and 16 are executed concurrently. The invocation at line 15 is then synchronised at line 17, but the one at line 16 may continue concurrently with the invocation of line 18, until they are both synchronised.

The invocations in the main statement execute three instances of method m. Every instance verifies if the receiver object is co-located with the argument object and, in case, it performs either a deployment to let the corresponding cogs be co-located or a deployment to the component d1. The expression @x of line 4 points to the deployment component where the (cog of the) object referred by x resides.

Table 2 shows a class definition D with a recursive method multi_create. This method creates n new cogs co-located with the caller object and moves them to the deployment component d1.

Analysing the cog-deployment of the programs in Tables 1 and2 is not straightforward. For example, significant questions regarding Table 1 are: (i) what is the cog-load of the component d1 during the lifetime of the main state-ment? (ii) Can the component d0 be garbage-collected after a while in order to optimise resource usages? Let the main statement of Table 2 be // available deployment components declaration: data DCData = d0, d1 ; //main statement:

D x = new cog D() ; Fut<Bool> f = x!multi_create(10) ;
Then, an important question about Table 2 is: (iii) is there an upper bound to the number of cogs deployed to d0? The technique we study in the following sections lets us to answer to such kind of questions in a formal way.

Behavioural types for resource deployment

Our technique for analysing resource deployments in dcABS programs is mostly based on our past experience in designing type inference systems for analysing deadlock-freedom of concurrent (object-oriented) languages [START_REF] Giachino | Deadlock analysis of concurrent objects: Theory and practice[END_REF][START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Giachino | A Framework for Deadlock Detection in ABS[END_REF].

A basic ingredient of every type system is the definition of the association of types with language constructs. The type system of dcABS associates an abstract deployment behaviour to every statement and expression. Formally, the association is defined by the typing judgment

Γ ;n ⊢ c s : ❜ ⊲ Γ ′ ;n ′ (1)
to be read as: in an environment Γ and at a timestamp n, the statement s of an object whose cog is c has a type ❜ and has effects Γ ′ and n ′ . The pair Γ ′ and n ′ is used to type the continuation. To explain (1), consider the line 12 of Table 1:

C x1 = new cog C( ); moveto d1;
The statement C x1 = new cog C( ); has two effects: (i) creating a new colocated cog (with a fresh name, say c 1 ) , and (ii) populating this new cog with a new object whose value is stored in x1. As regards (i), there is a deployment of the new cog at the deployment component where the current cog c resides. We define this behaviour by means of the type

c 1 → c
As regards (ii), we record (in the typing judgment) the name of the cog of x1.

In particular, variable assignment may propagate cog names throughout the program and this may affect the behavioural types. That is, our type system includes the analysis of aliases (c.f. Γ ′ in ( 1) is an update of Γ ). In particular, in order to trace propagations of names, we associate to each variable a so-called future record, ranged over by r and defined in Table 3. A future record may be either (i ) a dummy value --that models primitive types, or (ii ) a record

r ::= --| X | [cog:c, x:r] | fut(r) future record ❜ ::= 0 | c → c ′ n÷n | c → d n÷n | C!m(r) → r ′ m÷n behavioural type | ❜ + ❜ | ❜ ❜ | ❜ m÷n
Table 3. Future records and behavioural types of dcABS name X that represents a place-holder for a value and can be instantiated by substitutions, or (iii ) [cog:c, x :r], which defines an object with its cog name c and the values for fields of the object, or (iv ) fut(r), which is associated to method invocations returning a value with record r. As regards Line 12, since C has no field, we record in the environment Γ ′ of (1) the binding x1: [cog : c 1 ], where c 1 is a fresh cog name.

The statement moveto d1 corresponds to migrating the current cog (i.e. c) to the deployment component d1. This is specified by the type c → d1.

The above ones are the basic deployment informations of our type system. We next discuss the management of method invocations, which is the major difficulty in the design of the type system. In fact, the execution of methods' bodies may change deployment informations and these changes, because invocations are asynchronous, are the main source of imprecision of our analysis. Consider, for example, line 15 of Table 1 15 (This association is defined during the typing of the method body -see below.)

The behavioural type of the invocation

x1!m(x2) is therefore C!m([cog : c 1 ], [cog : c 2 ]) → --where Γ (x1) = [cog : c 1 ] and Γ (x2) = [cog : c 2 ].
There is a relevant feature that is not expressed by the type C!m([cog :

c 1 ], [cog : c 2 ]
) → --. The task corresponding to the invocation x1!m(x2) must be assumed to start when the invocation is evaluated and to terminate when the operation get on the corresponding future is performedcf. line 17. During this interval, the statements of x1!m(x2) may interleave with those of the caller and those of the other method invocations thereincf. line 16. To have a more precise analysis, we label the type of line 15 with the (logical) time interval in which it has an effect on the computation. Namely we write ❜ m÷n , where m and n are the starting and the ending interval points, respectively. Our type system increments logical timestamps in correspondence of 1. cog creations, 2. cog migrations, 3. and synchronisation points (get operations).

For example, the lines 15-20 of the code in Table 1 have associated timestamps As a consequence, the behavioural type of the above code is

C!m(r 1 , r 2 ) → -- n÷n C!m(r 2 , r 3 ) → -- n÷n+1 C!m(r 3 , r 2 ) → -- n+1÷n+2
where r 1 , r 2 and r 3 are the record types of the objects x1, x2, and x3, respectively.

As we will see in Section 4, this will impact on the analysis by letting us to consider all the possible computations.

The syntax of behavioural types ❜ is defined in Table 3. Apart those types that have been already discussed, ❜+❜ ′ defines the abstract behaviour of conditionals, ❜ ❜ ′ corresponds to a juxtaposition of behavioural types, and ❜ m÷n defines a behavioural type ❜ to be executed in the interval m ÷ n. It is worth to notice that it is the combination of intervals that models the sequential and the parallel composition: two disjoint intervals specify two subsequent actions, while two overlapping intervals specify two (possibly) parallel actions. This complies with dcABS semantics where parallelism is not explicit in the syntax, but it is generated by the (asynchronous) invocations of methods.

We next discuss the association of a method behavioural type to a method declaration. To this aim, let us consider lines 3-5 of the code in Table 1:

Bool m (C x) {
if (@this != @x) moveto @x else moveto d1; return true; }

The behaviour of m in C is given by (r, r ′ ) {❜ m } → --, where r and r ′ are the future records of the receiver of the method and of the argument, respectively, ❜ m is the type of the body and --is the future record of the returned boolean value. The records r and r ′ are formal parameters of m. Therefore, it is always the case that cog and record names in r and r ′ do occur linearly and bind the occurrences of names in ❜ m . It is worth to notice that cog names occurring in ❜ m may be not bound. These free names correspond to new cog instructions.

In the case of m in C, its type is:

([cog : c], [cog : c ′ ]){ c → c ′ 1÷1 + c → d1 1÷1 } → --.
The behavioural type for the the main statement of Table 1 is:

c 1 → start 1÷1 start → d1 2÷2 c 2 → start 3÷3 start → d2 4÷4 c 3 → start 5÷5 start → d3 6÷6 C!m([cog : c 1 ], [cog : c 2 ]) → -- 7÷7 C!m([cog : c 2 ], [cog : c 3 ]) → -- 7÷8 C!m([cog : c 3 ], [cog : c 2 ]) → -- 8÷9 .
We conclude this section with the typing of the code in Table 2. Method move in D has type:

([cog : c]) { c → d1 1÷1 } → -- Method multi_create in D has type: ([cog : c], --) { (2) 0 + c ′ → c 1÷1 D!multi create([cog : c ′ ], --) → -- 2÷2 D!move([cog : c ′ ]) → -- 3÷3 } → --
We notice that the then-branch is typed with 0. In fact, it does not affect the method behaviour since it does not contain any deployment information nor method invocation.

Analysis of behavioural types

The analysis of behavioural types defined in Section 3 highlights the trend of cog numbers running in each deployment component over a period of (logical) time. More specifically, behavioural types are used to compute the abstract states of a system that record the deployment of cogs with respect to components. The component load is then obtained by projecting out the number of cogs in a state, which can be visualised by means of a standard graphic plotter program. A primary item of this programme is the definition of the semantics of behavioural types. To this aim we use deployment environments Σ that map cog names to sets of deployment components. For example [start → {d0}] is the initial deployment environment. Behavioural types' semantics is defined by means of a transition system where states are triples Σ, ❜, n and transitions Σ, ❜, n m÷m ′ -→ Σ ′ , ❜ ′ , n ′ are defined inductively according to the structure of ❜. The basic rules of the transition relation are

(MoveTo-c) Σ, c → c ′ m÷m , n m÷m -→ Σ[c → Σ(c ′ )], 0, max (m, n) (MoveTo-d) Σ, c → d m÷m , n m÷m -→ Σ[c → {d}], 0, max (m, n) (Invk) C.m = (r){❜m}r ′ var (❜m) \ var (r, r ′ ) = c c ′ are fresh ❜m[ c ′ / c ][ s, s ′ / r, r ′ ] = ❜ ′ Σ, C!m(s) → s ′ m÷m ′ , n m÷m ′ -→ Σ, ❜ ′ m÷m ′ , max (m, n)
The rules (MoveTo-c) and (MoveTo-d) update the deployment environment and return a null behavioural type. Rule (Invk) deals with method invocations and, apart from instantiating the formal parameters with the actual ones, it creates fresh cog names that correspond to the new cog operations in the method body. The inductive rules (that are omitted in this paper) lift the above transitions to structured behavioural types. In particular, let m ÷ n m ′ ÷ n ′ if and only if n < m ′ ( is a partial order). The rule for

❜ 1 • • • ❜ k enables a transition m÷n -→ provided m ÷ n is -minimal in the set of transitions of ❜ 1 , • • • , ❜ k .
In order to illustrate the operational semantics of behavioural types we discuss the transitions of the type of the main statement in Table 1:

❜ 0 = c 1 → start 1÷1 start → d1 2÷2 c 2 → start 3÷3 start → d2 4÷4 c 3 → start 5÷5 start → d3 6÷6 C!m([cog : c 1 ], [cog : c 2 ]) → -- 7÷7 C!m([cog : c 2 ], [cog : c 3 ]) → -- 7÷8 C!m([cog : c 3 ], [cog : c 2 ]) → -- 8÷9 . Let Σ 0 = [start → d0].
According to the semantics of behavioural types, we have

Σ0 , ❜0, 0 1÷1 -→ Σ1 , ❜1, 1 2÷2 -→ Σ2 , ❜2, 2 3÷3 -→ Σ3 , ❜3, 3 4÷4 -→ Σ4 , ❜4, 4 5÷5 -→ Σ5 , ❜5, 5 6÷6 -→ Σ6 , ❜6, 6
where, at each step 1 ≤ i ≤ 6, the type that is evaluated is the one with interval i ÷ i, the deployment environment

Σ 6 is [start → {d3}, c 1 → {d0}, c 2 → {d1}, c 3 → {d2}], and the type ❜ 6 is C!m([cog : c 1 ], [cog : c 2 ]) → --7÷7 C!m([cog : c 2 ], [cog : c 3 ]) → -- 7÷8 C!m([cog : c 3 ], [cog : c 2 ]) → -- 8÷9 .
In Figure 1 we have drawn the computations starting at Σ 6 , ❜ 6 , 6 . Here we discuss the rightmost computation. In Σ 6 , ❜ 6 , 6 , the two transitions that are possible are the method invocations with intervals 7 ÷ 7 and 7 ÷ 8. We perform the one with interval 7 ÷ 8 and, by rule (Invk), we get Σ 6 , ❜ 8 , 7 , where

❜ 8 = C!m([cog : c 1 ], [cog : c 2 ]) → --7÷7 c 2 → c 3 1÷1 + c 2 → d1 1÷1 7÷8 C!m([cog : c 3 ], [cog : c 2 ]) → -- 8÷9 . Σ6 , ❜6
Σ 8 is [start → {d3}, c 1 → {d0}, c 2 → {d2}, c 3 → {d2}]. and ❜ 11 is C!m([cog : c 1 ], [cog : c 2 ]) → -- 6÷6 C!m([cog : c 3 ], [cog : c 2 ]) → -- 7÷8 .
In Σ 8 , ❜ 11 , 7 only one transition is possible: the method invocation with interval 7÷7. Therefore one has Σ 8 , ❜ 14 , 7 , where

❜ 14 = c 1 → c 2 1÷1 + c 1 → d1 1÷1 7÷7 C!m([cog : c 3 ], [cog : c 2 ]) → -- 8÷9 .
In the state Σ 8 , ❜ 14 , 7 the possible transitions are those of the type

c 1 → c 2 1÷1 + c 1 → d1 1÷1 7÷7 . By letting c 1 → d1 1÷1 move, one has Σ 11 , ❜ 17 , 7 , where Σ 11 = [start → {d3}, c 1 → {d1}, c 2 → {d2}, c 3 → {d2}] and ❜ 17 = C!m([cog : c 3 ], [cog : c 2 ]) → --8÷9 .
Finally, by performing two transitions labelled 8 ÷ 9, one first unfolds the method invocation and then evaluates the corresponding body

c 3 → c 2 1÷1 + c 3 → d1 1÷1 8÷9
. By letting c 3 → d1 1÷1 move, the computation terminates with a deployment environment

Σ 13 = [start → {d3}, c 1 → {d1}, c 2 → {d2}, c 3 → {d1}].
Given a transition system T as the one illustrated in Figure 1, it is possible to compute the abstract trace, i.e. the sequence Σ(0

) • Σ(1) • Σ(2) • • • where Σ(i) is the deployment environment Σ(i) : c → ∪{Σ(c) | there is ❜ such that Σ, ❜, i ∈ T } .
For example, letting the deployment environments of Figure 1 be

Σ 6 = [start → {d3}, c 1 → {d0}, c 2 → {d1}, c 3 → {d2}] Σ 7 = [start → {d3}, c 1 → {d1}, c 2 → {d1}, c 3 → {d2}] Σ 8 = [start → {d3}, c 1 → {d0}, c 2 → {d2}, c 3 → {d2}] Σ 9 = [start → {d3}, c 1 → {d1}, c 2 → {d1}, c 3 → {d1}] Σ 10 = [start → {d3}, c 1 → {d1}, c 2 → {d2}, c 3 → {d2}] Σ 11 = [start → {d3}, c 1 → {d2}, c 2 → {d2}, c 3 → {d2}] Σ 12 = [start → {d3}, c 1 → {d1}, c 2 → {d2}, c 3 → {d1}] Σ 13 = [start → {d3}, c 1 → {d2}, c 2 → {d2}, c 3 → {d1}]
we can compute the cog trend for each deployment component. Let

Σ(i)| d def = {c | d ∈ Σ(i)(c)}. Then Σ(i)| d d0 d1 d2 d3 Σ(0) start ∅ ∅ ∅ Σ(1) c 1 , start ∅ ∅ ∅ Σ(2) c 1 start ∅ ∅ Σ(3) c 1 c 2 , start ∅ ∅ Σ(4) c 1 c 2 start ∅ Σ(5) c 1 c 2 c 3 , start ∅ Σ(6) c 1 c 2 c 3 start Σ(7) c 1 c 1 , c 2 c 1 , c 2 , c 3 start Σ(8) ∅ c 1 , c 2 , c 3 c 1 , c 2 , c 3 start
Graphically (note that d0 starts at level 1, since at the beginning it contains the "start" cog): simply rely on the label of the transition to recognise the state of the computation, but at each interval the visualiser performs a sort of zoom in, so to magnify the nested behaviour. The result is the sequentialised behaviour depicted below.

To address the second one, we just approximate the behaviour by letting at most n nested recursive invocations. The corresponding graphs are as follows, fixing n = 8, (note that d0 starts at level 1, since at the beginning it contains the "start" cog): In this case, the recursive behaviour corresponds to a pick of deployed cogs in the interval 2 ÷ 3. This pick grows according to the value of n. The interesting property we may grasp from the graphs for d0 is that, the upward pick in the interval 1 ÷ 2 corresponds to a downward pick in the same interval of the same length. This is due to the property that, for each increment in that interval, there is a decrement, thus leaving unchanged the number of cogs in d0 (which is 2). A different behaviour is manifested by the graph of the component d1. In this case, there is a growing increment of deployed cogs according to the increasing of n. The rightmost function lets us derive that the deployment component d1 may become critical as the computation progresses.

Related work

Resource analysis has been extensively studied in the literature and several methods have been proposed, ranging from static analyses (data-flow analysis and type systems) to model checking. We discuss in this section a number of related techniques and the differences with the one proposed in this paper.

A well-known technique is the so-called resource-aware programming [START_REF] Moreau | Resource aware programming[END_REF] that allows users to monitor the resources consumed by their programs and to express policies for the management of such resources in the programs. Resource-aware programming is also available for mainstream languages, such as Java [START_REF] Czajkowski | JRes: A resource accounting interface for Java[END_REF]. Our typing system may integrate resource-aware programming by providing statictime feedbacks about the correctness of the management, such as full-coverage of cases, correctness of the policies, etc.

Other techniques address resource management in embedded systems and mostly use performance analysis on models that are either process algebra [START_REF] Lüttgen | Bisimulation on speed: A unified approach[END_REF], or Petri Nets [START_REF] Sgroi | Synthesis of embedded software using free-choice Petri nets[END_REF], or various types of automata [START_REF] Vulgarakis | Embedded systems resources: Views on modeling and analysis[END_REF]. It is also worth to remind that similar techniques have been defined for web services and business processes [START_REF] Foster | Model checking service compositions under resource constraints[END_REF][START_REF] Netjes | Analysis of resourceconstrained processes with Colored Petri Nets[END_REF]. Usually, all these approaches are invasive because they oblige programmers to declare the cost of transitions in terms of time or in terms of a single resource. On the contrary, our technique does not assign any commitment to programmers, which may be completely unaware of resources and their management.

In [START_REF] Albert | Quantified abstractions of distributed systems[END_REF] a quantified analysis targets ABS programs and returns informations about the different kinds of nodes that compose the system, how many instances of each kind exist, and node interactions. A resource analysis infers upper bounds to the number of concrete instances that the nodes and arcs represent. (The analysis in [START_REF] Albert | Quantified abstractions of distributed systems[END_REF] does not explicitly support deployment components and cog migration; however we believe that this integration is possible.) An important difference of this analysis with respect to our contribution is that our behavioural types are intended to represent a part of SLA that may be validated in a formal way and that support compositional analysis. It is not clear if these correspondence with SLA is also possible for the models of [START_REF] Albert | Quantified abstractions of distributed systems[END_REF].

A type inference technique for resource analysis has been developed in [START_REF] Hoffmann | Multivariate amortized resource analysis[END_REF][START_REF] Hofmann | Automatic type inference for amortised heap-space analysis[END_REF]. They study the problem of worst-case heap usage in functional and (sequential) object-oriented languages and their tool returns functions on the size of inputs of every method that highlight the heap consumption. On the contrary, our technique returns upper bounds disregarding input sizes. However, we think it is possible to extend our types to enable a transition system model that support the expressivity of [START_REF] Hofmann | Automatic type inference for amortised heap-space analysis[END_REF] (our current analysis of behavioural types is preliminary and must be considered as a proof-of-concept). In these regards, we plan to explore the adoption of behavioural types that depends [START_REF] Bove | Dependent types at work[END_REF] on the input data of conditions in if-statements. We observe, anyway, that the generalisation of the results in [START_REF] Hoffmann | Multivariate amortized resource analysis[END_REF][START_REF] Hofmann | Automatic type inference for amortised heap-space analysis[END_REF] to a concurrent setting has not been investigated.

Kobayashi, Suenaga and Wischik develop a technique that is very close to the one in this paper [START_REF] Kobayashi | Resource usage analysis for the pi-calculus[END_REF]. In particular, they extend pi-calculus with primitives for creating and using resources and verify whether a program conforms with resource usage declarations (that may be also automatically inferred). A difference between their technique and the one in this paper is that here the resource analysis is performed ex-post by resorting to abstract transition systems of behavioural types, while in [START_REF] Kobayashi | Resource usage analysis for the pi-calculus[END_REF] the analysis is done during the type checking(/inference). As discussed in [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF], our technique is in principle more powerful than those verifying resource usage during the checking/inference of types.

Conclusions

This work is a preliminary theoretical study about the analysis of resource deployments by means of type systems. Our types are lightweight abstract descriptions of behaviours that retain resource informations and admit type inference.

The analysis of behavioural types that has been discussed in Section 4 is very preliminary. In fact, in Example 2, the resource analysis depends on the input value of the method multi_create. In these cases, a reasonable output of the analysis is a formula that defines the cog-load of deployment components according to the actual value in input. As discussed in Section 5, we intend to investigate more convenient behavioural type analyses, possibly by using more expressive types, such as dependent ones [START_REF] Bove | Dependent types at work[END_REF].

One obvious research direction is to apply our technique for defining an inference system for resource deployment in programming languages, such as ABS or core ABS, and prototyping it with a tool for displaying the load of deployment components. The programme is similar to the one developed for deadlock analysis [START_REF] Giachino | A Framework for Deadlock Detection in ABS[END_REF]. The next step is then the experiment of the prototype on real programs in order to have assessments about its performance and precision.

We also intend to study the range of application of type system techniques when resources are either cloud virtual machines, or CPU, or memory, or bandwidth. The intent is to replace/complement the simulation techniques used in [START_REF] Johnsen | Dynamic resource reallocation between deployment components[END_REF][START_REF] Johnsen | Validating timed models of deployment components with parametric concurrency[END_REF] with static analysis techniques based on types.

  this != @x) moveto @x else moveto d1; return true; } } // available deployment components declaration: data DCData = d0, d1, d2, d3; //main statement: C x1 = new cog C( ); moveto d1; C x2 = new cog C( ); moveto d2; C x3 = new cog C( ); moveto d3; Fut<Bool> f1 = x1!m(x2); Fut<Bool> f2 = x2!m(x3); Bool b1 = f1.get; Fut<Bool> f3 = x3!m(x2); Bool b2 = f2.get; Bool b3 = f3.get;

  Line 12 contains a definition of dcABS: it creates a new object of class C in a new cog, locally deployed, and stores a reference to the new object in the variable x1. The subsequent statement moveto d1 specifies the migration of the class D { Bool move ( ) { moveto d1 ; return true ; } Bool multi_create (Int n) { if (n<=0) return true ; else { D x = new cog D ( ) ; Fut<Bool> f = x!multi_create(n-1) ; Bool u = f.get ; Fut<Bool> g = x!move( ) ; Bool v = g.get ; return true ; } } }

  Fut<Bool> f1 = x1!m(x2);and assume that the environment Γ (and Γ ′ ) in (1) binds method m as followsΓ (C.m) = ([cog : c], [cog : c ′ ]) → --where -[cog : c] and [cog : c ′ ] are the future records of the receiver and of the argument of the method invocation, respectively, ---is the future record of the returned value (it is --because returned values have primitive type Bool).

Fut<Bool>

  f1 = x1!m(x2); // timestamp: n Fut<Bool> f2 = x2!m(x3); // timestamp: n Bool b1 = f1.get; // timestamp: n Fut<Bool> f3 = x3!m(x2); // timestamp: n + 1 Bool b2 = f2.get; // timestamp: n + 1 Bool b3 = f3.get; // timestamp: n + 2

Fig. 1 .

 1 Fig. 1. An example of transition system of behavioural types

Table 2 .

 2 A dcABS recursive program current cog, i.e. cog start, from the current deployment component d0 to the deployment component d1.

⋆ Partly funded by the EU project FP7-610582 ENVISAGE: Engineering Virtualized Services.

We conclude our overview by discussing the issue of recursive invocation. To this aim, consider the type (2) of the method multi_create in Table 2 and the main statement D x = new cog D( ); Fut<Bool> f = x!multi_create(4); Bool b = f.get; whose type is:

Being d0 and d1 the two declared deployment components, we obtain the following computation:

We observe the following two facts: first, every transition, except the initial one, is at logical timestamp 2, because only the outermost interval is observable, while the nested intervals are only relevant to specify the order of events at the same level of nesting; second, in case of recursion the specified behaviour is potentially infinite and parameterised by the number n of transitions, which depends on the number of recursive invocations.

In visualising the results of the analysis, these two aspects pose some questions: the first one may lead us to flatten all the events at timestamp 2 as they happened in parallel, while if observing carefully the computation we notice the events follow a strict sequence; the second one may make it difficult to graphically represent the unbounded behaviour. To address the first point, we don't


Elena Giachino

Naoki Kobayashi

Cosimo Laneve

Deadlock analysis of unbounded process networks

Deadlock detection in concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale. To enable the analysis of such programs, (1) we define an algorithm for detecting deadlocks of a basic model featuring recursion and fresh name generation: the lam programs, and (2) we design a type system for value passing CCS that returns lam programs. As a byproduct of these two techniques, we have an algorithm that is more powerful than previous ones and that can be easily integrated in the current release of TyPiCal, a type-based analyser for pi-calculus.

Introduction

Deadlock-freedom of concurrent programs has been largely investigated in the literature [START_REF] Boyapati | Ownership types for safe program.: preventing data races and deadlocks[END_REF][START_REF] Flanagan | A type and effect system for atomicity[END_REF][START_REF] Abadi | Types for safe locking: Static race detection for Java[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Suenaga | Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references[END_REF][START_REF] Vasconcelos | Type inference for deadlock detection in a multithreaded polymorphic typed assembly language[END_REF]. The proposed algorithms automatically detect deadlocks by building graphs of dependencies (a, b) between resources, meaning that the release of a resource referenced by a depends on the release of the resource referenced by b. The absence of cycles in the graphs entails deadlock freedom. When programs have infinite states, in order to ensure termination, current algorithms use finite approximate models that are excerpted from the dependency graphs. The cases that are particularly critical are those of programs that create networks with an arbitrary number of nodes.

To illustrate the issue, consider the following pi-calculus-like process that computes the factorial:

Fact(n,r,s) = if n=0 then r?m. s!m else new t in (r?m. t!(m*n)) | Fact(n-1,t,s)

Here, r?m waits to receive a value for m on r, and s!m sends the value m on s. The expression new t in P creates a fresh communication channel t and executes P. If the above code is invoked with r!1 | Fact(n,r,s), then there will be a synchronisation between r!1 and the input r?m in the body of Fact(n,r,s). In turn, this may delegate the computation of the factorial to another process in parallel by means of a subsequent synchronisation on a new channel t. That is, in order to compute the factorial of n, Fact builds a network of n + 1 nodes, where node i takes as input a value m and outputs m*i. Due to the inability of statically reasoning about unbounded structures, the current analysers usually return false positives when fed with Fact. For example, this is the case of TyPiCal [START_REF] Kobayashi | TyPiCal: Type-based static analyzer for the Pi-Calculus[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], a tool developed for pi-calculus. (In particular, TyPiCal fails to recognise that there is no circularity in the dependencies among r, s, and t.)

In this paper we develop a technique to enable the deadlock analysis of processes with arbitrary networks of nodes. Instead of reasoning on finite approximations of such processes, we associate them with terms of a basic recursive model, called lam -for deadLock Analysis Model -, which collects dependencies and features recursion and dynamic name creation [START_REF] Giachino | A beginner's guide to the deadLock Analysis Model[END_REF][START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF]. For example, the lam function corresponding to Fact is fact(a 1 , a 2 , a 3 , a 4 ) = (a 2 , a 3 ) + (ν a 5 , a 6 ) (a 2 , a 6 ) fact(a 5 , a 6 , a 3 , a 4 ) where (a 2 , a 3 ) displays the dependency between the actions r?m and s!m and (a 2 , a 5 ) the one between r?m and t!(m*n). The function fact is defined operationally by unfolding the recursive invocations; see Section 3. The unfolding of fact(a 1 , a 2 , a 3 , a 4 ) yields the following sequence of abstract states (bound names in the definition of fact are replaced by fresh ones in the unfoldings). fact(a 1 , a 2 , a 3 , a 4 ) -→ (a 2 , a 3 ) + (a 2 , a 6 ) fact(a 5 , a 6 , a 3 , a 4 )

-→ (a 2 , a 3 ) + (a 2 , a 6 ) (a 6 , a 3 ) + (a 2 , a 6 ) (a 6 , a 8 ) fact(a 7 , a 8 , a 3 , a 4 ) -→ (a 2 , a 3 ) + (a 2 , a 6 ) (a 6 , a 3 ) + (a 2 , a 6 ) (a 6 , a 8 ) (a 8 , a 3 ) +(a 2 , a 6 ) (a 6 , a 8 ) (a 8 , a 10 ) fact(a 9 , a 10 , a 3 , a 4 ) -→ • • • While the model of fact is not finite-state, in Section 4 we demonstrate that it is decidable whether the computations of a lam program will ever produce a circular dependency. In our previous work [START_REF] Giachino | A beginner's guide to the deadLock Analysis Model[END_REF][START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF], the decidability was established only for a restricted subset of lams.

We then define a type system that associates lams to processes. Using the type system, for example, the lam program fact can be extracted from the factorial process Fact. For the sake of simplicity, we address the (asynchronous) value passing CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], a simpler calculus than pi-calculus, because it is already adequate to demonstrate the power of our lam-based approach. The syntax, semantics, and examples of value passing CCS are in Section 5; the type system is defined in Section 6. As a byproduct of the above techniques, our system is powerful enough to detect deadlocks of programs that create networks with arbitrary numbers of processes. It is also worth to notice that our system admits type inference and can be easily extended to pi-calculus. We discuss the differences of our techniques with respect to the other ones in the literature in Section 7 where we also deliver some concluding remark.

Preliminaries

We use an infinite set A of (level) names, ranged over by a, b, c,

• • • . A relation on a set A of names, denoted R, R ′ , • • • , is an element of P(A × A), where P(•) is the standard powerset operator and • × • is the cartesian product. Let -R + be the transitive closure of R. -{R 1 , • • • , R m } ⋐ {R ′ 1 , • • • , R ′ n } if and only if, for all R i , there is R ′ j such that R i ⊆ R ′ j + . -(a 0 , a 1 ), • • • , (a n-1 , a n ) ∈ ∈ {R 1 , • • • , R m } if and only if there is R i such that (a 0 , a 1 ),• • • , (a n-1 , a n ) ∈ R i . -{R 1 , • • • , R m } {R ′ 1 , • • • , R ′ n } def = {R i ∪ R ′ j | 1 ≤ i ≤ m and 1 ≤ j ≤ n}. We use R, R ′ , • • • to range over {R 1 , • • • , R m } and {R ′ 1 , • • • , R ′ n },

The language of lams

In addition to the set of (level) names, we will also use function names, ranged over by f, g, h, • • • . A sequence of names is denoted by a and, with an abuse of notation, we also use a to address the set of names in the sequence.

A lam program is a pair L , L , where L is a finite set of function definitions f( a) = L f , with a and L f being the formal parameters and the body of f, and L is the main lam. The syntax of the function bodies and the main lam is

L ::= 0 | (a, b) | f( a) | L L | L + L | (ν a)L
The lam 0 enforces no dependency, the lam (a, b) enforces the dependency (a, b), while f( a) represents a function invocation. The composite lam L L ′ enforces the dependencies of L and of L ′ , while L + L ′ nondeterministically enforces the dependencies of L or of L ′ , (ν a)L creates a fresh name a and enforces the dependencies of L that may use a. Whenever parentheses are omitted, the operation " " has precedence over "+". We will shorten

L 1 • • • L n into i∈1..n L i and (ν a 1 ) • • • (ν a n )L into (ν a 1 • • • a n )L. Function definitions f( a) = L f and (ν a)
L are binders of a in L f and of a in L, respectively, and the corresponding occurrences of a in L f and of a in L are called bound. A name x in L is free if it is not underneath a (ν a) (similarly for function definitions). Let var(L) be the set of free names in L.

In the syntax of L, the operations " " and "+" are associative, commutative with 0 being the identity on , and definitions and lams are equal up-to alpha renaming of bound names. Namely, if a var(L), the following axioms hold:

(ν a)L = L (ν a)L ′ L = (ν a)(L ′ L) (ν a)L ′ + L = (ν a)(L ′ + L)
Additionally, when V ranges over lams that do not contain function invocations, the following axioms hold:

V V = V V + V = V V (L ′ + L ′′ ) = V L ′ + V L ′′ (1)
These axioms permit to rewrite a lam without function invocations as a collection (operation +) of relations (elements of a relation are gathered by the operation ). Let ≡ be the least congruence containing the above axioms.

Definition 2. A lam V is in normal form, denoted nf(V), if V = (ν a)(V 1 + • • • + V n ), where V 1 , • • • , V n are dependencies only composed with . Proposition 1. For every V, there is nf(V) such that V ≡ nf(V).
In the rest of the paper, we will never distinguish between equal lams. Moreover, we always assume lam programs L , L to be well formed.

Remark 1. The axioms (1) are restricted to terms V that do not contain function invocations. In fact, ,c)) because the evaluation of the two lams (see below) may produce terms with different names.

f( d) ((a, b)+(b, c)) (f( d) (a, b))+(f( d) (b
In the paper, we always assume lam programs L , L to be well-formed. Operational semantics. Let a lam context, noted L[ ], be a term derived by the following syntax:

L[ ] ::= [ ] | L L[ ] | L + L[ ] As usual L[L]
is the lam where the hole of L[ ] is replaced by L. According to the syntax, lam contexts have no ν-binder; that is, the hassle of name captures is avoided. The operational semantics of a program L , L is a transition system where states are lams, the transition relation is the least one satisfying the rule

(Red) f( a) = (ν c)L f ∈ L c ′ are fresh L f [ c ′ / c ][ a ′ / a ] = L ′ f L[f( a ′ )] -→ L[L ′ f ]
and the initial state is the lam L ′ such that L ≡ (ν c)L ′ and L ′ does not contain any ν-binder. We write -→ * for the reflexive and transitive closure of -→.

By (red), a lam L is evaluated by successively replacing function invocations with the corresponding lam instances. Name creation is handled by replacing bound names of function bodies with fresh names. For example, if f(a) = (ν c)((a, c) f(c)) and f(a ′ ) occurs in the main lam, then f(a ′ ) is replaced by (a ′ , c ′ ) f(c ′ ), where c ′ is a fresh name.

Let us discuss some examples.

1. {f(a, b, c) = (a, b) g(b, c) + (b, c), g(d, e) = (d, e) + (e, d)}, f(a, b, c) . Then f(a, b, c) -→ (a, b) g(b, c) + (b, c) -→ (a, b) (b, c) + (c, b) + (b, c) -→ (a, b) (b, c) + (a, b) (c, b) + (b, c)
The lam in the final state does not contain function invocations. This is because the above program is not recursive. Additionally, the evaluation of f(a, b, c) has not created names. This is because the bodies of f and g do not contain ν-binders.

2. {f ′ (a) = (ν b)(a, b) f ′ (b)} , f ′ (a 0 ) . Then f ′ (a 0 ) -→ (a 0 , a 1 ) f ′ (a 1 ) -→ (a 0 , a 1 ) (a 1 , a 2 ) f ′ (a 2 ) -→ n (a 0 , a 1 ) • • • (a n+1 , a n+2 ) f ′ (a n+2 )
In this case, because of the (ν b) binder, the lam grows in the number of dependencies as the evaluation progresses.

{f ′′

(a) = (ν b)(a, b) + (a, b) f ′′ (b)}, f ′′ (a 0 ) . Then f ′′ (a 0 ) -→ (a 0 , a 1 ) + (a 0 , a 1 ) f ′′ (a 1 ) -→ (a 0 , a 1 ) + (a 0 , a 1 ) (a 1 , a 2 ) + (a 0 , a 1 ) (a 1 , a 2 ) f ′′ (a 2 ) -→ n (a 0 , a 1 ) + • • • + (a 0 , a 1 ) • • • (a n+1 , a n+2 ) f ′′ (a n+2 )
In this case, the lam grows in the number of "+"-terms, which in turn become larger and larger as the evaluation progresses.

Flattening and circularities. Lams represent elements of the set P(P(A × A )). This property is displayed by the following flattening function.

Let L be a set of function definitions and let I(•), called flattening, be a function on lams that (i) maps function name f defined in L to elements of P(P(A × A)) and (ii) is defined on lams as follows

I(0) = {∅}, I((a, b)) = {{(a, b)}}, I(L L ′ ) = I(L) I(L ′ ), I(L + L ′ ) = I(L) ∪ I(L ′ ), I((ν a)L) = I(L)[ a ′ / a ] with a ′ fresh, I(f( c)) = I(f)[ c / a
] (where a are the formal parameters of f).

Note that I(L) is unique up to a renaming of names that do not occur free in L. Let I ⊥ be the map such that, for every f defined in L , I ⊥ (f) = {∅}. For example, let L defines f and g and let The property of "having a circularity" is preserved by ≡ while the "absence of circularities" of a composite lam can be carried to its components. Proposition 2. 1. if L ≡ L ′ then L has a circularity if and only if L ′ has a circularity; 2. L L ′ has no circularity implies both L and L ′ have no circularity (similarly for L + L ′ and for (ν a)L).

I(f) = {{(a, b), (b, c)}} I(g) = {{(b, a)}} L ′′ = f(a, b, c) + (a, b) g(b, c) f(d, b, c) + g(d,

The decision algorithm for detecting circularities

In this section we assume a lam program L , L such that pairwise different function definitions in L have disjoint formal parameters. Without loss of generality, we assume that L does not contain any ν-binder.

Fixpoint definition of the interpretation function.

The basic item of our algorithm is the computation of lam functions' interpretation. This computation is performed by means of a standard fixpoint technique that is detailed below. Let A be the set of formal parameters of definitions in L and let κ be a special name that does not occur in L , L . We use the domain P(P(A ∪ {κ} × A ∪ {κ})), ⊆ which is a finite lattice [START_REF] Davey | Introduction to Lattices and Order[END_REF].

Definition 5. Let f i ( a i ) = (ν c i )L i , with i ∈ 1..n, be the function definitions in L . The family of flattening functions I (k) L : {f 1 , • • • , f n } → P(P(A ∪ {κ} × A ∪ {κ})) is defined as follows I (0) L (f i ) = {∅} I (k+1) L (f i ) = {proj a i (R + ) | R ∈ I (k) L (L i )} where proj a (R) def = {(a, b) | (a, b) ∈ R and a, b ∈ a} ∪ {(κ, κ) | (c, c) ∈ R and c a}.
We notice that I (0)

L is the function I ⊥ of the previous section.

Proposition 3. Let f( a) = (ν c)L f ∈ L . (i) For every k, I (k) L (f) ∈ P(P(( a ∪ {κ}) × ( a ∪ {κ}))). (ii) For every k, I (k) L (f) ⋐ I (k+1) L (f).
Proof. 1 is immediate by definition. 2 follows by a straightforward structural induction on L.

⊓ ⊔

Since, for every k, I (k) L (f i ) ranges over a finite lattice, by the fixpoint theory [START_REF] Davey | Introduction to Lattices and Order[END_REF], there exists m such that I (m) L is a fixpoint, namely

I (m) L ≈ I (m+1) L
where ≈ is the equivalence relation induced by ⋐. In the following, we let I L , called the interpretation function (of a lam), be the least fixpoint I (m)

L . Example 1. For example, let L be the factorial function in Section 1. Then

I (0) L (fact) = {∅} I (1) L (fact) = {{(a 2 , a 3 )}, ∅} I (2) L (fact) = {{(a 2 , a 3 )}, ∅} That is, in this case, I L = I (1) L . ⊓ ⊔ Lemma 1. Let f( a) = (ν c)L f ∈ L and b ′ , b ′′ ∈ b and c ′ be disjoint from b, a. Then (b ′ , b ′′ ) ∈ ∈ I (k+1) L (f( b)) if and only if there is R ∈ I (k) L (L f [ c ′ / c ][ b / a ]) such that (b ′ , b ′′ ) ∈ R + . (In particular this statement holds when I (k+1) L = I (k) L = I L .)
Lam programs and circularities. Below we use multiple lam contexts, that is lam contexts with several holes, written

L[ ] • • • [ ],
with the standard meaning. For example, if

L[ ][ ] = [ ] (a, b) + [ ] then L[f(b, c)][(a, c)] = f(b, c) (a, b) + (a, c). Lemma 2. Let {f 1 ( a 1 ) = (ν c 1 )L 1 , • • • , f n ( a n ) = (ν c n )L n }, L be a lam program and let L[f i 1 ( a ′ 1 )] • • • [f i m ( a ′ m )] -→ m L[L i 1 [ c ′ 1/ c i 1 ][ a ′ 1/ a i 1 ]] • • • [L i m [ c ′ m/ c im ][ a ′ m/ a im ]]
where

L[•] • • • [•] is a multiple context without function invocations.
Then, the following two properties are equivalent:

1. I (k+1) L (L[f i 1 ( a ′ 1 )] • • • [f i m ( a ′ m )]) has a circularity, 2. I (k) L (L[L i 1 [ c ′ 1/ c i 1 ][ a ′ 1/ a i 1 ]] • • • [L i m [ c ′ m/ c im ][ a ′ m/ a im ]]) has a circularity. Proof. Let L ′ = L[f i 1 ( a ′ 1 )] • • • [f i m ( a ′ m )] and L ′′ = L[L i 1 [ c ′ 1/ c i 1 ][ a ′ 1/ a i 1 ]] • • • [L i m [ c ′ m/ c im ][ a ′ m/ a im ]].
For the implication 2⇒ 1, there are two subcases:

a) I (k) L (L ′′ ) has a circularity consisting only of names in c ′ i . Namely there are c ′ 0 , c ′ 1 , • • • , c ′ h ∈ c ′ j such that (c ′ 0 , c ′ 1 ), (c ′ 1 , c ′ 2 ), • • • , (c ′ h , c ′ 0 ) ∈ ∈ I (k) L (L ′′ ) . Since names c ′
i are fresh, then, by definition of I L (•), the circularity must occur in

I (k) L (L i j [ c ′ i / c i j ]
), and conversely. In turn, this is possible if and only if

I (k) L (L i j ) has a circularity consisting of names in c i j (because [ c ′ j/ c i j ] is a bijective renaming)
. This means, by definition of

I (k+1) L (•), that (κ, κ) ∈ ∈ I (k+1) L (f i j ) and, in turn, (κ, κ) ∈ ∈ I (k+1) L (L ′ ). b) I (k) L (L ′′ ) has a circularity, let it be (b 0 , b 1 ), • • • (b h , b 0 ), that also contains names not in c ′ 1 , • • • , c ′ m . Without loss of generality, let (b 0 , b 1 ), • • • , (b h ′ -1 , b h ′ ) ∈ ∈ I (k) L (L i j [ c ′ j/ c i j ][ a ′ j/ a i j ]) (2)
while the other pairs of the circularity come from the context

L[ ] • • • [ ].
(b 0 , b h ′ ) ∈ I (k+1) L (f i j ( a ′ j )). This last statement gives (b 0 , b h ′ ), (b h ′ +1 , b h ′ +2 ), • • • (b h , b 0 ) ∈ ∈ I (k+1)
L (L ′ ). For the converse, we consider two cases.

c) Case (κ, κ) ∈ ∈ I (k+1) L (L ′ ). If (κ, κ) comes from the context L, (κ, κ) ∈ ∈ I (k) L (L ′′ ) follows immediately. If (κ, κ) comes from I (k+1)
L (f i j ( a ′ j )), then by the definition of I (k+1) L , I (k) L (L i j ) also has a circularity, hence also

I (k) L (L ′′ ). d) Otherwise, I (k+1)
L (L ′ ) has a circularity on names other than κ. By the definition of I (k+1) L (•), there exists R j ∈ I (k+1) L (f i j ( a ′ j )) for each j ∈ {1, . . . , m} such that

I (k+1) L (L[R 1 ] • • • [R m ])
has a circularity. (Here, we have identified R ⊆ A × A with the lam expression (a 1 ,a 2 )∈R (a 1 , a 2 ).) Because L does not contain function invocations, we have

I (k+1) L (L[R 1 ] • • • [R m ]) = I (k) L (L[R 1 ] • • • [R m ]).
By the definition of

I (k+1) L , there exists R ′ j ∈ I (k) L (L i j [ c ′ j/ c i j ][ a ′ j/ a i j ]) such that R j ⊆ R ′ j + . Therefore, I (k) L (L[R ′ 1 ] • • • [R ′ m ]
) has a circularity, hence also

I (k) L (L ′′ ). ⊓ ⊔ Lemma 3. Let L , L be a lam program and L[f( a ′ )] -→ L[L ′ [ c ′ / c ][ a ′ / a ]].
The following two properties are equivalent:

1. I L (L[f( a)]) has a circularity, 2. I L (L[L ′ [ c ′ / c ][ a ′ / a ]]) has a circularity.
Proof. The proof is similar to the one of Lemma 2: we consider the k such that I (k) L = I and we reason on I (k+1) and I (k) . (Only-if direction) We demonstrate that, if I L (L) has a circularity then there is

L -→ * L ′ such that I ⊥ (L ′ ) has a circularity.
Let m be the least natural number such that

I L = I (m) L . Let L = L[f i 1 ( a ′ 1 )] • • • [f i n ( a ′ n )] such that L[ ] • • • [ ] does not contain function invocations. Then L -→ n L[L i 1 [ c ′ 1/ c i 1 ][ a ′ 1/ a i 1 ]] • • • [L i n [ c ′ n/ c in ][ a ′ n/ a in ]] = L ′′ where c ′ 1 , • • • , c ′ n are fresh. Additionally, by Lemma 2, I (m-1) L (L ′′ ) has a circularity be- cause I (m)
L (L ′ ) has a circularity. Now, we reapply the same argument to L ′′ since I (m-1) L (L ′′ ) has a circularity. After m-steps we get a lam L ′ such that

I (0) L (L ′ ) = I ⊥ (L ′ ) has a circu- larity. ⊓ ⊔
For example, let L be the factorial function in Section 1 and let L = (a 3 , a 2 ) fact(a 1 , a 2 , a 3 .a 4 ). From Example 1, we have I L (fact) = {{(a 2 , a 3 )}, ∅}. Since I L (L) has a circularity, by Theorem 1, there is L -→ * L ′ such that I ⊥ (L ′ ) has a circularity. In fact it displays a circularity after the first transition:

L -→ (a 3 , a 2 ) ((a 2 , a 3 ) + (a 2 , a 5 ) fact(a 5 , a 6 , a 3 , a 4 ) ) .

Value-passing CCS

In the present and next sections, we apply the foregoing theory of lams to refine Kobayashi's type system for deadlock-freedom of concurrent programs [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. In his type system, the deadlock-freedom is guaranteed by a combination of usages, which are a kind of behavioral types capturing channel-wise communication behaviors, and capability/obligation levels, which are natural numbers capturing inter-channel dependencies (like "a message is output on x only if a message is received along y"). By replacing numbers with (lam) level names, we can achieve a more precise analysis of deadlock-freedom because of the algorithm in Section 4. The original type system in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] is for the picalculus [START_REF] Milner | A calculus of mobile processes[END_REF], but for the sake of simplicity, we consider a variant of the value-passing CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], which is sufficient for demonstrating the power of our lam-based approach. The syntax of processes P A and P is shown in Figure 1. A process can be the inert process 0, a message x!e sent on a name x that carries (the value of) an expression e, an input x?y.P that consumes a message x!v and behaves like P[ v / y ], a parallel composition of processes P | Q, a conditional if e then P else Q that evaluates e and behaves either like P or like Q depending on whether the value is 0 (true) or = 0 (false), a restriction (ν a; x : T)P that behaves like P except that communications on x with the external environment are prohibited, an invocation A( a; e) of the process corresponding to A.

= 0 |! a 1 a 2 |? a 1 a 2 .U | (U 1 |U 2 ) | α | µα.U
An expression e can be a name x, an integer value v, or a generic binary operation on integers v op v ′ , where op ranges over a set including the usual operators like +, ≤, etc. Integer expressions without names (constant expressions) may be evaluated to an integer value (the definition of the evaluation of constant expressions is omitted).

Let [[e]] be the evaluation of a constant expression e ([[e]

] is undefined when the integer expression e contains integer names). Let also [[x]] = x when x is a non-integer name.

We defer the explanation of the meaning of types T (and usages U) until Section 6. It is just for the sake of simplicity that processes are annotated with types and level names. They do not affect the operational semantics of processes, and can be automatically inferred by using an inference algorithm similar to those in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF].

Similarly to lams, A( a; x) = P A and (ν a; x : T)P are binders of a; x in P A and of a, x in P, respectively. We use the standard notions of alpha-equivalence, free and bound names of processes and, with an abuse of notation, we let var(P) be the free names in P. In process name definitions A( a; x) = P A , we always assume that var(P A ) ⊆ a, x. Definition 6. The structural equivalence ≡ on processes is the least congruence containing alpha-conversion of bound names, commutativity and associativity of | with identity 0, and closed under the following rule:

((ν a; x : T )P) | Q ≡ (ν a; x : T )(P | Q) a, x var(Q) .
The operational semantics of a program D, P is a transition system where the states are processes, the initial state is P, and the transition relation → D is the least one closed under the following rules:

(R-Com) [[e]] = v x!e | x?y.P → D P[ v / y ] (R-Par) P → D P ′ P | Q → D P ′ | Q (R-New) P → D Q (ν a; x : T )P → D (ν a; x : T )Q (R-IfT) [[e]] 0 if e then P else Q → D P (R-IfF) [[e]] = 0 if e then P else Q → D Q (R-Call) [[ e]] = v A( a; x) = P ∈ D A( a ′ ; e) → D P[ a ′ / a ][ v / x ] (R-Cong) P ≡ P ′ P ′ → D Q ′ Q ′ ≡ Q P → D Q
We often omit the subscript of → D when it is clear from the context. We write → * for the reflexive and transitive closure of →.

The deadlock-freedom of a process P, which is the basic property that we will verify, means that P does not get stuck into a state where there is a message or an input. The formal definition is below.

Definition 7 (deadlock-freedom).

A program D, P is deadlock-free if the following condition holds: whenever P → * P ′ and either (i) P ′ ≡ (ν a 1 ;

x 1 : T 1 ) • • • (ν a k ; x k : T k )(x!v | Q), or (ii) P ′ ≡ (ν a 1 ; x 1 : T 1 ) • • • (ν a k ; x k : T k )(x?y.Q 1 | Q 2 )
, then there exists R such that P ′ → R.

Example 2 (The dining philosophers). Consider the program consisting of the process definitions

Phils(a 1 , a 2 , a 3 , a 4 ; n : int, fork 1 : U 1 , fork 2 : U 2 ) = if n = 1 then Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) else (ν a 5 , a 6 ; fork 3 : U 3 | U 3 | ! a 5 a 6 )( Phils(a 1 , a 2 , a 5 , a 6 ; n -1, fork 1 , fork 3 ) | Phil(a 5 , a 6 , a 3 , a 4 ; fork 3 , fork 2 ) | fork 3 !1 ) Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 : U 1 , fork 2 : U 2 ) = fork 1 ?x 1 .fork 2 ?x 2 .( fork 1 !x 1 | fork 2 !x 2 | Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) )
and of the main process P:

(ν a 1 , a 2 ; fork 1 :

U 1 | U 1 | ! a 1 a 2 )(ν a 3 , a 4 ; fork 2 : U 2 | U 2 | ! a 1 a 2 ) ( Phils(a 1 , a 2 , a 3 , a 4 ; m, fork 1 , fork 2 ) | Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) | fork 1 !1 | fork 2 !1 ) Here, U 1 = µα.? a 2 a 1 .(! a 1 a 2 | α), U 2 = µα.? a 4 a 3 .(! a 3 a 4 | α)
, and U 3 = µα.? a 6 a 5 .(! a 5 a 6 | α), but please ignore the types for the moment. Every philosopher Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) grabs the two forks fork 1 and fork 2 in this order, releases the forks, and repeats the same behavior. The main process creates a ring consisting of m + 1 philosophers, where only one of the philosophers grabs the forks in the opposite order to avoid deadlock. This program is indeed deadlock-free in our definition. On the other hand, if we replace Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) with Phil(a 1 , a 2 , a 3 , a 4 ; fork 2 , fork 1 ) in the main process, then the resulting process is not deadlock-free.

⊓ ⊔

The dining philosophers example is a paradigmatic case of the power of the analysis described in the next section. This example cannot be type-checked in Kobayashi's previous type system [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]: see Remark 2 in Section 6.

The deadlock freedom analysis of value-passing CCS

We now explain the syntax of types in Figure 1. A type is either int or a usage. The former is used to type integer names; the latter is used to type channel names [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Kobayashi | Type systems for concurrent programs[END_REF]. A usage describes how a channel can be used for input and output. The usage 0 describes a channel that cannot be used, ! a 1 a 2 describes a channel that is used for output, ? a 1 a 2 .U describes a channel that is first used for input and then used according to U, and U | U ′ describes a channel that is used according to U and U ′ , possibly in parallel. For example, in process x!2 | x?z.y!z, y has the usage ! a 1 a 2 (please, ignore the subscript and superscript for the moment), and x has the usage ! a 3 a 4 | ? a 5 a 6 .0. The usage µα.U describes a channel that is used recursively according to U[ µα.U / α ]. The operation µα.is a binder and we use the standard notions of alpha-equivalence, free and bound usage names. For example, µα.! a 1 a 2 .α describes a channel that can be sequentially used for output an arbitrary number of times; µα.? a 1 a 2 .! a 3 a 4 .α describes a channel that should be used for input and output alternately. We often omit a trailing 0 and just write ? a 1 a 1 for ? a 1 a 1 .0. The superscripts and subscripts of ? and ! are level names of lams (recall Section 3), and are used to control the causal dependencies between communications [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. The superscript, called an obligation level, describes the degree of the obligation to use the channel for the specified operation. The subscript, called a capability level, describes the degree of the capability to use the channel for the specified operation (and successfully find a partner of the communication).

In order to detect deadlocks we consider the following two conditions:

1. If a process has an obligation of level a, then it can exercise only capabilities of level a ′ less than a before fulfilling the obligation. This corresponds to a dependency (a ′ , a). For example, if x has type ? a 1 a 2 and y has type ! a 3 a 4 , then the process x?u.y!u has lam (a 2 , a 3 ).

2. The whole usage of each channel must be consistent, in the sense that if there is a capability of level a to perform an input (respectively, a message), there must be a corresponding obligation of level a to perform a corresponding message (respectively, input). For example, the usage ! a 1 a 2 | ? a 2 a 1 is consistent, but neither ! a 1 a 2 | ? a 1 a 2 nor ! a 1 a 2 is. To see how the constraints above guide our deadlock analysis, consider the (deadlocked) process: x?u.y!u | y?u.x!u. Because of condition 2 above, the usage of x and y must be of the form ? a 1 a 2 | ! a 2 a 1 and ? a 3 a 4 | ! a 4 a 3 respectively. Due to 1, we derive (a 2 , a 4 ) for x?u.y!u, and (a 4 , a 2 ) for y?u.x!u. Hence the process is deadlocked because the lam (a 2 , a 4 ) (a 4 , a 2 ) has a circularity. On the other hand, for the process x?u.y!u | y?u.0 | x!u, we derive the lam (a 2 , a 4 ), which has no circularity. Indeed, this last process is not deadlocked. While we use lams to detect deadlocks, Kobayashi [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] used natural numbers for obligation/capability levels.

As explained above, usages describe the channel-wise behavior of a process, and they form a tiny process calculus. The usage reduction relation U U ′ defined below means that if a channel of usage U is used for a communication, the channel may be used according to U ′ afterwards. Definition 8. Let = be the least congruence on usages containing alpha-conversion of bound names, commutativity and associativity of | with identity 0, and closed under the following rule:

(UC-Mu) µα.U = U[ µα.U / α ]
The reduction relation U U ′ is the least relation closed under the rules:

(UR-Com) ! a 1 a 2 | ? a 3 a 4 .U U (UR-Par) U 1 U ′ 1 U 1 | U 2 U ′ 1 | U 2 (UR-Cong) U 1 = U ′ 1 U ′ 1 U ′ 2 U ′ 2 = U 2 U 1 U 2
As usual, we let * be the reflexive and transitive closure of .

The following relation rel(U) guarantees the condition 2 on capabilities and obligations above, that each capability must be accompanied by a corresponding obligation. This must hold during the whole computation, hence the definition below. The predicate rel(U) is computable because it may be reduced to Petri Nets reachability (see [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF] for the details about the encoding). Definition 9. U is reliable, written rel(U), when the following conditions hold:

1. whenever U * U ′ and U ′ = ! a 1 a 2 | U 1 ,
= ? a 1 a 2 .U 1 | U 2 , there is U 3 such that U 2 = ! a 2 a 3 | U 3 for some a 3 .
The following type system uses type environments, ranged over Γ, Γ ′ , • • • , that map integer and channel names to types and process names to sequences [ a; T ]. When x dom(Γ), we write Γ, x : T for the environment such that (Γ, x : T )(x) = T and (Γ, x : T )(y) = Γ(y), otherwise. The operation Γ 1 | Γ 2 is defined by: As usual, Γ ⊢ e : T means that e evaluates to a value of type T under an environment that respects the type environment Γ. The judgment Γ ⊢ P : L means that P uses each channel x according to Γ(x), with the causal dependency as described by L. For example, x:? a 1 a 2 , y:! a 3 a 4 ⊢ x?u.y!u : (a 2 , a 3 ) should hold. The typing rules of value-passing CCS are defined in Figure 2, where we use the predicate noact(Γ) and the function ob(U) defined as follows:

(Γ 1 | Γ 2 )(x) =                    Γ 1 (x) if x ∈ dom(Γ 1 ) and x dom(Γ 2 ) Γ 2 (x) if x ∈ dom(Γ 2 ) and x dom(Γ 1 ) [ a; T ] if Γ 1 (x) = Γ 2 (x) = [ a; T ] int if Γ 1 (x) = Γ 2 (x) = int U 1 | U 2 if Γ 1 (x) = U 1 and Γ 2 (x) = U 2 The map Γ 1 | Γ 2 is undefined if, for some x, (Γ 1 | Γ 2 )(x)
Processes:

(T-Zero) noact(Γ) Γ ⊢ 0 : 0 (T-Out) Γ ⊢ e : int Γ, x:! a 1 a 2 ⊢ x!e : 0 (T-In)
Γ, x : U, y : int ⊢ P : L Γ, x:? a 1 a 2 .U ⊢ x?y.P : L ( a∈ob(Γ) (a 2 , a))

(T-Par) Γ ⊢ P : L Γ ′ ⊢ P ′ : L ′ Γ | Γ ′ ⊢ P | P ′ : L L ′ (T-New) Γ, x : U ⊢ P : L rel(U) a ∩ var(Γ) = ∅ Γ ⊢ (ν a; x : U)P : (ν a)L (T-If) Γ ⊢ e : int Γ ′ ⊢ P : L Γ ′ ⊢ P ′ : L ′ Γ | Γ ′ ⊢ if e then P else P ′ : L + L ′ (T-Call) Γ(A) = [ a; T] | a| = | a ′ | Γ ⊢ e : T Γ ⊢ A( a ′ ; e) : f A ( a ′ ) Expressions: (T-Int) noact(Γ) Γ ⊢ n : int (T-Var) noact(Γ) Γ, x : T ⊢ x : T (T-Op) Γ ⊢ e : int Γ ⊢ e ′ : int Γ ⊢ e op e ′ : int (T-Seq) (Γ i ⊢ e i : T i ) i∈1..n Γ 1 | • • • | Γ n ⊢ e 1 ,. . ., e n : T 1 ,. . ., T n Programs: (T-Prog) D = i∈1..n {A i ( a i ; x i : T i ) = P i } Γ = (A i : [ a i ; T i ]) i∈1..n (Γ, x i : T i ⊢ P i : L i ) i∈1..n Γ ′ ⊢ P : L L = i∈1..n {f A i ( a i ) = L i } Γ | Γ ′ ⊢ D, P : L , L
(0) = ∅ ob(! a 1 a 2 ) = {a 1 } ob(? a 1 a 2 .U) = {a 1 } ob(U | U ′ ) = ob(U) ∪ ob(U ′ ) ob(µα.U) = ob(U[ 0 / α ])
The predicate noact(Γ) is used for controlling weakening (as in linear type systems). For example, if we did not require noact(Γ) in rule T-Zero, then we would obtain x:? a 1 a 2 .0 ⊢ 0 : 0. Then, by using T-In and T-Out, we would obtain: x:? a 1 a 2 .0 | ! a 2 a 1 ⊢ 0 | x!1 : 0, and wrongly conclude that the output on x does not get stuck. It is worth to notice that, in the typing rules, we identify usages up to =.

A few key rules are discussed. Rule (T-In) is the unique one that introduces dependency pairs. In particular, the process x?u.P will be typed with a lam that contains pairs (a 2 , a), where a 2 is the capability of x and a is the obligation of every channel in P (because they are all causally dependent from x). Rule (T-Out) just records in the type environment that x is used for output. Rule (T-Par) types a parallel composition of processes by collecting the environments -operation " | " -(like in other linear type systems [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF][START_REF] Kobayashi | Type systems for concurrent programs[END_REF]) and the lams of the components. Rule (T-Call) types a process name invocation in terms of a (lam) function invocation and constrains the sequences of level names in the two invocations to have equal lengths (| a| = | a ′ |) and the types of expressions to match with the types in the process declaration.

Example 3. We illustrate the type system in Figure 2 by typing two simple processes: P = (ν a 1 , a 2 ; x:? y : 0, z : int ⊢ 0 : 0 y:? a 3 a 4 ⊢ y?z.0 : 0

∅ ⊢ 1 : int x:! a 2 a 1 ⊢ x!1 : 0 x:? a 1 a 2 | ! a 2 a 1 , y:? a 3 a 4 | ! a 4 a 3 ⊢ x?z.y!z | y?z.0 | x!1 : (a 2 , a 4 ) ∅ ⊢ Q : (ν a 1 , a 2 )(ν a 3 , a 4 )(a 2 , a 4 )
The lam in the conclusion has no circularity. In fact, Q is not deadlocked.

⊓ ⊔

Example 3 also spots one difference between the type system in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] and the one in Figure 2. Here the inter-channel dependencies check is performed ex-post by resorting to the lam algorithm in Section 4; in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] this check is done during the type checking(/inference) and, for this reason, the process P is not typable in previous Kobayashi's type systems. In this case, the two analysers both recognize that P is deadlocked; Example 4 below discusses a case where the precision is different.

The following theorem states the soundness of our type system.

Theorem 2. Let Γ ⊢ D, P : L , L such that noact(Γ). If L , L has no circularity then D, P is deadlock-free.

The following examples highlight the difference of the expressive power of the system in Figure 2 and the type system in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF].

Example 4. Let D, P be the dining philosopher program in Example 2 and U 1 and U 2 be the usages defined therein. We have Γ ⊢ D, P : L , L where

Γ = Phils : [a 1 , a 2 , a 3 , a 4 ; int, U 1 , U 2 ], Phil : [a 1 , a 2 , a 3 , a 4 ; U 1 , U 2 ] L = { f Phils (a 1 , a 2 , a 3 , a 4 ) = f Phil (a 1 , a 2 , a 3 , a 4 ) +(νa 5 , a 6 )(f Phils (a 1 , a 2 , a 5 , a 6 ) f Phil (a 5 , a 6 , a 3 , a 4 )), f Phil (a 1 , a 2 , a 3 , a 4 ) = (a 1 , a 4 ) (a 3 , a 1 ) (a 3 , a 2 ) f Phil (a 1 , a 2 , a 3 , a 4 ) } L = (νa 1 , a 2 , a 3 , a 4 )(f Phils (a 1 , a 2 , a 3 , a 4 ) f Phil (a 1 , a 2 , a 3 , a 4 ))
For example, let

P 1 = fork 1 ?x 1 .fork 2 ?x 2 .( fork 1 !x 1 | fork 2 !x 2 | Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) ) P 2 = fork 2 ?x 2 .( fork 1 !x 1 | fork 2 !x 2 | Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) ) P 3 = fork 1 !x 1 | fork 2 !x 2 | Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 )
Then the body P 1 of Phil is typed as follows:

Γ 2 , fork 1 :! a 1 a 2 ⊢ fork 1 !x 1 : 0 Γ 2 , fork 2 :! a 3 a 4 ⊢ fork 2 !x 2 : 0 Γ 2 , fork 1 : U 1 , fork 2 : U 2 ⊢ Phil(a 1 , a 2 , a 3 , a 4 ; fork 1 , fork 2 ) : f Phil (a 1 , a 2 , a 3 , a 4 ) Γ 2 , fork 1 :! a 1 a 2 | U 1 , fork 2 :! a 3 a 4 | U 2 ⊢ P 3 : f Phil (a 1 , a 2 , a 3 , a 4 ) Γ 1 , fork 1 :! a 1 a 2 | U 1 , fork 2 : U 2 ⊢ P 2 : (a 3 , a 1 ) (a 3 , a 2 ) f Phil (a 1 , a 2 , a 3 , a 4 ) Γ, fork 1 : U 1 , fork 2 : U 2 ⊢ P 1 : (a 1 , a 4 ) (a 3 , a 1 ) (a 3 , a 2 ) f Phil (a 1 , a 2 , a 3 , a 4 )
where

Γ 1 = Γ, x 1 : int, Γ 2 = Γ, x 2 : int, U 1 = µα.? a 2 a 1 .(! a 1 a 2 | α) and U 2 = µα.? a 4 a 3 .(! a 3 a 4 | α).
Because L , L has no circularity, by Theorem 2, we can conclude that D, P is deadlock-free.

⊓ ⊔ Remark 2. The dining philosopher program cannot be typed in Kobayashi's type system [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. That is because his type system assigns obligation/capability levels to each input/output statically. Thus only a fixed number of levels (represented as natural numbers) can be used to type a process in his type system. Since the above process can create a network consisting of an arbitrary number of dining philosophers, we need an unbounded number of levels to type the process. (Kobayashi [11] introduced a heuristic to partially mitigate the restriction on the number of levels being fixed, but the heuristic does not work here.) A variant of the dining philosopher example has been discussed in [START_REF] Kobayashi | A type system for lock-free processes[END_REF]. Since the variant is designed so that a finite number of levels are sufficient, it is typed both in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] and in our new type system.

Similarly to the dining philosopher program, the system in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] returns a false positive for the process Fact in Section 1, while it is deadlock-free according to our new system. We detail the arguments in the next example.

Example 5. Process Fact of Section 1 is written in the value passing CCS as follows.

Fact(a 1 , a 2 , a 3 , a 4 ; n : int, r:? a 1 a 2 , s:! a 3 a 4 ) = if n = 0 then r?n.s!n else (ν a 5 , a 6 ; t:? a 5 a 6 | ! a 6 a 5 )(r?n.t!(m × n) | Fact(a 5 , a 6 , a 3 , a 4 ; n -1, t, s))

Let Γ = Fact : [a 1 , a 2 , a 3 , a 4 ; int, ? a 1 a 2 , ! a 3 a 4 ] and P be the body of the definition above. Then we have Γ, n : int, r:? a 1 a 2 , s:! a 3 a 4 ⊢ P : L for L = (a 2 , a 3 ) + (ν a 5 , a 6 )((a 2 , a 6 ) f Fact (a 5 , a 6 , a 3 , a 4 )). Thus, we have: Γ ⊢ D, P ′ : L , L ′ for:

P ′ = (ν a 1 , a 2 ; r:? a 1 a 2 | ! a 2 a 1 )(ν a 3 , a 4 ; s:? a 4 a 3 | ! a 3 a 4 )(r!1 | Fact(a 1 , a 2 , a 3 , a 4 ; m, r, s) | s?x.0) L = {f Fact (a 1 , a 2 , a 3 , a 4 ) = L} L ′ = (ν a 1 , a 2 , a 3 , a 4 )(0 f Fact (a 1 , a 2 , a 3 , a 4 ) 0)
where m is an integer constant. Since (L , L ′ ) does not have a circularity, we can conclude that (D, P ′ ) is deadlock-free.

Proof of Theorem 2

Let Γ Γ ′ if, for some x, Γ = Γ ′′ , x : U and Γ ′ = Γ ′′ , x : U ′ with U U ′ . As usual, let * be the transitive closure of .

Theorem 2 follows from the following lemmas.

By the typing rules, Γ ′ , x 1 :

U 1 , • • • x k : U k ⊢ x!e | Q : L is possible provided, for every 1 ≤ i ≤ n: Γ ′ i , z i :? a ′ i a i ⊢ z i ?w i .Q i : L i a∈ob(Γ ′ i ) (a i , a) where Γ ′ i = Γ ′ , x 1 : U i 1 , • • • x k : U i k and Γ ′ , x 1 : U 1 , • • • x k : U k = Γ ′ 1 , z 1 :? a ′ 1 a 1 | • • • | Γ ′ n , z n :? a ′ n a n and L = i∈1..n L i a∈ob(Γ ′ i ) (a i , a) . We notice that L ≡ i∈1..n L i L ′ , with L ′ = i∈1..n, a∈ob(Γ ′ i ) (a i , a)
. Since I ⊥ (L) has no circularity then, by Proposition 2, I ⊥ ( i∈1..n L i ) I ⊥ (L ′ ) has no circularity and, in turn,

I ⊥ (L ′ ) = {R L ′ } and R L ′ , where R L ′ = i∈1..n {(a i , a) | a ∈ ob(Γ ′ i )}
, have no circularity. Let a j , with j ∈ 1..n, be a minimal level of R L ′ , namely:

there is no a ′ such that (a ′ , a j ) ∈ R L ′ .

Because R L ′ has no circularity, a j does exist and, without loss of generality, let z j = x j .

By rule (T-In), U j =?

a ′ j a j .U ′ j | U ′′ j . By rel(U j ) we derive U ′′ j =! a j a ′′ j | U ′′′ j ,
for some a ′′ j and U ′′′ j . By (T-Par) and the fact that a j is minimal in R L ′ , we immediately derive that there exists 1 ≤ i ≤ m such that y i = x j , thus we have P → D R for some R, as required.

⊓ ⊔

Type inference An untyped value-passing CCS program is a program where restrictions are (ν x)P, process invocations are A( e) and process definitions are A( x) = P.

Given an untyped value-passing CCS program D, P , with var(P) = ∅, there is an inference algorithm to decide whether there exists a program D ′ , P ′ that coincides with D, P , except for the type annotations, and such that Γ ⊢ D ′ , P ′ : L , L . The algorithm is almost the same as that of the type system in [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF] and, therefore, we do not re-describe it here. The only extra work compared with the previous algorithm is the lam program extraction, which is done using the rules in Figure 2. Finally, it suffices to analyze the extracted lams by using the fixpoint technique in Section 4.

Synchronous value passing CCS and pi calculus The type system above can be easily extended to the pi-calculus, where channel names can be passed around through other channels. To that end, we extend the syntax of types as follows.

T ::= int | ch(T, U).

The type ch(T, U) describes a channel that is used according to the usage U, and T is the type of values passed along the channel. Only a slight change of the typing rules is sufficient, as summarized below. In particular, (T-Out') introduces dependencies between an output channel and the values sent along the channel. We notice that, in case of synchronous value passing CCS (as well as pi-calculus), where messages have continuations, rule (T-Out') also introduces dependency pairs between the capability of the channel and the obligations in the continuation.

Related Work and Conclusions

In this paper we have designed a new deadlock detection technique for the value-passing CCS (and for the pi-calculus) that enables the analysis of networks with arbitrary numbers of nodes. Our technique relies on a decidability result of a basic model featuring recursion and fresh name generation: the lam programs. This model has been introduced and studied in [START_REF] Giachino | A beginner's guide to the deadLock Analysis Model[END_REF][START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF] for detecting deadlock of an object-oriented programming language [START_REF] Giachino | A framework for deadlock detection in ABS. Software and System Modeling[END_REF], but the decidability was known only for a subset of lams where only linear recursion is allowed [START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF], and only approximate algorithms have been given for the full lam model. The application of the lam model to deadlock-freedom of the value-passing CCS (and pi-calculus) is also new, and the resulting deadlock-freedom analysis significantly improves the previous deadlock-freedom analysis [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], as demonstrated through the dining philosopher example. In particular, Kobayashi's type system provides a mechanism for dealing with a limited form of unbounded dependency chains, but the mechanism is rather ad hoc and fragile with respect to a syntactic change. For example, while is typable, the variation obtained by swapping new s in and new t in is untypable. Neither Fact nor the dining philosopher example are typable in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. More recently, in [START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF], Padovani has introduced another type system for deadlock-freedom, which has a better support than Kobayashi's one for reasoning about unbounded dependency chains, by using a form of polymorphism on levels. However, since the levels in his type system are also integers, neither the Fact example nor the dining philosopher example are typable. In addition, Padovani's type system cannot deal with non-linear channels, like the fork channels in the dining philosopher example. That said, our type system does not subsume Padovani's one, as our system does not support recursive types. Like other type-based analyses, our method cannot reason about value-dependent behaviors. For example, consider the following process:

(if b then x?z.y!z else y!1 | x?z.) | (if b then x!1 | y?z. else y?z.x!z).

It is deadlock-free, but our type system would extract the lam expression: ((a x , a y ) + 0) (0 + (a y , a x )) (where a x and a y are the capability levels of the inputs on x and y respectively), detecting a (false) circular dependency.

The integration of TyPiCal with the deadlock detection technique of this paper is left for future work. We expect that we can extend our analysis to cover lock-freedom [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF], too. To that end, we can require that a lam is not only circularity-free but is also well founded, and/or combine the deadlock-freedom analysis with the termination analysis, following the technique in [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF].

  which are elements of P(P(A × A)). Definition 1. A relation R has a circularity if (a, a) ∈ R + for some a. A set of relations R has a circularity if there is R ∈ R that has a circularity. For instance {(a, b), (b, c)}, {(a, b), (c, b), (d, b), (b, c)}, {(e, d), (d, c)}, {(e, d)} has a circularity because the second element of the set does.

Definition 3 .

 3 A lam program L , L is well formed if (1) function definitions in L have pairwise different function names and all function names occurring in the function bodies and L are defined; (2) the arity of function invocations occurring anywhere in the program matches the arity of the corresponding function definition; (3) every function definition in L has shape f( a) = (ν c)L f , where L f does not contain any ν-binder and var(L f ) ⊆ a ∪ c.

  e) (d, c) + (e, d). Then I(L ′′ ) = {(a, b), (b, c)}, {(a, b), (c, b), (d, b), (b, c)}, {(e, d), (d, c)}, {(e, d)} I ⊥ (L ′′ ) = ∅, {(a, b)}, {(d, c)}, {(e, d)} . Definition 4. A lam L has a circularity if I ⊥ (L) has a circularity. A lam program L , L has a circularity if there is L -→ * L ′ and L ′ has a circularity.

  The general case follows by iterating the following argument. Then, by Lemma 1, (2) is possible if and only if

⊓ ⊔ Theorem 1 .

 1 A lam program L , L has a circularity if and only if I L (L) has a circularity. Proof. (If direction) By definition, L , L has a circularity if there is L -→ * L ′ such that I ⊥ (L ′ ) has a circularity. By induction on the length of L -→ * L ′ . When the length is 0 then I ⊥ (L ′ ) has a circularity implies I L (L) has a circularity (by I ⊥ (L ′ ) = I (0) L (L ′ ) and Proposition 3(2)). Assume L -→ * L ′ be equal to L -→ L ′′ -→ * L ′ . By inductive hypothesis, we assume that the theorem holds on the computation L ′′ -→ * L ′ . Then, by Lemma 3, if I L (L ′′ ) has a circularity then I L (L) has a circularity. Therefore the theorem.

P

  (processes) ::= 0 | x!e | x?y.P | (P | Q) | if e then P else Q | (ν a; x : T)P | A( a; e) e (expressions) ::= x | v | e 1 op e 2 T (types) ::= int | U U (usages) ::

Fig. 1 .

 1 Fig. 1. The Syntax of value-passing CCS

  does not match any of the cases. Let var(Γ) = {a | there is x : Γ(x) = U and a ∈ var(U)}. There are three kinds of type judgments: Γ ⊢ e : T -the expression e has type T in Γ; Γ ⊢ P : L -the process P has lam L in Γ; Γ ⊢ D, P : L , L -the program D, P has lam program L , L in Γ.

Fig. 2 .

 2 Fig. 2. The type system of value-passing CCS (we assume a function name f A for every process name A)

Γ

  ⊢ e : T Γ, x : ch(T, ! a 1 a 2 ) ⊢ x!e : a∈ob(Γ) (a 2 , a) (T-In')Γ, x : ch(T, U), y : T ⊢ P : L Γ, x : ch(T, ? a 1 a 2 .U) ⊢ x?y.P : L ( a∈ob(Γ) (a 2 , a))

Fib

  (n,r) = if n<2 then r?n else new s in new t in (Fib !(n-1,s) | s?x.( Fib !(n-2,t)|t?y.r!(x+y))

  there are U 2 and U 3 such that U 1 = ? a 2 a 3 .U 2 | U 3 for some a 3 ; and 2. whenever U * U ′ and U ′

  a 1 a 2 | ! a 2 a 1 )(ν a 3 , a 4 ; y:? a 3 a 4 | ! a 4 , a 4 ) (a 4 , a 2 ) ∅ ⊢ P : (ν a 1 , a 2 )(ν a 3 , a 4 ) (a 2 , a 4 ) (a 4 , a 2 )and we notice that the lam in the conclusion has a circularity (in fact, P is deadlocked).

	a 3 )(x?z.y!z | y?z.x!z) a 4 | ! a 4 a 1 )(ν a 3 , a 4 ; y:? a 3 a 2 | ! a 2 Q = (ν a 1 , a 2 ; x:? a 1 a 3 )(x?z.y!z | y?z.0 | x!1)
	The proof tree of P is
	y:! a 4 a 3 , z : int ⊢ y!z : 0	x:! a 2 a 1 , z : int ⊢ x!z : 0
	x:? a 1 a 2 , y:! a 4 a 3 ⊢ x?z.y!z : (a 2 , a 4 )	x:! a 2 a 1 , y:? a 3 a 4 ⊢ y?z.x!z : (a 4 , a 2 )
	x:? a 1 a 2 | ! a 2 a 1 , y:? a 3 a 4 | ! a 4 a 3 ⊢ x?z.y!z | y?z.x!z : (a 2 The typing of Q is
	z : int ⊢ z : int
	y:! a 4 a 3 , z : int ⊢ y!z : 0
	x:? a 1 a 2 , y:! a 4 a 3 ⊢ x?z.y!z : (a 2 , a 4 )

Acknowledgments This work was partially supported by JSPS Kakenhi 23220001 and by the EU project FP7-610582 ENVISAGE: Engineering Virtualized Services.

Lemma 4 (type preservation). Let Γ ⊢ D, P : L , L and P → D Q. Then there exist L ′ and Γ ′ such that Γ * Γ ′ and Γ ′ ⊢ D, Q : L , L ′ and I L (L ′ ) ⋐ I L (L).

Proof. This follows by induction on the derivation of P → D Q, with case analysis on the last rule used. The only non-trivial cases are R-Com and R-Call.

-Case R-Com: In this case, we have

By the conditions Γ 1 ⊢ P : L and P = x!e | x?y.P ′ , we have

By the condition Γ 2 ⊢ e : int and [[e]] = v, we have Γ 2 ⊢ v : int. By using the standard substitution lemma, we obtain

Then we have the required result.

-Case R-Call: In this case, we have

By the conditions Γ 1 ⊢ e : T i and [[ e]] = v, we have Γ 1 ⊢ v : T i . Thus, by applying the standard substitution lemma to Γ 0 , x i :

We have the required result for Γ ′ = Γ 1 and

Lemma 5. Let Γ ⊢ D, P : L , L such that I L (L) has no circularity and noact(Γ). If 1. either P ≡ (ν a 1 ;

then there exists R such that P → D R.

Proof. If Q contains conditionals or process calls at the top level, then the required property immediately follows. Thus, we can assume that Q is a parallel composition of inputs and messages. That is

We demonstrate the case 1 of the statement, the other case is similar, hence omitted. Since Γ ⊢ D, P : L , L then there is