In this technical report, we develop a framework for the analysis of resource usage in concurrent systems. We propose an oracle the omniscient garbage collector (OGC) that decides precisely the minimal resource consumption of a process: its resource index. The underlying theory is developed as a nominal automata framework, and applied to the specic problem of tracking resource usage. The framework is put into practice to track resource usage and consumption in pi-calculus processes. Two complementary abstractions are proposed: the rst is based on the labelled transitions, while the second relies on a variant calculus slice-pi that enrich reductions with observations about the resource events. The two abstractions are tested experimentally on classical pi-calculus examples using a prototype analysis tool. In all the examples the resource index can be computed very quickly although in theory it is an NP-complete problem.

R ⊆ R a nite set of resource variables, also denoted by vars(G). V a nite set of vertices, and E ⊆ V × V a nite set of edges, such that there is a unique

. It has 8 resource variables A . . . H and is suciently non-trivial so that it exhibits most of the corner cases of the model.

Most of the properties of resource graphs we will consider can be characterized as properties about nite paths, falling in two categories: complete paths and lasso expansions.

Denition 2.2 (Complete path and lasso). A complete path of a resource graph G with

The vertex v e is called the entry of the lasso and v n its exit. These are respectively denoted by v e = entry( ρ) and v n = exit( ρ). The nite expansion of depth k of the lasso is denoted by ρ k = v 1 , . . . , v e-1 | v e , . . . , v n k , which corresponds to the nite path:

v 1 , . . .

INTRODUCTION

The analysis of resource usage in computational systems is undoubtedly a fundamental research topic, especially in the realm of resource-contrained embedded systems. In this paper, we study basic qualitative and quantitative questions about resource usage for systems involving concurrent activities sharing dynamic resources.

If we abstract from its internal structure, a resource becomes a pure name [START_REF] Gordon | Notes on Nominal Calculi for Security and Mobility[END_REF]], i.e. an object with a globally unique and testable identity. This is the specialty of nominal calculi in general, and the π-calculus [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] in particular. Despite their lack of structure, the pure names display the primordial life-cycle of resources: (1) dynamic allocation, (2) arbitrary usage orderings, and (3) non-trivial garbage collection semantics, the latter point being central in our study.

Our starting point is the resource graph : a resource-focused view of the state-space of a process. From a qualitative perspective, our principal means of abstraction from the low-level details of the graphs (e.g. their branching structure) is the resource prole : a trace-semantics of resource usage. Traces of resource proles are words of formal languages that we name ν-languages dened over innite alphabets of fresh names. To recognize resource proles, we introduce the ν-automata, which are variants of register automata.

Using these devices, we show that the ν-languages corresponding to resource proles are quasi-reguar [START_REF] Kaminski | Finite-Memory Automata[END_REF]. On the positive side, this means that many results about quasi-regular languages can naturally be lifted to resource proles. On the more negative side, a basic question such as the equivalence-testing of resource proles can easily be shown dicult.

To reason about the quantitative notion of resource consumption, we rene the ν-language characterization by considering nite restrictions of their alphabets. The corresponding bounded resource proles provide a natural measure of resource consumption of process behaviors. An interesting indicator is the resource bound which connes the number of resources required for the correct execution of a given system. Ultimately, the least of such bounds namely the resource index represents a profound semantic characteristic of the behavior under study. We provide the Omniscient Garbage Collector (OGC) : a static analysis approach for resource bound and resource index closely related to the maximal independent sets problem and thus graph coloring [START_REF] Jensen | Graph coloring problems[END_REF]. We show, in particular, that computing the resource index is a NP-complete problem, but tight resource bounds can be computed with simple and ecient polynomial algorithms.

Beyond the theory, we aim at the development of practical tools for the analysis of resource usage in concurrent systems. Using a prototype, we propose a couple of experiments of resource consumption in the realm of the π-calculus. To illustrate the versatiliy of the approach, we propose two dierent resource abstractions for π-processes: one based on the labelled transitions for open systems, and another one for closed systems. Pure reductions are opaque and to circumvent this, we introduce slice-π, a rather standard π-calculus extended with an alternative restriction operator allowing the observation of names owing between processes. In all the experiments we observe the same phenomenon which reinforces a strong belief that the apparent intractability of some of the proposed algorithms, especially the computation of the resource index, is largely compensated by the small size of the objects on which they apply. Indeed, most of the examples we explored (especially some classical π-calculus benchmarks) yield very small conict graphs in comparison to the state space of the analyzed processes: in the order of at most a few dozen nodes for systems with more than 100 000 states.

The outline of the paper is as follows. In Section 2 we introduce the basic features and properties of resource graphs. The resource proles are presented in Section 3. The related ν-automata theory is developed in Section 4. In Section 5 we discuss the quantitative aspects most notably the resource bounds and indices as well as the OGC framework for resource analysis. Our experimental study with the π-calculus is described in Section 6. A panorama of related work is given in Section 7.

This paper is based on a previous publication [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF]] that focuses on the algorithmic aspects. Thus, the latter can be seen as a companion for the present paper whose purpose is to dig much deeper into the underlying automata-based theory. Most proofs (except for the shorter ones) are detailed in a dedicated Appendix (cf. page 21).

RESOURCE GRAPHS

As a starting point we propose a simple yet accurate characterization of resource usage in concurrent processes. The resource graphs correspond to the transition systems of processes in which we only observe the events related to resource usage. Denition 2.1 (Resource graph). Let R be a countably innite set of resource variables ranging over X, Y, Z, . . . A resource graph G is a directed graph R, V, E, α, γ, δ with:

Example of a resource graph

We denote by Ψ(G) (resp. Ψ(G)) the nite sets of all complete paths (resp. lassos) of G.

There are only two complete paths in the graph of Fig. 1: v ⊥ , v 1 , v k , . . . , v 6 , v 8 , v 11 , v with v k = v 2 or v k = v 3 . There are six lassos, an example being v ⊥ , v 1 , v 3 | v 4 , . . . , v 6 , v 8 with entry v 4 . Lasso entries are the emphasized vertices, while dashed edges represent the loop closing connections from the exit to the entry of the lasso. In [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF], we describe a polynomial algorithm to compute the complete paths and lassos of a resource graph using a decomposition in nested strongly-connected components.

We impose only minimal constraints on the nature and usage of resource events that are carried by resource graph vertices, although some usage patterns must be enforced. Denition 2.3 (Correct resource usage). A resource graph G has correct resource usage i for each resource X ∈ vars(G) it has at most one vertex v such that X ∈ α(v), and for each nite path ρ = v 1 , . . . , v n of G there is at most one vertex v in ρ such that X ∈ δ(v).

Moreover, ∀j, 1 ≤ j ≤ n s.t. X ∈ γ(v j ), ∃i, 1 ≤ i ≤ j s.t. X ∈ α(v i ) and: if ρ is a complete path then: ∃k, j ≤ k ≤ n s.t. X ∈ δ(v k ).
if ρ is a lasso with entry v e then:

(dynamic) ∃k,

j ≤ k ≤ n s.t. X ∈ δ(v k ) if i ≥ e or ∀l, e ≤ l ≤ n, X / ∈ γ(v l ), (static) ∀k, 1 ≤ k ≤ n, X / ∈ δ(v k ) otherwise.
Most of the constraints are obvious: a given resource is allocated only once globally, and deleted at most once in each path. For a resource used in a given path, a basic principle is that it must be preceded by an allocation and followed by a deletion. However, some subtlety arise because of the cyclic nature of the lassos. Suppose a resource X allocated at some vertex v i and used at v j (j ≥ i) in a lasso with entry v e . There are two cases to consider depending on whether X should survive the cycle or not. In the dynamic case X must be deleted at some vertex v k with k ≥ j. This corresponds to two possible situations: (1) the allocation is performed after the lasso entry (thus, within the cycle), or (2) the resource is not used within the cycle. Considering the lasso v ⊥ , v 1 , v 3 | v 4 , . . . , v 6 , , v 8 in Fig. 1, then situation (1) applies to resources A and B and situation (2) applies to resource H which is allocated before the entry but not used within the cycle. Complementarily, if the allocation of X is performed before the entry of a lasso ρ and it is used within its cycle, then X must survive the cycle and is thus said a static resource for ρ. We denote by static(ρ) the set of variables that are static for the lasso ρ. For example, in the lasso v ⊥ , v 1 | v 3 , . . . , v 11 the resources E (allocated at v 1 and used at v 3 ) and G (allocated at v 3 and used at v 5 ) are static resources.

H

1(1) G 1(1) A 2(2) B 2(2) C 1(2) D 3(1) E 4(3) Fig. 2.
The conict relation for the resource graph of Fig. 1.

This leads to a fundamental classication between inactive (i.e. unused), static, and otherwise dynamic resources.

Denition 2.4 (Resource classication). Let G be a resource graph with vertex set V .



  inactive(G) def = {X | ∀v ∈ V, X / ∈ γ(v)} static(G) def = {X | ∀ρ ∈ Ψ(G), X ∈ static(ρ)} dynamic(G) def = vars(G) \ (static(G) ∪ inactive(G))
In our example the sets are static(G) = {E, G}, inactive(G) = {F } and dynamic(G) = {A, B, C, D, H}. A central concept is the notion of conict in resource uses.

Denition 2.5 (Conict relation). Let X, Y ∈ vars(G) be two distinct resources and ρ a path of G. A conict between X and Y occurs in ρ = v 1 , . . . , v n at position j, 1 ≤ j ≤ n, denoted by X j ρ Y , if any of the following conditions holds:

there exists two vertices v i , v k of ρ (i ≤ j ≤ k) such that X ∈ γ(v i ) ∩ γ(v k ) and Y ∈ γ(v j ).
whenever ρ is a lasso v 1 , . . . , v e-1 | v e , . . . , v n in which X is static, e ≤ j ≤ n and Y ∈ γ(v j ).

If there is a position i in a path ρ such that X i ρ Y or Y i ρ X then X and Y are said in conict, which is denoted X Y .

The conict graph obtained for our illustrative example is depicted on Fig. 2 (for the moment, we ignore the numeric annotations of the nodes). For example we have a conict B D generated by the sub-path v 7 , v 9 , v 10 since D ∈ γ(v 7 ), B ∈ γ(v 9 ) and D ∈ γ(v 10 ).

This corresponds to the rst case of the denition. For the second case, a conict such as A G comes from the fact that A ∈ γ(v 4 ) and G ∈ γ(v 5 ) with v 5 occurring in a lasso after its entry v 4 and before its exit (in this case v 8 ).

Two events play an important role in the life-cycle of a resource: its rst use and its last use. There is also one special case to consider: when a resource must be fetched for a later use, which as we will see allow a form of non-local freshness. These can be characterized on the nite paths of a resource graph. Denition 2.6 (First use, last use and resource fetch). Let G be a resource graph, ρ either a complete path v 1 , . . . , v n or a lasso v 1 , . . . , v e-1 | v e , . . . , v n , and v j one of the vertices of ρ (1 ≤ j ≤ n). For a resource X of G:

X ∈ first ρ (v j ) i X ∈ γ(v j ) and ∀i, 1 ≤ i < j, X / ∈ γ(v i ) and if ρ is a lasso and X ∈ static(ρ) then j < e. X ∈ last ρ (v j ) i X ∈ γ(v j ) \ static(ρ) and ∀k, j < k ≤ n, X / ∈ γ(v k ) X ∈ fetch ρ (v j ) i ρ is a lasso, X ∈ static(ρ), j = e -1 and ∀i, 1 ≤ i < j, X / ∈ γ(v i )
For the example of Fig. 1, we consider the resource E in the complete path ρ = v ⊥ , v 1 , v 2 , . . . , v 6 , v 8 , v 11 , v . Its rst use is at vertex v 2 (i.e. E ∈ first ρ (v 2 )) while its last use is at vertex v 3 (i.e. E ∈ last ρ (v 2 )). Note that these are path-specic notions since in the other complete path (not going through v 2 ) the resource E is both rst-and-last used at vertex v 3 . Now we consider the lasso ρ = v ⊥ , v 1 , v 3 | v 4 , v 5 , v 6 , v 8 and resource G. Since G is static in ρ it has no last use. Moreover, it has no rst use also because what would be its rst use is within the cycle. Hence at vertex v 4 (the entry of the lasso) the variable G must be fetched (i.e. pre-allocated), thus G ∈ fetch ρ (v 4 ).

RESOURCE PROFILES

Resource graphs provide quite a low level view over concurrent process behaviors wrt. resource usage. All the properties we aim to study can be characterized at a more abstract level considering only traces of resource uses. The most fundamental aspect of these trace sets is that they involve dynamically bound resources, whose identity is not known in advance. This naturally leads to languages involving pure names, that is, sets of words with symbols freshly generated that we name ν-languages.

Denition 3.1 (ν-language). Let V be a (potentially) countably innite set of pure names ranging over ν 1 , ν 2 , . . . . A ν-language L over alphabet V is a set of words in (2 V ) * .

The denition makes ν-language quite similar to traditional formal language, although dened over potentially innite alphabets. This way, when a new resource is needed for a given system to perform an action, a fresh identity for the resource is always available.

Reasoning on languages with innite alphabets is in general very dicult [START_REF] Isper | The Innite State Acceptor and Its Application to AI[END_REF]] so we must dene a proper language subset that ts our reasoning requirements.

Our objective is to precisely characterize the ν-language corresponding to the expected behavior of a resource graph. The rst step is to explain how pure names are consumed by the processes. Denition 3.2 (Allocator, Allocation). An allocator Γ is a partial one-to-one function from a nite set of variables to the alphabet of a ν-language. Let ρ be a nite path of a graph G and v one of its vertices an Γ an allocator. An allocation alloc ρ (Γ, α, v) of a ν-symbol α (a set of pure names) is such that α can be decomposed as old(α) ∪ trans(α) ∪ new(α) with:

old(α) = {ν ∈ ran(Γ) | ∃X ∈ γ(v) \ first ρ (v), Γ(X) = ν} trans(α) is a set T ⊆ α \ old(α) such that card(T ) = card(first ρ (v) ∩ last ρ (v)) new(α) is a set N ⊆ α \ (old(α) ∪ trans(α)) such that card(N ) = card(first ρ (v) \ last ρ (v))
The denition above explains how a ν-symbol α is consumed, which corresponds to resource uses at vertex v. The subset old(α) corresponds to the pure names already bound in Γ (old bindings). The pure names in new(α) corresponds to simultaneous allocations and uses at vertex v (new bindings). The remaining consumed names in trans(α) are for a special case: when the names are allocated, used and released in an atomic way. In this case there is no need to record any binding.

The second ingredient is the binding of variables, i.e. the storage of the allocated pure names.

Denition 3.3 (Binding). Let Γ be an allocator, α a set of symbols and v a vertex of a nite path ρ. The binding of α to Γ is an allocator bind ρ (Γ, α, v) = Γ old ∪ Γ new ∪ Γ fetch with:

Γ old = {X → Γ(X) | X / ∈ last ρ (v)} Γ new = {X → ν | ν ∈ new(α) ∧ X ∈ first ρ (v) \ last ρ (v)} Γ fetch = {X → ν | ν / ∈ α ∧ X ∈ fetch ρ (v)}
The denition separates the binding in three disjoint subsets: the old bindings that must be preserved from the previous steps (i.e. for allocated resources that are not release at vertex v and the new bindings that must be recorded for further uses. A special case if for the pure names that are allocated but not used at vertex v, which we call fetching a resource. Based on the previous two denitions we can properly dene the trace sets of resource usage.

Denition 3.4 (Resource prole). The resource prole R G of a resource graph G is a ν-language such that w = α 1 • • • α n ∈ R G if and only if there exists a nite path ρ = v 0 , . . . , v n (either a complete path or a nite expansion of a lasso) such that, for each

position k, 0 < k ≤ n, we have alloc ρ (Γ k-1 , α k , v k ) with: Γ 0 = ∅ ∀j > 0, Γ j = bind ρ (Γ j-1 , α j , v j )
Two properties summarize in essence the ν-languages characterized by the denition above: the binding condition that impersonates the identity of resources, and the conict freedom that is the main requirement of resource proles. Proposition 3.5 (Binding condition). For a position k, 1 ≤ k ≤ n of a nite path ρ = v 1 , . . . , v n (either a complete path or a nite expansion of a lasso) then Γ k (X) = ν if and only if either there exists i,

1 ≤ i ≤ k such that X ∈ first ρ (v i ) ∪ fetch ρ (v i ) and Γ i (X) = ν, provided j, i ≤ j < k such that X ∈ last ρ (v j ). Proposition 3.6 (Conflict freedom). If X k ρ Y then Γ k (X) = Γ k (Y ).
Proof. cf. Appendix A.1 page 21.

AUTOMATA-THEORETIC FRAMEWORK

It is possible to work directly at the level of resource graphs to characterize many properties of the resource proles. This is basically what it is done in [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF].

However, if this is interesting from an algorithmic point of view, we overlook many important theoretical issues. Moreover, the automata-theory developed in this section provides a much more solid ground for the statements of the properties and their proof.

ν-automata

Our rst step is the denition of recognizers for an interesting subset of ν-languages. Denition 4.1 (ν-automaton). A ν-automaton is a pair X , A , where X is a nite disjoint set of variables, and A = Q, q init , ∆, F is a nite state automaton over the alphabet Σ = 2 {νX,X,νX|X∈X } with Q a nite set of states, q init ∈ Q the initial state, ∆ ⊆ Q × Σ × Q the transition relation and F ⊆ Q the set of accepting states.

A ν-automaton is similar to a nite-memory automaton (FMA [START_REF] Kaminski | Finite-Memory Automata[END_REF]) except that the transitions allow to explicitly bind or unbind a symbol. For example it is possible to fetch a fresh symbol without actually consuming it. Also, it is possible to release a name stored in memory. Moreover, the symbols are in fact sets of pure names, which amounts to consider simultaneous resource uses. Hence, ν-automata are resource-oriented variants of traditional FMA's.

As recognizers, the ν-automata correspond to a generalization of the resource proles characterized by Def. 3.4.

Denition 4.2 (ν-language of a ν-automaton).

Let a ν-automaton be A = X , A , with A = Q, q init , ∆, F . For q ∈ Q an actual state of A is a conguration q c = (q, Γ) with Γ an allocator. We denote by Q c the set of all congurations of automaton A. The initial conguration is q c init def = (q init , ∅) and F c = {(q, Γ) | q ∈ F ∧ Γ is an allocator } is the set of accepting congurations. The transition relation ∆ An example of aν-automaton A.

induces the relation ∆ c ⊆ Q c × Σ × Q c such that ((q, Γ), α, (q , Γ )) ∈ ∆ c if and only if there exists a label λ ∈ 2 {νX,X,νX|X∈X } and an allocator Γ such that (q, λ, q ) ∈ ∆ and:

α can be decomposed as α old ∪ α trans ∪ α new with:

α old = {ν ∈ ran(Γ) | X ∈ λ ∧ νX / ∈ λ ∧ Γ(X) = ν} α trans = {ν ∈ V \ α old | X ∈ λ ∧ νX ∈ λ ∧ νX ∈ λ} α new = {ν ∈ V \ (α old ∪ α trans ) | X ∈ λ ∧ νX ∈ λ ∧ νX / ∈ λ} Γ = {X → Γ(X) | νX / ∈ λ} ∪ {X → ν | ν ∈ α new ∧ νX ∈ λ ∧ νX / ∈ λ} ∪ {X → ν | ν / ∈ α ∧ νX ∈ λ ∧ X / ∈ λ ∧ νX / ∈ λ} Let w = α 1 α 2 • • • α n be a ν-word over alphabet 2 V . A run of A on w consists of a sequence of congurations c 0 , c 1 , . . . , c n such that c 0 = q c init and for all i, 1 ≤ i ≤ n, (c i-1 , α i , c i ) ∈ ∆ c .
For a word w, an accepting run of w is a run c 0 , c 1 , . . . , c n such that c n ∈ F c . An automaton A accepts a word w if there exists an accepting run of w. The ν-language of automaton A is the of set of ν-words L(A) = {w | A accepts w}.

Example. Consider a ν-automaton A def = {A, B, C}, {q 0 , q 1 , q 2 , q 3 }, q 0 , ∆, {q 3 } with ∆ = {(q 0 , {νA}, q 1 ), (q 1 , {νB, B}, q 2 ), (q 2 , {B, νB}, q 1 ), (q 2 , {νC, C, νC}, q 2 ), (q 2 , {A, νA, νB}, q 3 ), (q 3 , {}, q 0 )}. Its graphical representation is depicted on Fig. 3, and its behavior is as follows. From the initial state q 0 to q 1 , an arbitrary (but nite) set of pure names is fetched for variable A, but only an empty-set of pure names is consumed along the transition. The states q 1 and q 2 form a kind a sub-automaton comparable to a FMA recognizing the repetition of a symbol. From q 1 to q 2 a symbol is is rst read from the input and bound to variable B. Then an arbitrary number of symbols are read but not stored (this is a transient binding) in the self-loop of q 2 . Then B is release either by reentering the loop starting from q 1 or before acceptance by nal state q 3 . The transition from q 2 to q 3 is interesting since variable the variable A fetched initially is now used. This means that the pure names consumed must be distinct from all the names previously used.

Thus, the ν-automaton implements a form of non-local freshness unavailable in FMA. This is neither a fresh register automaton (FRA [START_REF] Tzevelekos | Fresh-register automata[END_REF]]) which require global freshness while here, the pure names bound to A can be reused if after the transition from q 3 to q 0 .

Resource prole recognizers

The investigation of the ν-automata in isolation although an interesting goal would go beyond the scope of the present paper. We are more interested in using ν-automata as recognizers of resource proles. Denition 4.3. Let G = R, V, E, α, γ, δ be a resource graph. Its induced ν-automaton

A G is dened as follows: A G def = vars(G), Q, q v ⊥ , ∆, {q v } , with: Q = {q v,ρ | ρ ∈ Ψ(G) ∪ Ψ(G), v ∈ ρ \ {v ⊥ , v }} ∪ {q v ⊥ , q v } ∆ = {(q vi,ρ , lbl ρ vi→vj , q vj ,ρ ) | ρ ∈ Ψ(G) ∪ Ψ(G), v i → v j ∈ ρ} ∪ {(q vn, ρ , lbl ρ vn→ve , q ve, ρ ), (q vn, ρ , {}, q v ) | ρ = • • • | v e , . . . , v n ∈ Ψ(G)} with: lbl ρ v→v = {νX | X ∈ first ρ (v ) ∨ (X ∈ fetch ρ (v ) ∧ v = exit(ρ)} ∪ {X | X ∈ γ(v )} ∪ {νX | X ∈ last ρ (v )}
The construction of the ν-automaton from a given resource graph relies on a decomposition of the latter in terms of its complete paths and lassos (cf. Def. 2.2). Note that there is no one-to-one correspondence between the vertices of the resource graph G and the states of the automaton. However, each vertex v of a given pat ρ is in one-to-one correspondence with a state named q v,ρ in A G . It is a simple fact that the ν-automaton corresponding to a resource graph can be of an exponential size, since we enumerate the paths of the graph. In practice, we show in [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF] that it is often possible to work directly at the graph level.

We must now show that the construction is sound, i.e. that the automaton we build from

a resource graph G indeed recognizes its resource prole R G . Lemma 4.4. Let G a resource graph. Then L(A G ) = R G . Proof. cf. Appendix A.2 page 21.
The ν-automaton of Fig. 3 can be easily shown not to correspond to any possible resource graph. It it thus interesting to characterize more precisely the sub-class of ν-automata recognizers of resource proles. One interesting argument is that this sub-class is (strictly) contained in the quasi-regular languages.

Theorem 4.5. Let G be a resource graph. The R G is quasi-regular.

Proof. The proof is both non-trivial and tedious. The rough sketch is as follows. First, we provide an alternative construction of ν-automata from resource graphs, in which all the lassos are expanded exactly once. This allows to remove the rst use vs. fetch subtlety. Then, we show that this new construction still characterizes the resource proles. Moreover the ν-words accepted by these automata can be transformed by a simple homomorphism so that they can be recognized by nite-memory automata (FMA), demonstrating the membership result. The detailed sketch is explained in Appendix A.3 page 22.

It is important to emphasize the obtained FMA are in an order of magnitude larger than the original ν-automata. For example the translation of the resource graph of Fig 1 (with 13 vertices) yield a ν-automaton with 32 states. In comparison, the translated FMA has 408 states, and the growth can be show exponential. Note that the translation to FMA does not work for arbitrary ν-automata.

RESOURCE ANALYSIS

We are now interested in quantifying the amount of resources the system under study requires to behave correctly. To address this question, we introduce an oracle the Omniscient Garbage Collector (OGC) that decides a priori the maximum amount of resources a system can consume. We rely on a simple although far-reaching principle : if the OGC under-estimates the consumption of the system, then a resource conict would occur.

Bounded resource proles

Although ν-language are dened over innite alphabets, the individual ν-words may only consume a nite amount of resources.

Denition 5.1 (Consumption). Let L be a ν-language. The consumption of a ν-word

w = α 1 . . . α n in L is ξ(w) = card ( n i=1 α n ). The consumption of the ν-language itself is ξ(L) = card w=α1...αn∈L n i=1 α n
If a ν-word consumption is inherently nite (they have a nite length), this is not the case of ν-languages that are in most cases innite sets of words. However, it is natural to introduce such a restricted class. Denition 5.2 (Bounded ν-language). A k-bounded ν-language L k is a ν-language dened over a nite alphabet V k of cardinality k.

Proposition 5.3. A k-bounded ν-language has resource consumption at most k.

Proof. This is trivial by Def. 5.1.

The notion of bounded ν-language can be naturally lifted to resource proles. Denition 5.4 (Bounded resource prole). A k-bounded resource prole R k G of a resource graph G is a k-bounded ν-language satisfying Def. 3.4. The measure k is named the resource bound of the graph G.

This restricted denition implies a major requirement for the resource bound k: it must be large enough so that the constraints imposed by Def. 3.4 can be fullled.

An important property of bounded ν-language is that they are insensitive to bijective renamings of pure names. Denition 5.5 (Renaming). Let V and V be two disjoint sets of pure names. A renaming

ζ is a mapping of V → V . The renaming by ζ of : a ν-symbol α ⊆ V is ζ(α) = {ζ(ν) | ν ∈ α}, a ν-word w = α 1 • • • α n ∈ (2 V ) * is ζ(α 1 ) • • • ζ(α n ), a ν-language L over alphabet V is ζ(L) = {ζ(w) | w ∈ L}.
Proposition 5.6. Let G be a resource graph, and

R k G , R k G two k-bounded resource proles dened over respective alphabets V k and V k . Then there is a bijective renaming ζ of V k → V k such that R k G = ζ(R k G ). Proof.
It is a simple fact that in Def. 3.4 only the equality of the pure names in V is exploited, which is the basic principle of the pure names. As such, if R k G is assumed to be a k-bounded resource prole, then renaming its pure names by another set of at least k pure names would not contradict Def. 3.4.

From now on, we will thus consider the k-bounded resource prole R k G , implicitly consid- ering the whole family of resource proles that can be obtained by bijective renamings of their alphabets.

The central question remains: is there in general a bound k such that R k G is dened? In this paper, we only study nite resource graph, which means that we only capture processes that consume only a nite amount of resources at any given point of execution. Moreover, this amount must be bound by the memory of the resource graph, i.e. its resource variables.

Thus a worst-case bound does exists, and it is determined thanks to the following Lemma. Lemma 5.7. Let G be a resource graph such that inactive

(G) = ∅. If k = card(vars(G)) then R k G exists and is recognized by A k G which is automaton A G (of Def. 4.3) restricted to alphabet V k = {v X | X ∈ vars(G)}.
Proof. The principle of the proof is to apply a renaming of the alphabet that associates a single pure name ν X to each resource variable X of vars(G). The complete proof is in Appendix A.4 page 23.

Corollary 5.8. card(vars(G)) is a resource bound for resource graph G.

This provides us with a starting point for our quantitative resource bound analysis. The bound k = card(vars(G)) is the nominal resource bound of G. Before going further in our quantitative study, we provide alternative and arguable simpler proofs for some results presented in the companion paper [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF]].

Theorem 5.9. Let G be a resource graph with resource bound k. Then R k G is regular.

Proof. This is a simple Corollary of Lemma 4.5, for the languages of FMA over nite alphabets are proved regular in [START_REF] Kaminski | Finite-Memory Automata[END_REF].

Corollary 5.10. Bounded resource prole equivalence is PSPACE-hard.

The Omniscient Garbage Collector

Obviously, a process cannot require more resources than the amount of available memory.

However, it may be the case that less memory is enough so that it still behaves correctly.

One thing leading to another, we may ask what is the miminal amount of needed memory.

To adress these questions, we develop in this section a static analysis that can determinate lower bounds of resource consumption direcly from the resource graphs. The objective is to compute a measure k that guarantees the existence of a k-bounded resource prole for a given graph G. The greatest of such bounds is of course the number of resource variables of G, according to Lemma 5.7. To decrease the bound, the only possible way is thus to unify variables of the translated ν-automata.

Denition 5.11 (Unifying variables in ν-automata). Let A = X , A be a ν-automaton

with A = Q, q init , ∆, F . The unication of variables E ⊆ X with Z / ∈ X is: unify E X (A) = (X \ E) ∪ {Z}, unify E X (A) provided:        unify E X (A) = Q, q init , unify E X (∆), F unify E X (∆) = {(q, {unify E X (l) | l ∈ λ}, q ) | (q, λ, q ) ∈ ∆} unify E X (X) = Z if X ∈ E X otherwise unify E X (νX) = νunify E X (X) unify E X (νX) = νunify E X (X) Let Π = {E i | i ∈ [1; n]} be a partition of vars(G), and let Z = {Z 1 . . . Z n } a set of n variables distinct from those vars(G). Then unify Π Z (A) = unify Em 1 Zm 2 (. . . unify Em 1 Zm n (A)) for an arbitrary permutation m 1 , . . . , m n of [1; n].
The unication process is relatively technical but intuitively quite simple: each reference to any of the variables of E in the automaton is replaced by the fresh variable Z. The unication is also lifted to partitions of the set of variables. The unication of each indepedent subset can be performed in an arbitrary order (trivially the outcome is the same since the sets are disjoint).

A fundamental requirement is that the unied variables must correspond to nonconicting resources. Lemma 5.12. Let G be a resource graph and R k G its bounded resource prole such that k = card(vars(G)), and

A k G its recognizer. Moreover let E ⊆ vars(G) such that, ∀X i , X j ∈ E, i = j =⇒ ¬(X i X j ). Then R k-card(E)+1 G is recognized by unify E Z (A k G ) provided Z / ∈ vars(G).
Proof. The proof is similar to that of Lemma 5.7, except that we do not consider a simple renaming of pure name, but a unication of variables. The proof details are in Appendix A.5 page 24.

Similarly to the unication process, the reduction scheme can be lifted to the partition of the resource variables wrt. the conict relation.

Lemma 5.13. Let G be a resource graph and R k G its bounded resource prole such that k = card(vars(G)), and A k G its recognizer. Moreover let

Π = {E 1 , . . . , E n } a partition of vars(G) such that, ∀E = {X 1 , . . . , X m } ∈ Π, ∀i, j, i = j =⇒ ¬(X i X j ). Then R card(Π) G is recognized by unify Π Z (A k G ) provided Z ∩ vars(G) = ∅.
Proof. cf. Appendix A.5 page 24.

Of course, the reduction process must stop at some point, since a minimal amount of memory is required for a process to behave correctly. Hence, a resource graph G has a minimal resource bound which we name its resource index. The basic principle is to minimize the parameter card(Π) of Lemma 5.13.

Lemma 5.14 (Resource index). Let G be a resource graph and Π the set of maximal independent subsets of vars(G) wrt. the conict relation . Then card(Π) is the resource index of G.

Proof. cf. Appendix A.6.

From an algorithmic point of view, the computation of the maximal indepedents sets is based on grap coloring [START_REF] Jensen | Graph coloring problems[END_REF]. In Fig. 2, the numbered labels of the nodes correspond to colorings of the conicts corresponding to the resource graph of Fig. 1. The numbers on the left (before the open parenthesis) correspond to rst-t coloring using the node ordering H, G, A, B, C, D, E. First, H can be colored by (location) 1 and so is G since it is not connected to H. Next, A and B must use color 2 since they are connected to G. The color 1 can be reused for C since it is not yet connected to a colored node. The node D is connected to C (color 1) and B (color 2) and thus must be colored 3. Finally, E is connected to nodes colored up-to 3 and thus has color 4. The independent sets we consider form the partition Π firstfit = {{C, G, H}, {A, B}, {D}, {E}}. The corresponding resource bound is 4.

To obtain the maximal independent sets, we require the perfect coloring of the relation graph. In Fig. 2 this corresponds to the numbers within parentheses. The strategy here is to use the color 2 for both B and C. This way D can reuse color 1 and thus E has color 3 instead of 4. We obtain the partition Π perfect = {{D, G, H}, {A, B, C}, {E}}. The resource index of the resource graph is thus 3 (which is also the chromatic number of the conict graph). Unfortunately, the nding of a perfect coloring is notoriously a dicult problem.

Theorem 5.15. Computing the resource index of a resource graph is NP-complete.

Proof. cf. e.g. [START_REF] Jensen | Graph coloring problems[END_REF] for a detailed proof.

This can be seen as a somewhat negative result, although we remark that the perfect coloring algorithm only applies to the conict graph and not the complete resource graph. In most practical cases the former should be much smaller than the latter. Moreover, interesting properties of separability can often be exploited (cf. [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF]). Last but not least, less tight but still interesting resource bounds can be found in polynomial time. One such example is through the use of rst-t coloring.

P α -→ P bn(α) ∩ fn(Q) = ∅ P | Q α -→ P | Q (par) P ab -→ P Q ab -→ Q P | Q τ -→ P | Q (sync) P ≡ P P α -→ Q Q ≡ Q P α -→ Q (struct) Fig. 5.
The early labelled transition semantics of the π-calculus.

Proof. Let d be the maximum out-degree of a graph. It is a classical result that a k-coloring bounded by d + 1 can be computed in linear time by a rst-t coloring based on an arbitrary ordering of the graph vertices.

APPLICATION: RESOURCE ANALYSIS OF π-CALCULUS PROCESSES

In this section we describe the experimental application of our framework for the analysis of resource consumption in π-calculus processes.

A π-calculus refresher

The syntax of the variant of the π-calculus we cover in the experiment1 is given in Fig. 4.

We also remind the structural congruence between two processes, which is the least relation on processes satisfying:

P ≡ Q by a renaming of bound variables P | Q ≡ Q | P , P | (Q | R) ≡ (P | Q) | R and P | 0 ≡ P D[ a] ≡ P { a/ x} if D( x) def = P for res ∈ {new, local}, res(x) (P | Q) ≡ P | res(x) Q provided x /
∈ free(P )

The semantics of the language is recalled in Fig. 5. Informally, the process 0 has no transition. The scope of a name x can be restricted by either new(x) of local(x) and for now, the two constructs are assumed synonymous (this will be dierent in reduction semantics).

A prexed process α.P denotes a transition with a label corresponding to the action α and continuing as process P . There are four kinds of labels depending on the action α: a label τ is generated by a silent action τ or by a synchronization. a label ab is generated by an input action a(b) for any name b received along channel a and bound to the variable x (in early semantics). a label ab is generated by an output action ab of datum b along channel a, under the provision that a and b are not restricted (i.e. in the scope of a new or a local. a label aνb is a bound output generated by an output action ab where b is restricted, unlike a.

The construct P | Q expresses the parallel composition (in terms of interleaving) of the sub-processes P and Q. These cover the independent evolution of the processes, of alternatively the synchronization for a composition of the form ab.P | a(x).Q. The latter generates a transition with label τ and a continuation of the form: P | Q{a/x}. Finally, the language has tail calls that corresponds to possibly recursive unfoldings of process denitions.

Abstracting transition labels

The rst step of our experiment is to generate a resource graph that reects the behavior of a π-calculus process in terms of resource usage. A natural interpretation consists in interpreting almost directly the labelled transition system (LTS) as a resource graph. Under this interpretation, each transition P µ -→ Q is associated to three vertices v P , v µ and v Q and the edges (v P , v µ ) and (v µ , v Q ). The resource usage is then specied by the values associated to α(v µ ), γ(v µ ) and δ(v µ ). Schematically, we have:

a transition P aνb --→ Q creates a resource X b and is interpreted as: v P α{X b },γ{X b },δ{} v Q a transition P ab -→ Q such that there is a resource X b for b is interpreted as: v P α{},γ{X b },δ{} v Q any other transition P µ -→ Q is interpreted as: v P α{},γ{},δ{} v Q
In this rst abstraction, the rationale is: every data sent to the environment count as resource uses. Hence, any bound output counts as the creation of a fresh resource as well as a use, and each output of a name associated to a resource counts as a simple use. There are possible variations, such as counting the channel itself as a use (e.g. recording a use with ba in case b is associated to a resource X b ), or also taking input into consideration. It is then possible to distinguish between input or output resource uses. In all these possible interpretations, the leitmotiv is that resource prole equivalence should be a necessary (although insucient) condition for bisimilarity 2 . We also require the destruction of resources through δ's. A simple and eective heuristic is to insert a δ{X b } when there is no further free occurrence of the name b in the process.

Let us consider as a rst example the following process:

P def = new(c) ac.bc.P
This is a special case of a common pattern for generating fresh names. Here, the restricted name c is sent rst along a and then b towards the environment. The whole process is then iterated, leading to the following derivations:

2 We do not provide in this report a formal proof that bisimilarity implies resource prole equivalence but this is rather trivial since the traces of resource proles encode all the information stored in the transition labels. The rst output along a corresponds to a bound output since c is restricted but the further output is not bound anymore. Given a resource variable X c representing the name c once required fresh, we obtain the following resource graph:

v ⊥ α{Xc},γ{Xc} v1 γ{Xc},δ{Xc} v2 v
A theoretically acceptable alternative would to have an innite system generating an innite number of resources. Although the version with the least xpoint shows that exactly one resource is required for this behavior, the resource index is invariantly 1 because there can be no conict for this process in any acceptable interpretation.

A minimal conict can be generated by e.g.:

new(a) new(b) ca.cb.ca.0

A slightly complexied variant of this process is as follows:

Q def = new(a) new(b) ca.cb.da.d(x).cx.0 C[X] def = new(d) [Q | X]
The resource graph corresponding to C[d(y).dy.0] is 3 :

v ⊥ α{Xa},γ{Xa} v1 α{X b },γ{X b } v2 v3 v4 γ{Xa},δ{Xa} v5 v
This maintains the conict X a X b and thus the resource index of the system is 2, whereas if we consider the variant C[d(y).dc.0] then the resource graph becomes:

v ⊥ α{Xa},γ{Xa} v1 α{X b },γ{X b },δ{X b } v2 δ{Xa} v3 v4 v5 v
The conict X a X b is no more and hence the resource index is 1 in this case. This illustrates the profoundly semantic nature of the proposed resource abstraction. Indeed, the behavior of X within the context C[X] can be as complex as required so that in the general case (beyond nite control) one cannot decide whether the conict should take place or not. Experimental results for the resource abstraction on labelled transitions.

This abstraction has been implemented in a prototype tool and we analyzed several examples from the HAL environment [START_REF] Ferrari | Verifying Mobile Processes in the HAL Environment[END_REF]]. At present, the tool only support nite control processes and the construction of the resource graph is purely semantic. Since we do not need to preserve the whole branching structure, we can apply a few heuristics to reduce the size of the resource graphs, but in the worst case it can be as large as (although no larger than) the full LTS e.g. as produced by HAL. The problem of producing the smallest possible resource graph is open and we conjecture that its complexity is high.

Fig. 6 gives the gures we obtain for the examples that are particularly interesting for the considered abstraction. For each example, we give the size of the LTS produced by HAL and we compare it with the size of the resource graph we obtain. This measure is not really signicant but it still emphasizes the fact that there is an important potential of abstraction when constructing the resource graphs. A metric much more signicant is the resource index that we obtain using our omniscient garbage collector. A detailed comment of the results is provided in [START_REF] Deharbe | The Omniscient Garbage Collector: a Resource Analysis Framework[END_REF] but the main outcome of the experiment is that the conict graph in all the examples is very small, hence its perfect coloring is always an aordable task. Moreover, the resource index always convey an important information regarding the process behaviors. As an illustration, we can relate the number n of competing cells in heap n+1 (resp. buffer n ) to the resource index n. In the GSM cases, the resource graph (and thus resource index) does not change, which says that despite their important syntactical dierence, they all exhibit exactly the same resource usage.

Rening reductions

Abstracting from the labelled transitions is quite natural but requires a very powerful observer. In comparison, the reduction semantics are much less demanding. However, they only apply on closed systems. An intermediate approach is to model part of the observer within the system. For this we allow a process behavior to be sliced from the point of view of the environment. A process of the form local(x) P considers x as a classical π-calculus restriction but explicitly decorated by a tag inobservable. In comparison, in new(x) P the name x is tagged observable. Names can also be assigned the tag observed although not in their initial state. Now, a standard reduction P → Q of the π-calculus is rened so that it produces a labelled reduction of the form Λ P µ -→ Λ Q in the slice-π variant. The component Λ is a set of names tagged as observable. A name a with the observable tag but lacking the observed tag is such that a ∈ Λ. Otherwise, if it is observable observed then a ∈ Λ. Of course, it cannot be the case that {a, a} ⊆ Λ.

Each reduction P → Q is now reinterpreted as either:

an open reduction of the form: an opaque reduction of the form:

Λ τ.P • -→ Λ P (step) Λ ∪ {x} P µ -→ Λ P x / ∈ Λ Λ new(x) P µ -→ Λ P (obs) Λ µ -→ Λ P x / ∈ Λ Λ local(x) P µ -→ Λ P (inobs) a ∈ Λ ∪ {b} ∨ a ∈ Λ Λ {b} ab.P | a(x).Q b --→ Λ ∪ {b} P | Q{b/x} (sync-fresh) a ∈ Λ ∨ a ∈ Λ b / ∈ Λ Λ ab.P | a(x).R b --→ Λ ∪ {b} P | R{b/x} (sync-open) a ∈ Λ ∨ a ∈ Λ ∪ {b} Λ ∪ {b} ab.P | a(x).Q b - → Λ ∪ {b} P | Q{b/x} (sync-obs) a / ∈ Λ Λ ab.P | a(x).R • -→ Λ P | R{b/x} (sync-inobs) Λ P µ -→ Λ P Λ P | Q µ -→ Λ P | Q (par) P ≡ P Λ P µ -→ Λ Q Q ≡ Q Λ P µ -→ Λ Q (struct)
Λ P • -→ Λ Q in any other case.
The complete operational semantics of the slice-π calculus is provided in Fig. 7. In terms of resource graphs, the interpretation is now quite similar to the labelled abstraction: Reductions of slice-π processes with a observable (top) or inobservable (bottom).

a reduction Λ P b --→ Λ Q creates a resource X b and is interpreted as: v Λ P α{X b },γ{X b },δ{} v Λ Q a reduction Λ P b - → Λ Q such that there is a resource X b for b is interpreted as: v Λ P α{},γ{X b },δ{} v Λ Q any other reduction Λ P • -→ Λ Q is interpreted as: v Λ P α{},γ{},δ{} v Λ Q {} new(a) new(b) S(a, b) x1 ---→ {a, b, x 1 } P (a) | Q (a, b) | Q(a, b) | R(b) x2 ---→ {a, b, x 1 , x 2 } P (a) | Q (a, b) | Q (a, b) | R(b) x1 -→ {a, b, x 1 , x 2 } P (a) | Q(a, b) | Q (a, b) | R(b) x2 -→ {a, b, x 1 , x 2 } S(a, b) . . . {} local(a) new(b) S(a, b) • -→ {b, x 1 } P (a) | Q (a, b) | Q(a, b) | R(b) • -→ {b, x 1 , x 2 } P (a) | Q (a, b) | Q (a, b) | R(b) x1 ---→ {b, x 1 , x 2 } P (a) | Q(a, b) | Q (a, b) | R(b) x2 ---→ {b, x 1 , x 2 } S(a, b) . . .
To illustrate the abstraction, we consider the processes new( a

       P (a) def = new(x) ax.P (a) Q(a, b) def = a(y).Q (a, b, y) Q (a, b, y) def = by.Q(a, b) R(b) def = b(z).R(b) S(a, b) def = P (a) | Q(a, b) | Q(a, b) | R(b)
Fig. 8 shows representative reductions of the rst process with a observable (on the left) and a inobservable (on the right). In the observable case the names a and b are recorded in the rst reduction as observable (i.e. put explicitly in the Λ component of the state). In the same reduction, the name x generated by P is opened (i.e. marked observed) by the synchronization with the leftmost process Q. A second x is opened in the next reduction by the synchronization between P and the rightmost Q. The two x's must be alpha-converted hence the introduction of x 1 and x 2 in the reductions. The Λ component of the transition contains {x 1 , x 2 } because these two observable names are actually observed. If we compare this behavior with the one of the right-hand side, a is there tagged inobservable since it is introduced by the local construct. This means it is not a member of the component Λ of the state, unlike b. Hence the names x 1 and x 2 are now introduced as observable but not yet observed because they are transmitted along a. In terms of resources graphs, the left-hand side reductions yield a conict X x1 X x2 that is absent in the rightmost process. The processes have indeed a dierent resource index: respectively 2 and 1. We thus obtain a level of exibility that is quite comparable to the labelled abstraction, but without the need for an idealistically powerful observer.

Based on this abstraction, we designed a simple example inspired by the classical dining philosophers problem. The idea is that the environment is modeled as a process that acknowledges through an observable channel eat the fact that a philosopher actually starts eating. All the other channels (ending points for the philosophers, the forks, etc.) are created inobservables (hence restricted with local instead of new). Experimental results for the resource abstraction on reductions.

channel along the environment observable eat. As a side eect, the philosophers, initially inobservable, inherit both the observable and observed tags in a dynamic way.

The results for some instances of the philo n examples are listed in Fig. 9. The size of the reduction graph grows exponentially since we modelled various sub-processes running in parallel (e.g. 13 processes for philo 4 ). The resource graphs we obtain using similar heuristics as in the labelled case are much smaller but in a similar order of magnitude in terms of growth. The resource index (and hence the maximum conict) is quite reassuring in that the number of philosophers actually competing for food remains below the number of fork pairs, ensuring the correctness of the protocol. Although simpler analyzes are of course possible for this specic example, the experiment emphasizes the fact that the resource index captures a deep semantic information, tightly related to the chosen resource abstraction.

Last but not least, none of our experiments (except those made on purpose) expose a large resource index. In fact, the perfect coloring of the conict graphs was almost immediate in all the examples, despite the high complexity of the algorithm. In the current version of the tool we use a simple and rather slow CSP-solver for the task. This largely covers our current needs but state-of-the art SAT solvers could be used for more demanding scenarios.

In cases perfect coloring would become unfeasible, we can still compute less tight but still interesting resource bounds very eciently, using e.g. rst-t coloring.

RELATED WORK

Resource control and analysis is a vast topic of research. Considered in their purest form, resources are pure names naturally leading to nominal calculi [START_REF] Gordon | Notes on Nominal Calculi for Security and Mobility[END_REF]] in general, and in particular the π-calculus [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] and its numerous variants. This is a rather abstract and open-ended setting, thus not a very prolic source of eective analysis algorithms. One approach is to enrich the semantics, as e.g. in [START_REF] Amadio | Resource control for synchronous cooperative threads[END_REF] where a resource bound analysis is proposed for a reactive synchronous variant of the π-calculus. For more classical (and abstract) variants, related studies address decidability issues often in connection with Petri nets, such as e.g. [START_REF] Amadio | On Decidability of the Control Reachability Problem in the Asynchronous pi-Calculus[END_REF]; Rosa-Velardo and de Frutos-Escrig 2010] and [START_REF] Hüchting | A Theory of Name Boundedness[END_REF]]. The latter introduces the name-bounded processes, a signicant class of innite-state systems for which the boundedness question is answered positively. It is particularly remarkable that reachability is also decidable for this class. In comparison, we assume the niteness of resource graphs, and deliberately de-emphasize the means by which they are obtained practically.

Indeed, a key feature of our framework is its independence from any particular formalism.

Furthermore, for a given formalism multiple resource abstractions can be experimented as illustrated in Section 6. The abstraction of active restrictions proposed in [START_REF] Hüchting | A Theory of Name Boundedness[END_REF]] only applies on reductions for closed systems. It is also dierent from the resource model we propose around the slice-π calculus, and to illustrate this aspect we consider the following process:

P (a) def = new(x) [ax.0 | a(y).P (y)] | τ.new(z) za.0
In the abstraction we propose, the resource index of new(a) P (a) is 1 because the processes new(z) za are deadlocked after the initial τ . However, since the name a is always free in these deadlocked processes the whole process has an innite number of active restrictions.

This particular example can be of course optimized but the deadlocked process can be complexied at will. Hence, we discuss a ner-grained abstraction that cannot be decided locally. Relying on an essentially semantic abstraction is not without consequences. For instance, our current implementation only works with nite control π-calculus processes. It is a very intriguing and open question whether interesting sub-classes of innite systems with nite resource graphs could be determined, probably starting with variants of the namebounded class itself. Another related abstraction is that of barbed semantics [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]] that also rene reductions but considering in this case the non-restricted channels as observables. This is to ultimately characterize an adequate notion of process equivalence namely strong barbed congruence when the reductions with observables are closed under context. While we could observe the channels instead of (or together with)

the data, we require our renement to remain in one-to-one correspondence with the plain reductions. Also particularly notable in [START_REF] Hüchting | A Theory of Name Boundedness[END_REF] is the prominent role played by the notion of garbage collection something already observed in e.g. the history-dependentautomata [START_REF] Ferrari | Verifying Mobile Processes in the HAL Environment[END_REF]] or in the π-graphs [START_REF] Peschanski | A Petri Net Interpretation of Open Recongurable Systems[END_REF]. This is a side note but to our knowledge, HD-Automata Laboratory (HAL) is the only tool allowing the generation of early labelled transition system from (nitary) π-calculus processes. Indeed, the generation of the early LTS is not trivial especially because it requires the determination of the active names [START_REF] Montanari | Checking Bisimilarity for Finitary pi-Calculus[END_REF], a notion tightly connected to the live variables of resource graphs.

Graph coloring relates to the very well-known problem of register allocation in compiler back-ends [START_REF] Chaitin | Register allocation and spilling via graph coloring (with retrospective)[END_REF]]. However, the behavior of registers is quite specic. For example, one can always choose not to allocate a register, or release it prematurely and defer to the central memory. Hence, the coloring can be both partial and imperfect, allowing many optimization heuristics that do not apply at all in our case. This still naturally connects our study with the well-studied notion of register automata and related formalisms, especially nite memory automata (FMA) [START_REF] Kaminski | Finite-Memory Automata[END_REF] and fresh register automata (FRA) [START_REF] Tzevelekos | Fresh-register automata[END_REF]]. Although the theory of ν-automata shall be further investigated, we suggest in the paper that they represent quite an expressive formalism. For instance, the automaton depicted in Fig 3 can be easily shown not simulable by either a FMA or a FRA. However, we show that resource proles are quasi-regular languages recognizable by FMA. In this specic case, the ν-automata are still relevant since they can trivially be shown exponentially smaller than their FMA counterparts. To our knowledge, the problem of reducing the memory of FMA has only been investigated in the deterministic case [START_REF] Benedikt | Minimal memory automata[END_REF]. Our study suggests an approach for non-deterministic FMA but only to reduce the storage size. Finally, we think that ν-automata represent an interesting formalism to address resource control issues as in e.g. [START_REF] Degano | Nominal Automata for Resource Usage Control[END_REF]] (automata-based approach)

or [START_REF] Kobayashi | Resource Usage Analysis for the pi-Calculus[END_REF]] (typechecking-based approach). This investigation is the next natural step of our study.

A. APPENDIX: PROOF DETAILS A.1. Proof of Propositions 3.5 and 3.6 (binding condition and conict freedom)

Proof. (Proposition 3.5) There are two cases to consider. First, if the binding X → ν

is not created at position k then it is said an old binding. By Def. 3.3 if there is no j, j < k such that X ∈ last ρ (v j ) vertex v (as assumed) then this binding must have been created at a previous position i < k. If the binding is new, then it is a simple fact that i = k.

Proof. (Proposition 3.6) We proceed by induction on k. First, for k = 0 we have no possible conict and Γ 0 = ∅ so that the property vacuously holds. Now suppose that the property is true for any position j, 0 < j ≤ k -1. We proceed by contradiction, showing that it cannot be the case it does not hold anymore at position k. We thus assume X k ρ Y and Γ k (X) = Γ k (Y ). There are three cases to consider. First, if Y ∈ first ρ (v k ) \ last ρ (v k ) then it must consume a symbol ν Y in the subset new(α k ) of Def. 3.2. The same denition imposes that this symbol must not be already present in the range of Γ k-1 . As such, if Γ k-1 (X) = ν X for some name ν X then it must be the case that ν

Y = ν X . Hence, Γ k (X) = Γ k (Y ), contradicting the hypothesis. If otherwise X / ∈ dom(Γ k-1 ) then the conict imposes that X ∈ first ρ (v k ) ∪ fetch ρ (v k ). If X consumes a name ν X at position k then we must have ν X ∈ new(α k ) or ν X ∈ trans(α k ). In both case a simple cardinality argument imposes that ν X = ν Y . The second case is if Y ∈ first ρ (v k ) ∩ last ρ (v k ), hence it is a transient binding.
In this case there is no new binding recorded, so there is nothing left to do. Finally, if the use at position v k is not a rst use, then the binding condition (cf. Prop. 3.5) imposes that there is a position i < k such that Y ∈ first ρ (v i ) ∪ fetch ρ (v i ). By the hypothesis of induction we have that Γ i (X) = Γ i (Y ) hence the contradiction. This nishes the proof.

A.2. Proof of Lemma 4.4 (resource prole recognizers)

The proof requires two auxiliary propositions. The rst one relates the structure of the graph G and the one of the A G . Proposition A.1. Let G be a resource graph. There is a one-to-one correspondence between Ψ(G) ∪ Ψ(G) and the graph of A G . Moreover, for each automata path θ ρ (resp. θ ρ k ) corresponding to a complete path ρ (resp. nite expansion ρ k of a lasso ρ) its starting state is initial and ending state is accepting.

Proof. By Def. 4.3 each vertex v i of a complete path ρ = v 1 , . . . , v n (resp. of a lasso ρ = v 1 , . . . v e-1 | v e , . . . , v n there is a corresponding state q vi,ρ (resp. q vi, ρ ) in the automaton A G . Moreover, for each edge (v i , v i+1 ) of ρ (resp. ρ) there exists a unique label l such that (q vi,ρ , l, q vi+1,ρ ) (resp. (q vi, ρ , l, q vi+1, ρ )) in the transition relation of A G . For a lasso, there is also an exit transition (q vn, ρ , {}, q v ) and there is no other state or transition dened, hence the one-to-one correspondence. Each nite path v 1 , . . . , v n of G corresponding to either a complete path or the k-th expansion of a lasso, by Def. 2.1 we have: v 1 = v ⊥ and v n = v . Hence q v1 = q v ⊥ which is initial and q v2 = q v which is accepting by construction.

The second proposition relates the transition labels of A G to the resource events (use, rst and last use, etc.). Proposition A.2. Let lbl ρ v→v be a transition label of A G . Then:

   X ∈ lbl ρ v→v i X ∈ γ(v ) νX ∈ lbl ρ v→v i first ρ (v ) ∪ fetch ρ (v ) if v = exit(ρ) ∅ otherwise νX ∈ lbl ρ v→v i X ∈ last ρ (v )
Proof. This is direct by Def .4.3.

Proof. (Lemma 4.4) We have to prove the equivalence w = α 1 • • • α n ∈ R G ⇐⇒ w ∈ L G with L G the language of A G . Consider the path ρ = v 1 , . . . , v n used to recognize word w as in Def. 3.4. By Prop. A.1 there is a corresponding path θ ρ = q v ⊥ , q v1,ρ , . . . , q vn,ρ in the graph of A G . Consider now the run σ = (q v ⊥ , Γ 0 ), (q v1,ρ , Γ 1 ), . . . , (q vn,ρ , Γ n ) such that for each position k, 1 ≤ k ≤ n, Γ k is built from Γ k-1 according to Def. 3.3. We must show that σ is an accepting run of w by showing that each symbol α k of the word is consumed by the conguration (q v k ,ρ , Γ k ) and moreover each Γ k can be built as in Def. 4.2. For the consumption part, we can use the decomposition of α k as the disjoint subsets old(α k ), trans(α k ) and new(α k ) of Def. 3.2. According to the construction of Def. 4.3 we know that as dened in Def. 4.2). Thus, α is fully consumed by the conguration (q v k ,ρ , Γ k ). Moreover, also thanks to Prop. A.2 the construction of Γ k from Γ k-1 , as governed by Def. 3.3, is a correct construction according to Def. 4.2. Hence, the conguration (q v k ,ρ , Γ k ) is accepting, as is the whole run σ since we left the position k arbitrary. Exactly the same reasoning steps can be followed in the converse way: from Def. 4.2 to Def. 3.4. This concludes the proof.

(q v k-1 ,ρ , lbl ρ v k-1 →vj , q v k ,ρ ) is
A.3. Proof of Theorem 4.5 (resource proles are quasi-regular)

The objective is to show that the resource prole of a graph G is quasi-regular, i.e. that it can be recognized by a nite memory automaton (FMA) accepting it. The reference paper for FMA is [START_REF] Kaminski | Finite-Memory Automata[END_REF]. For convenience, we adopt a slightly dierent notation, consisting in indexing the windows (i.e. registers) of FMA by variable names instead of integers, which can be trivially put in one-to-one correspondence.

Since we cannot encode the fetching (i.e. allocation without consumption) of a fresh symbol in FMA (this would at least require the power of fresh register automata), we have to nd a way to remove the fetching phase. This is possible for the subclass of ν-automata recognizing the resource proles. The idea is to unfold exactly once each lasso of the resource graph when building the recognizer.

Denition A.3. Let G = R, V, E, α, γ, δ be a resource graph, and Ψ 1 (G) the set of unfolded lassos such that:

Ψ 1 (G) def = { v 1 , . . . , v e-1 , v e1 , . . . , v n1 | v e2 , . . . , v n2 | v 1 , . . . , v e-1 | v e , . . . , v n ∈ Ψ(G)} The ν-automaton induced by G is A fma G def = vars(G), Q, q v ⊥ , ∆, {q v } , with: Q = {q v,ρ | ρ ∈ Ψ(G) ∪ Ψ 1 (G), v ∈ ρ \ {v ⊥ , v }} ∪ {q v ⊥ , q v } ∆ = {(q vi,ρ , lbl vj , q vj ,ρ ) | ρ ∈ Ψ(G) ∪ Ψ 1 (G), v i → v j ∈ ρ} ∪ {(q vn 2 , ρ , lbl ve 2 , q ve 2 , ρ ), (q vn 1 , ρ , {}, q v ), (q vn 2 , ρ , {}, q v ) | ρ = v 1 , . . . , v e1 , . . . , v n1 | v e2 , . . . , v n2 ∈ Ψ 1 (G)} with: lbl v = {νX | X ∈ first ρ (v)} ∪ {X | X ∈ γ(v)} ∪ {νX | X ∈ last ρ (v)}
The rst proof step is to show that the language of the new construction is still the expected resource prole.

Lemma A.4. Let G be a resource graph. Then

L(A G ) = L(A fma G ).
The dierence between A G and A fma G is that in the latter, all the allocations are now performed jointly with a use, hence no fetch event is required anymore.

The construction of a FMA from the ν-automaton A fma G is as follws.

Denition

A.5. Let A fma G = X , Q, q init , ∆, F as in Def. A.3. The induced FMA is M A fma G def = X , S, s init , u, ρ, µ, F , , such that: S = {s i , s j | s i σ -→ s j ∈ µ} u = {X → # | X ∈ X } ∪ {Start → Start, End → End, Flush → #} ρ(s i,k ,θ ) = X if ∃(q i , {r1, . . . , r n }, q j ) ∈ ∆ s.t. θ(r k ) = r k ∧ (r k = νX ∨ r k = ννX) ρ(s i,k ,θ ) = X if ∃(q i , {r1, . . . , r n }, q j ) ∈ ∆ s.t. θ(r k ) = r k ∧ (r k = νX ∨ r k = ννX) Flush otherwise µ = {s i Start ---→ s i,1,θ θ(r1) = == ⇒ • • • θ(rn) = == ⇒ s i,n+1,θ End --→ s j | (q i , λ, q j ) ∈ ∆, θ is a permutation function on dedup(λ) = {r 1 , . . . , r n }} F = {s i | q i ∈ F } with:          dedup(λ) = (λ \ ({X | νX ∈ λ ∨ νX ∈ λ} ∪ {νX, νX | {νX, νX} ⊆ λ})) ∪ {ννX | {νX, νX} ⊆ λ} s i νX = = ⇒ s j = s i X -→ s i Flush ---→ s j s i X = ⇒ s j = s i X -→ s i Flush ---→ s j s i νX = = ⇒ s j = s i X -→ s i X -→ s j s i ννX ==⇒ s j = s i X -→ s i X -→ s j
The encoding of transitions is made in two steps. First, each label set dedup(λ), in which we deduplicate bind and usage (resp. unbind and usage) of a same variable, is splitted into single events, by enumeration of all possible permutations of its elements. Then, each obtained transition is doubled. The goal is to correctly handle unbinds of variables, which must consume a symbol and place a fresh symbol into the corresponding window register.

According to this translation, ν-words have to be also transformed in order to be accepted by the FMA device. The ν-word encoding consists in placing tags to keep the information about where starts and ends a set of symbols. Then each occurence of ν-symbol is followed by the occurence of a fresh symbol taken in a separate namespace V. This new information is mandatory to reset window registers when the corresponding variables must be unbound. This addition must follow each symbol occurence since it is not possible to nd the binding and unbinding instant starting only with a ν-word. Formally, encoding of a ν-word is dened as follows:

w fma = α 1 fma • • • α n fma α i fma = Start. 1≤j≤m (θ(ν i ).ν i,j ).
End with α i = {r 1 , . . . , r m } and θ an arbitrary permutation function on α i The last step of the correspondance proof is to show that the language of a ν-automaton obtained from a resource graph and the language of its induced FMA are the same (upto the encoding of the ν-words).

Lemma A.6. Let A fma G be the ν-automaton induced by a resource graph G, and M A fma G the nite memory automaton induced by

A fma G . Then L(A fma G ) = {w | w fma ∈ L(M A fma G )}.
Since there exists an encoding of resource graph ν-automata in FMA, we can conclude that resource graph ν-automata language are quasi-regular.

A.4. Proof of Lemma 5.7 (nominal resource bound) Proof. (of Lemma 5.7) First, the hypothesis inactive(G) = ∅ is simply because an unused resource can be trivially removed from the resource graph G without any impact on the resource prole. Failing to remove them gratuitously complexies the bound calculations.

Our proof scheme is to rely on Lemma 4.4, which says that :

w ∈ R G i there exists a path ρ = v 1 , . . . , v n in G and an associated run σ = (q v ⊥ , Γ 0 ), (q v1 , Γ 1 ), . . . , (q vn , Γ n ) such that σ accepts w.

Based on the latter assumption, we dene a renaming ζ from V (innite alphabet of A G ) to V k . First, the renaming of the run σ is as follows :

ζ

(σ) = (q v ⊥ , Γ 0 ), (q v1 , ζ(Γ 1 )), . . . , (q vn , ζ(Γ n )) ∀i, 0 ≤ i ≤ n, ζ(Γ i ) = {ν X | X ∈ dom(Γ i )}
Hence, in all the bindings Γ i we just bind variables to their corresponding pure name in V k . To preserve the acceptance relation, we thus have to rename the word w so that the symbols recorded in the Γ i 's now get recorded in the ζ(Γ i )'s.

For this, we use the decomposition of α i of w as the disjoint sets α old A.5. Proof of Lemma 5.12 and Lemma 5.13 (unifying variables)

The following proposition will play an important role in a later result. It says that nonconicting resources may not be used at the same time (otherwise a conict would occur).

Proposition A.7. Let G be a resource graph, ρ = v 1 , . . . , v n a nite path of G and E ⊆ vars(G) a set of resource variables. If ∀X, Y ∈ E, ¬(X i ρ Y ) for a given position i, 1 ≤ i ≤ n then card(γ(v i )) ∩ E ≤ 1.

Proof. We proceed by contradiction. If we suppose card(γ(v i )) ∩ E ≥ 2, then there must be X, Y ∈ E such that X = Y and {X, Y } ⊆ γ(v i ). By Def. 2.5 we would have X i ρ Y (and also Y i ρ X) which contradicts the hypothesis ¬(X i ρ Y ).

Proof. (of Lemma 5.12) Our main hypothesis is: w ∈ R k G i there is a path ρ = v 1 , . . . , v n and a run σ = (q v ⊥ , Γ 0 ), (q v1,ρ , Γ 1 ), . . . , (q vn,ρ , Γ n ) of A k G such that σ accepts w. We also consider that the alphabet of pure names is V k = {ν X | X ∈ vars(G)}. Now, for each position i, 1 ≤ i ≤ n, we let :

unify E Z (Γ i ) = {X → ν X | X ∈ dom(Γ i ) \ E} ∪ {Z → ν Z | X ∈ dom(Γ i ) ∩ E}
and unify E Z (σ) = (q v ⊥ , Γ 0 ), (q v1,ρ , unify E Z (Γ 1 )), . . . , (q vn,ρ , unify E Z (Γ n )).

Hence, in each binding context Γ i the variables of E are all replaced by the unique mapping Z → ν Z and the other variables are left unchanged.

We now apply the renaming corresponding to the unication on the symbols of w. We consider the decomposition of each α i as the disjoint union α old i ∪ α trans i ∪ α new i . And we let :

unify E Z (α old i ) = {ν X ∈ α old i | X ∈ dom(Γ i ) \ E} ∪ {ν Z } if ∃Y ∈ E ∩ (γ(v i ) \ first ρ (v i )) ∅ otherwise
The symbols of α old i that are left unchanged are trivially consumed by conguration (q vi,ρ , unify E Z (Γ i )) since in this case the binding context is left unchanged. If a variable Y of E is used at position i, then it must be bound to a dedicated pure name, which we name ν Z . By Proposition A.7 only one pure name is enough. And since unify E Z (Γ i )(Z) = ν Z (cf. above) the conguration at step i also accepts ν z . If otherwise no variable of E is used at step i then there is nothing left to test.

For the transient and new bindings, the proof scheme is exactly the same, based on the following denitions:

       unify E Z (α trans i ) = {ν X ∈ α trans i | X ∈ (first ρ (v i ) ∩ last ρ (v i )) \ E} ∪ {ν Z } if ∃Y ∈ E, Y ∈ first ρ (v i ) ∩ last ρ (v i ) ∅ otherwise unify E Z (α new i ) = {ν X ∈ α new i | X ∈ (first ρ (v i ) \ last ρ (v i )) \ E} ∪ {ν Z } if ∃Y ∈ E, Y ∈ first ρ (v i ) \ last ρ (v i ) ∅ otherwise
We deduce that unify E Z (α i ) = unify E Z (α old i ) ∪ unify E Z (α trans i ) ∪ unify E Z (α new i ) is accepted by conguration (q vi,ρ , unify E Z (Γ i )). Thus w is accepted by run unify E Z (σ) as expected. This run is trivially a possible run of unify E Z (A k G ), which concludes the proof.

Proof. (of Lemma 5.13) The proof is almost the same as the one for Lemma 5.12 except that we consider a complete partition of vars(G). It is a simple fact that the unication of Π can be done in an arbitrary order since the renamings operate on a distinct domain (a subset E of variables and their unier Z) and distinct range (the name ν Z corresponding to the unier Z). Moreover, by iterating Lemma 5.12 we have that R k-E∈Π card(E)+card(Π) is recognized by unify Π Z (A k G ). And since E∈Π card(E) = card(vars(G)) we obtained the expected bound card(Π).

A.6. Proof of Lemma 5.14 (resource index)

We rst show that unifying conicting variables would contradict the process of recognizing resource proles.

Lemma A.8.

Let w = α 1 • • • α n be a ν-word accepted by a run σ = (q v ⊥ , Γ 0 ), (q v1,ρ , Γ 1 ), . . . , (q vn,ρ , Γ n ) of a ν-automaton A k G (with k variables) of a resource graph G. Then unify {X,Y } Z (w) is accepted by unify {X,Y } Z (σ) i ∀i,

1 ≤ i ≤ n, ¬(X i ρ Y )∧ ¬(Y i ρ X).
Proof. We proceed by contradiction. Suppose there is a position j of ρ such that X j ρ Y (the symmetric case is similar). This means that ∃i, k, 1 ≤ i ≤ j ≤ k ≤ n such that X ∈ γ(v i ) ∩ γ(v k ) and Y ∈ γ(v j ). There must be a pure name ν X such that ∀l, i ≤ l ≤ k, Γ l (X) = ν X (by the binding condition, cf. Prop. 3.5). And at position j the variable Y must be either bound to a name ν Y (old or new binding), or the latter name must be consumed immediately (transient binding). In both cases, ν Y must be distinct from ν X otherwise the conict freedom property (cf. Prop.3.6) would fail. However, unify {X,Y } Z (σ) rename both ν X and ν Y by a single name ν Z , thus trivially the run cannot accept w anymore.

Proof. We start with the resource prole R card(Π) G recognized by the automaton A with variables X = {X 1 , . . . , X card(Π) }. Suppose the resource prole R k G such that k = card(Π)-1 is recognizable.

Then two independent subsets of vars(G) must be unied, which means there are two variables X, Y ∈ X such that X Y (since they are dependent wrt. the partition of ) provided R k G is recognized by unify {X,Y } Z (A) for some Z / ∈ X . But this would contradict Lemma A.8, hence there is no resource bound lower than card(Π).

  Fig. 1.

  Fig. 3.

  Fig. 4.The syntax of the π-calculus (with slices).

Fig. 7 .

 7 Fig. 7.The semantics of the slice-π calculus.

Fig

  Fig. 8.

  ) new(b) S(a, b) vs. local(a) new(b) S(a, b) with:

  a transition of A G . Hence, by Prop. A.2 we can deduce the following equalities: old(α k ) = α old k , trans(α k ) = α trans k and new(α k ) = α new k (the latter sets

i

  (consumption from old bindings), α old i (transient bindings) and α new i(new bindings) as in Def. 4.2. Let ζ(α old i ) = {ν X | Γ i (X) = ν ∧ ν ∈ α old i }.Thus for an old binding of variable X, we have ζ(Γ i )(X) = ν X and thus the renamed binding is still accepted at position i of the renamed run. Next, ζ(α trans i ) = {ν X | X ∈ first ρ (v i ) ∩ last ρ (v i )}, hence there are enough fresh names so that the transient bindings are also consumed in the renamed run. Finally,ζ(α new i ) = {ν X | Γ i+1 (X) = ν ∧ ν ∈ α new i } if i < n and ζ(α new n ) = α new n = ∅ (since there is no new binding in the nal step of the run). Since ζ(Γ i+1 )(X) = ν X the latter subset gets also consumed as required. Thus, ζ(α i ) is naturally consumed by conguration (q vi,ρ , ζ(Γ i )).Hence, ζ(σ) accepts ζ(w) = ζ(α 1 ) • • • ζ(α n ) thus ζ(w) ∈ ζ(R G ) i ζ(σ)accepts w, which concludes the proof.

3

  A single-hole process context C[X] is a function from process expression extended by a single occurrence of a variable X to process expressions, such that C[P ] = C[X]{P/X} for a standard notion of substitution of variables by processes. Here for example C[d(y).dy.0] = new(d) Q | d(y).dy.0 .

	Model	LTS	Resource graph	Resource index
	heap 4	700	86	3
	heap 5	8476	303	4
	heap 6	126125	1094	5
	buffer 4	596	339	4
	buffer 5	7173	3621	5
	buffer 6	106878	49246	6
	GSM	489	56	3
	GSM buff	164	56	3
	GSM full	2183	56	3
	Fig. 6.

  The resource conicts occur when distinct philosophers eat at the same time on the table, by transmitting the philosopher

	Model	# Processes	Reductions	Resource graph	Resource index
	philos 2	7	133	20	1
	philos 3	10	2992	136	1
	philos 4	13	98245	4148	2
	Fig. 9.

For the sake of concision, we omit the constructs of non-deterministic choice and match/mismatch. Note that our prototype tool has support for both