Elena Giachino
email: tgiachino@cs.unibo.it

Cosimo Laneve
email: laneveu@cs.unibo.it

Deadlock detection in linear recursive programs ‹

Deadlock detection in recursive programs that admit dynamic resource creation is extremely complex and solutions either give imprecise answers or do not scale. We define an algorithm for detecting deadlocks of linear recursive programs of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations of names to so-called mutations, which transform tuples by introducing duplicates and fresh names. Our algorithm realizes the back-end of deadlock analyzers for objectoriented programming languages, once the association programs/basicmodel-programs has been defined as front-end.

Introduction

Modern systems are designed to support a high degree of parallelism by ensuring that as many system components as possible are operating concurrently. Deadlock represents an insidious and recurring threat when such systems also exhibit a high degree of resource and data sharing. In these systems, deadlocks arise as a consequence of exclusive resource access and circular wait for accessing resources. A standard example is when two processes are exclusively holding a different resource and are requesting access to the resource held by the other. In other words, the correct termination of each of the two process activities depends on the termination of the other. Since there is a circular dependency, termination is not possible.

The techniques for detecting deadlocks build graphs of dependencies px, yq between resources, meaning that the release of a resource referenced by x depends on the release of the resource referenced by y. The absence of cycles in the graphs entails deadlock freedom. The difficulties arise in the presence of infinite (mutual) recursion: consider, for instance, systems that create an unbounded number of processes such as server applications. In such systems, process interaction becomes complex and either hard to predict or hard to be detected during testing and, even when possible, it can be difficult to reproduce deadlocks and find their causes. In these cases, the existing deadlock detection tools, in order to ensure termination, typically lean on finite models that are extracted from the dependency graphs.

The most powerful deadlock analyzer we are aware of is TyPiCal, a tool developed for pi-calculus by Kobayashi [START_REF] Kobayashi | [END_REF][START_REF] Kobayashi | A partially deadlock-free typed process calculus[END_REF][START_REF] Igarashi | A generic type system for the pi-calculus[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. This tool uses a clever technique for deriving inter-channel dependency information and is able to deal with several recursive behaviors and the creation of new channels without using any pre-defined order of channel names. Nevertheless, since TyPiCal is based on an inference system, there are recursive behaviors that escape its accuracy. For instance, it returns false positives when recursion is mixed up with delegation. To illustrate the issue we consider the following deadlock-free pi-calculus factorial program * factorial ?( n ,( r , s )).

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

In this code, factorial returns the value (on the channel s) by delegating this task to the recursive invocation, if any. In particular, the initial invocation of factorial, which is r!1 | factorial!(n,(r,s)), performs a synchronization between r!1 and the input r?m in the continuation of factorial?(n,(r,s)).

In turn, this may delegate the computation of the factorial to a subsequent synchronization on a new channel t. TyPiCal signals a deadlock on the two inputs r?m because it fails in connecting the output t!(m*n) with them.

The technique we develop in this paper allows us to demonstrate the deadlock freedom of programs like the one above.

To ease program reasoning, our technique relies on an abstraction process that extracts the dependency constraints in programs by dropping primitive data types and values; -by highlighting dependencies between pi-calculus actions; -by overapproximating statement behaviors, namely collecting the dependencies and the invocations in the two branches of the conditional (the set union operation is modeled by ).

This abstraction process is currently performed by a formal inference system that does not target pi-calculus, but it is defined for a Java-like programming language, called ABS [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF], see Section 6. Here, pi-calculus has been considered for expository purposes. The ABS program corresponding to the pi-calculus factorial may be downloaded from [START_REF] Giachino | Deadlock Framework for ABS (DF4ABS) -online interface[END_REF]; readers that are familiar with Java may find the code in the Appendix A. As a consequence of the abstraction operation we get the function factorialpr, sq " pr, sq pr, tq factorialpt, sq where pr, sq shows the dependency between the actions r?m and s!m and pr, tq the one between r?m and t!(m*n). The semantics of the abstract factorial is defined operationally by unfolding the recursive invocations. In particular, the unfolding of factorialpr, sq yields the sequence of abstract states (free names in the definition of factorial are replaced by fresh names in the unfoldings)

factorialpr, sq ÝÑ pr, sq pr, tq factorialpt, sq ÝÑ pr, sq pr, tq pt, sq pt, uq factorialpu, sq ÝÑ pr, sq pr, tq pt, sq pt, uq pu, sq pu, vq factorialpv, sq ÝÑ ¨¨Ẅ e demonstrate that the abstract factorial (and, therefore, the foregoing pi-calculus code) never manifests a circularity by using a model checking technique. This despite the fact that the model of factorial has infinite states. In particular, we are able to decide the deadlock freedom by analyzing finitely many states -precisely three -of factorial.

Our solution. We introduce a basic recursive model, called lam programs -lam is an acronym for deadLock Analysis Model -that are collections of function definitions and a main term to evaluate. For example, `factorialpr, sq " pr, sq pr, tq factorialpt, sq , factorialpr, sq defines factorial and the main term factorialpr, sq. Because lam programs feature recursion and dynamic name creation -e.g. the free name t in the definition of factorial -the model is not finite state (see Section 3).

In this work we address the Question 1. Is it decidable whether the computations of a lam program will ever produce a circularity?

and the main contribution is the positive answer when programs are linear recursive.

To begin the description of our solution, we notice that, if lam programs are non-recursive then detecting circularities is as simple as unfolding the invocations in the main term. In general, as in case of factorial, the unfolding may not terminate. Nevertheless, the following two conditions may ease our answer:

(i) the functions in the program are linear recursive, that is (mutual) recursions have at most one recursive invocation -such as factorial; (ii) function invocations do not show duplicate arguments and function definitions do not have free names.

When (i) and (ii) hold, as in the program `fpx, y, zq " px, yq fpy, z, xq, fpu, v, wq ˘, recursive functions may be considered as permutations of names -technically we define a notion of associated (per)mutation -and the corresponding theory [START_REF] Comtet | Advanced Combinatorics: The Art of Finite and Infinite Expansions[END_REF] guarantees that, by repeatedly applying a same permutation to a tuple of names, at some point, one obtains the initial tuple. This point, which is known as the order of the permutation, allows one to define the following algorithm for Question 1:

1. compute the order of the permutation associated to the function in the lam and 2. correspondingly unfold the term to evaluate.

For example, the permutation of f has order 3. Therefore, it is possible to stop the evaluation of f after the third unfolding (at the state pu, vq pv, wq pw, uq fpu, v, wq) because every dependency pair produced afterwards will belong to the relation pu, vq pv, wq pw, uq.

When the constraint (ii) is dropped, as in factorial, the answer to Question 1 is not simple anymore. However, the above analogy with permutations has been a source of inspiration for us. order g(x 0 ,x 1 ,x 2 ,x 3 ,x 4 ,x 5 ,x 6 )=(x 3 ,x 1 )(x 0 ,x 8 )(x 8 ,x 7 )g(x 2 ,x 0 ,x 1 ,x 5 ,x 6 ,x 7 ,x 8 ), g(x 0 ,x 1 ,x 2 ,x 3 ,x g(x 0 ,x 1 ,x 2 ,x 3 ,x 4 ,x 5 ,x 6 ) (x 3 ,x 1 )(x 0 ,x 8 )(x 8 ,x 7 ) g(x 2 ,x 0 ,x 1 ,x 5 ,x 6 ,x 7 ,x 8 ) (x 5 ,x 0 )(x 2 ,x 10 )(x 10 ,x 9 ) g(x 1 ,x 2 ,x 0 ,x 7 ,x 8 ,x 9 ,x 10 ) (x 7 ,x 2 )(x 1 ,x 12 )(x 12 ,x 11 ) g(x 0 ,x 1 ,x 2 ,x 9 ,x 10 ,x 11 ,x 12 ) (x 9 ,x 1 )(x 0 ,x 14 )(x 14 ,x 13 ) g(x 2 ,x 0 ,x 1 ,x 11 ,x 12 ,x 13 ,x 14 )

(x 11 ,x 0 )(x 2 ,x 16 )(x 16 ,x 15 ) g(x 1 ,x 2 ,x 0 ,x 13 ,x 14 ,x 15 ,x 16 ) , g(x 0 ,x 1 ,x 2 ,x 3 ,x 4 ,x 5 ,x 6 )
Fig. 1. A lam program and its unfolding

Consider the main term factorialpr, sq. Its evaluation will never display factorialpr, sq twice, as well as any other invocation in the states, because the first argument of the recursive invocation is free. Nevertheless, we notice that, from the second state -namely pr, sq pr, tq factorialpt, sq -onwards, the invocations of factorial are not identical, but may be identified by a map that -associates names created in the last evaluation step to past names, -is the identity on other names.

The definition of this map, called flashback, requires that the transformation associated to a lam function, called mutation, also records the name creation. In fact, the theory of mutations allows us to map factorialpt, sq back to factorialpr, sq by recording that t has been created after r, e.g. răt.

We generalize the result about permutation orders (Section 2):

by repeatedly applying a same mutation to a tuple of names, at some point we obtain a tuple that is identical, up-to a flashback, to a tuple in the past.

As for permutations, this point is the order of the mutation, which (we prove) it is possible to compute in similar ways.

However, unfolding a function as many times as the order of the associated mutation may not be sufficient for displaying circularities. This is unsurprising because the arguments about mutations and flashbacks focus on function invocations and do not account for dependencies. In the case of lams where (i) and (ii) hold, these arguments were sufficient because permutations reproduce the same dependencies of past invocations. In the case of mutations, this is not true anymore as displayed by the function g in Figure 1. This function has order 3 and the first three unfoldings of gpx 0 , x 1 , x 2 , x 3 , x 4 , x 5 , x 6 q are those above the horizontal line. While there is a flashback from gpx 0 , x 1 , x 2 , x 9 , x 10 , x 11 , x 12 q to gpx 0 , x 1 , x 2 , x 3 , x 4 , x 5 , x 6 q, the pairs produced up-to the third unfolding px 3 , x 1 q px 0 , x 8 q px 8 , x 7 q px 5 , x 0 q px 2 , x 10 q px 10 , x 9 q px 7 , x 2 q px 1 , x 12 q px 12 , x 11 q do not manifest any circularity. Yet, two additional unfoldings (displayed below the horizontal line of Figure 1), show the circularity px 0 , x 8 q px 8 , x 7 q px 7 , x 2 q px 2 , x 10 q px 10 , x 9 q px 9 , x 1 q px 1 , x 12 q px 12 , x 11 q px 11 , x 0 q . In Section 4 we prove that a sufficient condition for deciding whether a lam program as in Figure 1 will ever produce a circularity is to unfold the function g up-to two times the order of the associated mutation -this state will be called saturated. If no circularity is manifested in the saturated state then the lam is "circularity-free". This supplement of evaluation is due to the existence of two alternative ways for creating circularities. A first way is when the circularity is given by the dependencies produced by the unfoldings from the order to the saturated state. Then, our theory guarantees that the circularity is also present in the unfolding of g till the order -see Figure 2.a. A second way is when the dependencies of the circularity are produced by [START_REF] Abadi | Types for safe locking: Static race detection for Java[END_REF] the unfolding till the order and by (2) the unfolding from the order till the saturated state -these are the so-called crossover circularities -see Figure 2.b. Our theory allows us to map dependencies of the evaluation (2) to those of the evaluation (1) and the flashback may break the circularity -in this case, the evaluation till the saturated state is necessary to collect enough informations. Other ways for creating circularities are excluded. The intuition behind this fact is that the behavior of the function (the dependencies) repeats itself following the same pattern every order-wise unfolding. Thus it is not possible to reproduce a circularity that crosses more than one order without having already a shorter one. The algorithm for detecting circularities in linear recursive lam programs is detailed in Section 5, together with a discussion about its computational cost.

We have prototyped our algorithm [START_REF] Giachino | Deadlock Framework for ABS (DF4ABS) -online interface[END_REF]. In particular, the prototype (1) uses a (standard but not straightforward) inference system that we developed for deriving behavioral types with dependency informations out of ABS programs [START_REF] Giachino | Deadlock analysis of concurrent objects: Theory and practice[END_REF] and ( 2) has an add-on translationg these behavioral types into lams. We have been able to verify an industrial case study developed by SDL Fredhopppermore than 2600 lines of code -in 31 seconds. Details about our prototype and a comparison with other deadlock analysis tools can be found in Section 6. There is no space in this contribution to discuss the inference system: the interested readers are referred to [START_REF] Giachino | Deadlock analysis of concurrent objects: Theory and practice[END_REF].

Generalizing permutations: mutations and flashbacks

Natural numbers are ranged over by a, b, i, j, m, n, . . . , possibly indexed. Let V be an infinite set of names, ranged over by x, y, z, ¨¨¨. We will use partial order relations on names -relations that are reflexive, antisymmetric, and transitive -, ranged over by V, V 1 , I, ¨¨¨. Let x P V if, for some y, either px, yq P V or py, xq P V. Let also var pVq " tx | x P Vu. For notational convenience, we write r

x when we refer to a list of names x 1 , . . . , x n .

Let V ' r xăr z, with r x P V and r z R V, be the least partial order containing the set V Y tpy, zq | x P r

x and px, yq P V and z P r zu. That is, r z become maximal names in V ' r xăr z. For example, -tpx, xqu ' xăz " tpx, xq, px, zq, pz, zqu; -if V " tpx, yq, px 1 , y 1 qu (the reflexive pairs are omitted) then V ' yăz is the reflexive and transitive closure of tpx, yq, px 1 , y 1 q, py, zqu; -if V " tpx, yq, px, y 1 qu (the reflexive pairs are omitted) then V ' xăz is the reflexive and transitive closure of tpx, yq, px, y 1 q, py, zq, py 1 , zqu.

Let x ď y P V be px, yq P V.

Definition 1. A mutation of a tuple of names, denoted ( a 1 , ¨¨¨, a n ) where 1 ď a 1 , ¨¨¨, a n ď 2 ˆn, transforms a pair @ V, px 1 , ¨¨¨, x n q D into @ V 1 , px 1 1 , ¨¨¨, x 1 n q D as follows. Let tb 1 , ¨¨¨, b k u " ta 1 , ¨¨¨, a n uzt1, 2, ¨¨¨, nu and let z b1 , ¨¨¨, z b k be k pairwise different fresh names. [That is names not occurring either in x 1 , ¨¨¨, x n or in V.] Then -if 1 ď a i ď n then x 1 i " x ai ; -if a i ą n then x 1 i " z ai ; -V 1 " V ' x 1 , ¨¨¨, x n ăz i1 , ¨¨¨, z i k . The mutation ( a 1 , ¨¨¨, a n ) of @ V, px 1 , ¨¨¨, x n q D is written @ V, px 1 , ¨¨¨, x n q D ( a1,¨¨¨,an ) ÝÑ @ V 1 , px 1 1 , ¨¨¨, x 1 n q D
and the label ( a 1 , ¨¨¨, a n ) is omitted when the mutation is clear from the context. Given a mutation µ " ( a 1 , ¨¨¨, a n ), we define the application of µ to an index i, 1 ď i ď n, as µpiq " a i .

Permutations are mutations ( a 1 , ¨¨¨, a n ) where the elements are pairwise different and belong to the set t1, 2, ¨¨¨, nu (e.g. ( 2, 3, 5, 4, 1 )). In this case the partial order V never changes and therefore it is useless. Actually, our terminology and statements below are inspired by the corresponding ones for permutations. A mutation differs from a permutation because it can exhibit repeated elements, or even new elements (identified by n `1 ď a i ď 2 ˆn, for some a i ). For example, by successively applying the mutation ( 2, 3, 6, 1, 1 ) to @ V, px 1 , x 2 , x 3 , x 4 , x 5 q D , with V " tpx 1 , x 1 q, ¨¨¨, px 5 , x 5 qu and r

x "

x 1 , x 2 , x 3 , x 4 , x 5 , we obtain @ V, px 1 , x 2 , x 3 , x 4 , x 5 q D ÝÑ @ V 1 , px 2 , x 3 , y 1 , x 1 , x 1 q D ÝÑ @ V 2 , px 3 , y 1 , y 2 , x 2 , x 2 q D ÝÑ @ V 3 , py 1 , y 2 , y 3 , x 3 , x 3 q D ÝÑ @ V 4 , py 2 , y 3 , y 4 , y 1 , y 1 q D ÝÑ ¨¨ẅ here V 1 " V ' r xăy 1 and, for i ě 1, V i`1 " V i ' y i ăy i`1 .
In this example, 6 identifies a new name to be added at each application of the mutation. The new name created at each step is a maximal one for the partial order.

We observe that, by definition, ( 2, 3, 6, 1, 1 ) and ( 2, 3, 7, 1, 1 ) define a same transformation of names. That is, the choice of the natural between 6 and 10 is irrelevant in the definition of the mutation. Similarly for the mutations ( 2, 3, 6, 1, 6 ) and ( 2, 3, 7, 1, 7 ). Definition 2. Let ( a 1 , ¨¨¨, a n ) « ( a 1 1 , ¨¨¨, a 1 n ) if there exists a bijective function f from rn `1..2 ˆns to rn `1..2 ˆns such that:

1. 1 ď a i ď n implies a 1 i " a i ; 2. n `1 ď a i ď 2 ˆn implies a 1 i " f pa i q.
We notice that ( 2, 3, 6, 1, 1 ) « ( 2, 3, 7, 1, 1 ) and ( 2, 3, 6, 1, 6 ) « ( 2, 3, 7, 1, 7 ). However ( 2, 3, 6, 1, 6 ) ff ( 2, 3, 6, 1, 7 ); in fact these two mutations define different transformations of names.

Definition 3. Given a partial order V, a V-flashback is an injective renaming ρ on names such that ρpxq ď x P V.

In the above sequence of mutations of px 1 , x 2 , x 3 , x 4 , x 5 q there is a V 4 -flashback from py 2 , y 3 , y 4 , y 1 , y 1 q to px 2 , x 3 , y 1 , x 1 , x 1 q. In the following, flashbacks will be also applied to tuples: ρpx 1 , ¨¨¨, x n q def " pρpx 1 q, ¨¨¨, ρpx n qq.

In case of mutations that are permutations, a flashback is the identity renaming and the following statement is folklore. Let µ be a mutation. We write µ m for the application of µ m times, namely @ V, px 1 , ¨¨¨,

x n q D µ m ÝÑ @ V 1 , py 1 , ¨¨¨, y n q D abbreviates @ V, px 1 , ¨¨¨, x n q D µ ÝÑ ¨¨¨µ ÝÑ @ V 1 , py 1 , ¨¨¨, y n q D looooooooooooooooooooooooooooooomooooooooooooooooooooooooooooooon m times . Proposition 1. Let µ " ( a 1 , ¨¨¨, a n ) and @ V, px 1 , ¨¨¨, x n q D µ ÝÑ @ V 1 , px 1 1 , ¨¨¨, x 1 n q D µ m ÝÑ @ V 2 , py 1 , ¨¨¨, y n q D µ ÝÑ @ V 3 , py 1 1 , ¨¨¨, y 1 n q D
If there is a V 2 -flashback ρ such that ρpy 1 , ¨¨¨, y n q " px 1 , ¨¨¨, x n q then there is a V 3 -flashback from py 1 1 , ¨¨¨, y 1 n q to px 1 1 , ¨¨¨, x 1 n q.

Proof. Let ρ 1 be the relation y 1 i Þ Ñ x 1 i , for every i. Then 1) ρ 1 is a mapping: y 1 i " y 1 j implies x 1 i " x 1 j . In fact, y 1 i " y 1 j means that either (i) 1 ď a i , a j ď n or (ii) a i , a j ą n. In subcase (i) y ai " y aj , by definition of mutation. Therefore ρpy ai q " ρpy aj q that in turn implies x ai " x aj . From this last equality we obtain x 1 i " x 1 j . In subcase (ii), a i " a j and the implication follows by the fact that ( a 1 , ¨¨¨, a n ) is a mutation.

2) ρ 1 is injective:

x 1 i " x 1 j implies y 1 i " y 1 j . If x 1 i P tx 1 , ¨¨¨,
x n u then 1 ď a i , a j ď n. Therefore, by the definition of mutation, x ai " x aj and, because ρ is a flashback, y ai " y aj . By this last equation y 1

i " y 1 j . If x 1 i R tx 1 , ¨¨¨, x n u then a i ą n and a i " a j . Therefore y 1

i " y 1 j by definition of mutation. 3) ρ 1 is a flashback:

x 1 i ‰ y 1 i implies x 1 i ď y 1 i P V 3 . If 1 ď a i ď n then y 1
i " y ai and x 1 i " x ai . Therefore y ai ‰ x ai and we conclude by the hypothesis about ρ that ρ 1 py ai q satisfies the constraint in the definition of flashback. If a i ą n then x 1 , ¨¨¨, x n ď x 1 i P V 1 . Since ρpy i q " x i , by the hypothesis about ρ, x i ď y i P V 2 . Therefore, by definition of mutation, x 1 i ď y i P V 2 . We derive x 1 i ď y 1 i P V 3 by transitivity because V 2 Ď V 3 and y i ď y 1 i P V 3 .

The following Theorem 1 generalizes the property that every permutation has an order, which is the number of applications that return the initial tuple. In the theory of permutations, the order is the least common multiple, in short lcm, of the lengths of the cycles of the permutation. This result is clearly false for mutations because of the presence of duplications and of fresh names. The generalization that holds in our setting uses flashbacks instead of identities. We begin by extending the notion of cycle. Definition 4 (Cycles and sinks). Let µ " ( a 1 , ¨¨¨, a n ) be a mutation and let 1 ď a i1 , ¨¨¨, a i ℓ ď n be pairwise different naturals. Then: i. the term pa i1 ¨¨¨a i ℓ q is a cycle of µ whenever µpa ij q " a ij`1 , with 1 ď j ď ℓ ´1, and µpa i ℓ q " a i1 (i.e., pa i1 ¨¨¨a i ℓ q is the ordinary permutation cycle); ii. the term ra i1 ¨¨¨a i ℓ´1 s ai ℓ is a bound sink of µ whenever a i1 R ta 1 , ¨¨¨, a n u, µpa ij q " a ij`1 , with 1 ď j ď ℓ ´1, and a i ℓ belongs to a cycle;

iii. the term ra i1 ¨¨¨a i ℓ s a , with n ă a ď 2 ˆn, is a free sink of µ whenever a i1 R ta 1 , ¨¨¨, a n u and µpa ij q " a ij`1 , with 1 ď j ď ℓ ´1 and µpa i ℓ q " a.

The length of a cycle is the number of elements in the cycle; the length of a sink is the number of the elements in the square brackets.

For example the mutation ( 5, 4, 8, 8, 3, 5, 8, 3, 3 ) has cycle p3, 8q and has bound sinks r1, 5s 3 , r6, 5s 3 , r9s 3 , r2, 4s 8 , and r7s 8 . The mutation ( 6, 3, 1, 8, 7, 1, 8 ) has cycle p1, 6q, has bound sink r2, 3s 1 and free sinks r4s 8 and r5, 7s 8 . Cycles and sinks are an alternative description of a mutation. For instance p3, 8q means that the mutation moves the element in position 8 to the element in position 3 and the one in position 3 to the position 8; the free sink r5, 7s 8 means that the element in position 7 goes to the position 5, whilst a fresh name goes in position 7.

Theorem 1. Let µ be a mutation, ℓ be the lcm of the length of its cycles, ℓ 1 and ℓ 2 be the lengths of its longest bound sink and free sink, respectively. Let also

k def " maxtℓ`ℓ 1 , ℓ 2 u. Then there exists 0 ď h ă k such that @ V, px 1 , ¨¨¨, x n q D µ h ÝÑ @ V 1 , py 1 , ¨¨¨, y n q D µ k´h ÝÑ @ V 2 , pz 1 , ¨¨¨, z n q D
and ρpz 1 , ¨¨¨, z n q " py 1 , ¨¨¨, y n q, for some V 2 -flashback ρ. The value k is called order of µ and denoted by o µ .

Proof. Let µ " ( a 1 , ¨¨¨, a n ) be a mutation, and let A " t1, 2, . . . , nuzta 1 , ¨¨¨, a n u.

If A " ∅, then µ is a permutation; hence, by the theory of permutations, the theorem is immediately proved taking ρ as the identity and h " 0.

If A ‰ ∅ then let a P A. By definition, a must be the first element of (i) a bound sink or (ii) a free sink of µ. We write either a P A piq or a P A piiq if a is the first element of a bound or free sink, respectively.

In subcase (i), let ℓ 1 a be the length of the bound sink with subscript a 1 and ℓ a 1 be the length of the cycle of a 1 . We observe that in @ V, px 1 , ¨¨¨,

x n q D µ ℓ 1 a ÝÑ @ U, px 1 1 , ¨¨¨, x 1 n q D µ ℓ a 1 ÝÑ @ W, px 2 1 , ¨¨¨, x 2 n q D we have x 1 a 1 " x 2 a 1 .
In subcase (ii), let ℓ 2 a be the length of the free sink. We observe that in @ V, px 1 , ¨¨¨,

x n q D µ ℓ 2 a ÝÑ @ U, px 1 1 , ¨¨¨, x 1 n q D
we have x a ď x 1 a P U, by definition of mutation.

Let ℓ, ℓ 1 and ℓ 2 as defined in the theorem. Then, if ℓ `ℓ1 ě ℓ 2 we have that @ V, px 1 , ¨¨¨,

x n q D µ ℓ 1 ÝÑ @ V 1 , py 1 , ¨¨¨, y n q D µ ℓ ÝÑ @ V 2 , pz 1 , ¨¨¨, z n q D and ρpz 1 , ¨¨¨, z n q " py 1 , ¨¨¨, y n q, where ρ " rz 1 Þ Ñ y 1 , ¨¨¨, z n Þ Ñ y n s is a V 2 -flashback. If ℓ l1 ă ℓ 2 then @ V, px 1 , ¨¨¨, x n q D µ ℓ 2 ´ℓ ÝÑ @ V 1 , py 1 , ¨¨¨, y n q D µ ℓ ÝÑ @ V 2 , pz 1 , ¨¨¨, z n q D
and ρpz 1 , ¨¨¨, z n q " py 1 , ¨¨¨, y n q, where ρ

" rz 1 Þ Ñ y 1 , ¨¨¨, z n Þ Ñ y n s is a V 2 - flashback.
For example, µ " ( 6, 3, 1, 8, 7, 1, 8 ), has a cycle p1, 6q, bound sink r2, 3s 1 and free sinks r4s 8 and r5, 7s 8 . Therefore ℓ " 2, ℓ 1 " 2 and ℓ 2 " 2. In this case, the values k and h of Theorem 1 are 4 and 2, respectively. In fact, if we apply the mutation µ four times to the pair @ V, px 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 q D , where

V " tpx i , x i q | 1 ď i ď 7u we obtain @ V, px 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 q D µ ÝÑ @ V 1 , px 6 , x 3 , x 1 , y 1 , x 7 , x 1 , y 1 q D µ ÝÑ @ V 2 , px 1 , x 1 , x 6 , y 2 , y 1 , x 6 , y 2 q D µ ÝÑ @ V 3 , px 6 , x 6 , x 1 , y 3 , y 2 , x 1 , y 3 q D µ ÝÑ @ V 4 , px 1 , x 1 , x 6 , y 4 , y 3 , x 6 , y 4 q D where V 1 " V ' x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 ăy 1 and, for i ě 1, V i`1 " V i ' y i´1 ăy i .
We notice that there is a V 4 -flashback ρ from px 1 , x 1 , x 6 , y 4 , y 3 , x 6 , y 4 q (produced by µ 4 ) to px 1 , x 1 , x 6 , y 2 , y 1 , x 6 , y 2 q (produced by µ 2 ).

The language of lams

We use an infinite set of function names, ranged over f, f 1 , g, g 1 ,. . ., which is disjoint from the set V of Section 2. A lam program is a tuple `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r x ℓ q " L ℓ , L ˘where f i p r x i q " L i are function definitions and L is the main lam. The syntax of L i and L is

L ::" 0 | px, yq | fpr xq | L L | L + L
Whenever parentheses are omitted, the operation " " has precedence over " + ". We will shorten L 1 ¨¨¨ L n into iP1..n L i . Moreover, we use T to range over lams that do not contain function invocations.

Let var pLq be the set of names in L. In a function definition fpr xq " L, r x are the formal parameters and the occurrences of names x P r

x in L are bound ; the names var pLqzr x are free.

In the syntax of L, the operations " " and " + " are associative, commutative with 0 being the identity. Additionally the following axioms hold (T does not contain function invocations) T T " T T + T " T T pL 1 + L 2 q " T L 1 + T L 2 and, in the rest of the paper, we will never distinguish equal lams. For instance, fpr uq + px, yq and px, yq + fpr uq will be always identified. 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 ).

Proposition 2. For every T, there exist T 1 , ¨¨¨, T n that are dependencies composed with , such that T " T 1 + ¨¨¨+ T n . Remark 1. Lams are intended to be abstract models of programs that highlight the resource dependencies in the reachable states. The lam T 1 + ¨¨¨+ T n of Proposition 2 models a program whose possibly infinite set of states tS 1 , S 2 , ¨¨¨u is such that the resource dependencies in S i are a subset of those in some T ji , with 1 ď j i ď n. With this meaning, generic lams L 1 + ¨¨¨+ L m are abstractions of transition systems (a standard model of programming languages), where transitions are ignored and states record the resource dependencies and the function invocations.

Remark 2. The above axioms, such as T pL 1 + L 2 q " T L 1 + T L 2 are restricted to terms T that do not contain function invocations. In fact, fpr uq ppx, yq + py, zqq ‰ pfpr uq px, yqq + pfpr uq py, zqq because the two terms have a different number of occurrences of invocations of f, and this is crucial for linear recursion -see Definition 6.

In the paper, we always assume lam programs `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r

x ℓ q " L ℓ , L ˘to be well-defined, namely (1) all function names occurring in L i and L are defined; (2) the arity of function invocations matches that of the corresponding function definition.

Operational semantics. Let a lam context, noted Lr s, be a term derived by the following syntax:

Lr s ::" r s | L Lr s | L +
Lr s As usual LrLs is the lam where the hole of Lr s is replaced by L. The operational semantics of a program `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r

x ℓ q " L ℓ , L ℓ`1 ˘is a transition system whose states are pairs @ V, L D and the transition relation is the least one satisfying the rule:

(Red) fpr xq " L var pLqzr x " r z r w are fresh Lr r w { r z sr r u { r x s " L 1 @ V, Lrfpr uqs D ÝÑ @ V ' r uă r w, LrL 1 s D By (red)
, a lam L is evaluated by successively replacing function invocations with the corresponding lam instances. Name creation is handled with a mechanism similar to that of mutations. For example, if fpxq " px, yq fpyq and fpuq occurs in the main lam, then fpuq is replaced by pu, vq fpvq, where v is a fresh maximal name in some partial order. The initial state of a program with main lam L is @ I L , L D , where I L def " tpx, xq | x P var pLqu. To illustrate the semantics of the language of lams we discuss three examples:

1. `fpx, y, zq " px, yq gpy, zq + py, zq, gpu, vq " pu, vq + pv, uq, fpx, y, zq ȃnd I " tpx, xq, py, yq, pz, zqu. Then @ I, fpx, y, zq D ÝÑ @ I, px, yq gpy, zq + py, zq D ÝÑ @ I, px, yq py, zq + px, yq pz, yq + py, zq D

The lam in the final state does not contain function invocations. This is because the above program is not recursive. Additionally, the evaluation of fpx, y, zq has not created names. This is because names in the bodies of fpx, y, zq and gpu, vq are bound. 2. `f1 pxq " px, yq

f 1 pyq , f 1 pxq ˘and V 0 " tpx 0 , x 0 qu. Then @ V 0 , f 1 px 0 q D ÝÑ @ V 1 , px 0 , x 1 q f 1 px 1 q D ÝÑ @ V 2 , px 0 , x 1 q px 1 , x 2 q f 1 px 2 q D ÝÑ n @ V n`2 , px 0 , x 1 q ¨¨¨ px n`1 , x n`2 q f 1 px n`2 q D where V i`1 " V i ' x i ăx i`1 .
In this case, the states grow in the number of dependencies as the evaluation progresses. This growth is due to the presence of a free name in the definition of f 1 that, as said, corresponds to generating a fresh name at every recursive invocation. 3. `f2 pxq " px, x 1 q + px,

x 1 q f 2 px 1 q, f 2 px 0 q ˘and V 0 " tpx 0 , x 0 qu. Then @ V 0 , f 2 px 0 q D ÝÑ @ V 1 , px 0 , x 1 q + px 0 , x 1 q f 2 px 1 q D ÝÑ @ V 2 , px 0 , x 1 q + px 0 , x 1 q px 1 , x 2 q + px 0 , x 1 q px 1 , x 2 q f 2 px 2 q D ÝÑ n @ V n`2 , px 0 , x 1 q + ¨¨¨+ px 0 , x 1 q ¨¨¨ px n`1 , x n`2 q f 2 px n`2 q D
where V i`1 are as before. In this case, the states grow in the number of " + "-terms, which become larger and larger as the evaluation progresses.

The semantics of the language of lams is nondeterministic because of the choice of the invocation to evaluate. However, lams enjoy a diamond property up-to bijective renaming of (fresh) names. Proposition 3. Let ı be a bijective renaming and ıpVq " tpıpxq, ıpyqq | px, yq P Vu. Let also

@ V, L D ÝÑ @ V 1 , L 1 D and @ ıpVq, Lr ıpr xq { r x s D ÝÑ @ V 2 , L 2 D
, where r x " var pVq. Then piq either there exists a bijective renaming

ı 1 such that @ V 2 , L 2 D " @ ıpV 1 q, L 1 r ıp r x 1 q { r x 1s D ,
where r x 1 " var pV 1 q, piiq or there exist L 3 and a bijective renaming

ı 1 such that @ V 1 , L 1 D ÝÑ @ V 3 , L 3 D and @ V 2 , L 2 D ÝÑ @ ı 1 pV 3 q, L 3 r ı 1 pr zq { r z s D
, where r z " var pV 3 q.

The informative operational semantics. In order to detect the circularity-freedom, our technique computes a lam till every function therein has been adequately unfolded (up-to twice the order of the associated mutation). This is formalized by switching to an "informative" operational semantics where basic terms (dependencies and function invocations) are labelled by so-called histories.

Let a history, ranged over by α, β, ¨¨¨, be a sequence of function names f i1 f i2 ¨¨¨f in . We write f P α if f occurs in α. We also write α n for α ¨¨¨α loomoon n times

. Let α ĺ β if there is α 1 such that αα 1 " β. The symbol ε denotes the empty history.

The informative operational semantics is a transition system whose states are tuples @ V, h F, L D where h F is a set of function invocations with histories and L, called informative lam, is a term as L, except that pairs and function invocations are indexed by histories, i.e. α px, yq and α fpr uq, respectively. Let

addhpα, Lq def " $ ' ' ' ' ' ' & ' ' ' ' ' ' % α px, yq if L " px, yq α fpr xq if L " fpr xq addhpα, L 1 q addhpα, L 2 q if L " L 1 L 2 addhpα, L 1 q + addhpα, L 2 q if L " L 1 + L 2
For example addhpfl, px 4 , x 2 q fpx 2 , x 3 , x 4 , x 5 qq " fl px 4 , x 2 q fl fpx 2 , x 3 , x 4 , x 5 q.

Let also h Lr s be a lam context with histories (dependency pairs and function invocations are labelled by histories, the definition is similar to Lr s).

The informative transition relation is the least one such that

(Red+) fpr xq " L var pLqzr x " r z r w are fresh Lr r w { r z sr r u { r x s " L 1 @ V, h F, h Lr α fpr uqs D ÝÑ @ V ' r uă r w, h F Y t α fpr uqu, h Lraddhpαf, L 1 qs D When @ V, h F, L D ÝÑ @ V 1 , h F 1 , L 1 D
by applying (Red+) to α fpr uq, we say that the term α fpr uq is evaluated in the reduction. The initial informative state of a program with main lam L is @ I L , ∅, addhpε, Lq D . For example, the flh-program `fpx, y, z, uq " px, zq lpu, y, zq , lpx, y, zq " px, yq fpy, z, x, uq , hpx, y, z, uq " pz, xq hpx, y, z, uq fpx, y, z, uq , hpx 1 , x 2 , x 3 , x 4 q has an (informative) evaluation

@ I L , ∅, ε hpx 1 , x 2 , x 3 , x 4 q D ÝÑ @ I L , h F, L h fpx 1 , x 2 , x 3 , x 4 q D ÝÑ @ I L , h F 1 , L hf px 1 , x 3 q hf lpx 4 , x 2 , x 3 q D ÝÑ @ I L 'x 4 ăx 5 , h F 2 , L 1 hfl px 4 , x 2 q hfl fpx 2 , x 3 , x 4 , x 5 q D , where L " h px 3 , x 1 q h hpx 1 , x 2 , x 3 , x 4 q L 1 " L hf px 1 , x 3 q h F " t ε hpx 1 , x 2 , x 3 , x 4 qu h F 1 " h F Y t h fpx 1 , x 2 , x 3 , x 4 qu h F 2 " h F 1 Y t hf lpx 4 , x 2 , x 3 qu.
There is a strict correspondence between the non-informative and informative semantics that is crucial for the correctness of our algorithm in Section 5. Let rr¨ss be an eraser map that takes an informative lam and removes the histories. The formal definition is omitted because it is straightforward.

Proposition 4. 1. If @ V, h F, L D ÝÑ @ V 1 , h F 1 , L 1 D then @ V, rrLss D ÝÑ @ V 1 , rrL 1 ss D ; 2. If @ V, rrLss D ÝÑ @ V 1 , L 1 D then there are h F, h F 1 , L 1 such that rrL 1 ss " L 1 and @ V, h F, L D ÝÑ @ V 1 , h F 1 , L 1 D .
Circularities. Lams record sets of relations on names. The following function 5p¨q, called flattening, makes explicit these relations 5p0q " 0, 5ppx, yqq " px, yq, 5pfpr xqq " 0, 5pL L 1 q " 5pLq 5pL 1 q, 5pL + L 1 q " 5pLq + 5pL 1 q.

For example, if L " fpx, y, zq + px, yq gpy, zq fpu, y, zq + gpu, vq pu, vq + pv, uq then 5pLq " px, yq + pu, vq + pv, uq. That is, there are three relations in L: tpx, yqu and tpu, vqu and tpv, uqu. By Proposition 2, 5pLq returns, up-to the lam axioms, sequences of (pairwise different) -compositions of dependencies.

The operation 5p¨q may be extended to informative lams L in the obvious way: 5p α px, yqq " α px, yq and 5p α fpr xqq " 0.

Definition 5. A lam L has a circularity if 5pLq " px 1 , x 2 q px 2 , x 3 q ¨¨¨ px m , x 1 q T 1 + T 2

for some x 1 , ¨¨¨, x m . A state @ V, L D has a circularity if L has a circularity. Similarly for an informative lam L.

The final state of the fgh-program computation has a circularity; another function displaying a circularity is g in Section 1. None of the states in the examples 1, 2, 3 at the beginning of this section has a circularity.

Linear recursive lams and saturated states

This section develops the theory that underpins the algorithm of Section 5. In order to lightening the section, the technical details have been moved in Appendix B.

We restrict our arguments to (mutually) recursive lam programs. In fact, circularity analysis in non-recursive programs is trivial: it is sufficient to evaluate all the invocations till the final state and verify the presence of circularities therein. A further restriction allows us to simplify the arguments without loosing in generality (cf. the definition of saturation): we assume that every function is (mutually) recursive. We may reduce to this case by expanding function invocation of non-(mutually) recursive functions (and removing their definitions).

Linear recursive functions and mutations. Our decision algorithm relies on interpreting recursive functions as mutations. This interpretation is not always possible: the recursive functions that have an associated mutation are the linear recursive ones, as defined below.

The technique for dealing with the general case is briefly discussed in Section 8 and is detailed in Appendix C. Definition 6. Let `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r x ℓ q " L ℓ , L ˘be a lam program. A sequence f i0 f i1 ¨¨¨f i k is called a recursive history of f i0 if (a) the function names are pairwise different and (b) for every 0 ď j ď k, L ij contains one invocation of f i j`1%k (the operation % is the remainder of the division).

The lam program is linear recursive if (a) every function name has a unique recursive history and (b) if f i0 f i1 ¨¨¨f i k is a recursive history then, for every 0 ď j ď k, L ij contains exactly one invocation of f i j`1%k .

For example, the program `f1 px, yq " px, yq f 1 py, zq f 2 pyq + f 2 pzq , f 2 pyq " py, zq f 2 pzq , L ȋs linear recursive. On the contrary `fpxq " px, yq gpxq , gpxq " px, yq fpxq + gpyq , L is not linear recursive because g has two recursive histories, namely g and gf.

Linearity allows us to associate a unique mutation to every function name. To compute this mutation, let H range over sequences of function invocations. We use the following two rules:

f i α |ù ε f i pr x i q " L i α |ù f i pr x i q f j α |ù Hf i pr xq f i pr x i q " L i var pL i qzr x i " r z r w are fresh Lrf j pr yqs " L i r r w { r z sr r x { r xi s α |ù Hf i pr xqf j pr yq Let ε |ù fpx 1 , ¨¨¨, x n q ¨¨¨fpx 1 1 , ¨¨¨, x 1
n q be the final judgment of the proof tree with leaf fαf |ù ε, where fα is the recursive history of f. Let also

x 1 1 , ¨¨¨, x 1 n zx 1 , ¨¨¨, x n " z 1 , ¨¨¨, z k . Then the mutation of f, written µ f " ( a 1 , ¨¨¨, a n ) is defined by a i " $ & % j if x 1 i " x j n `j if x 1 i " z j Let o f ,
called order of the function f, be the order of µ f . For example, in the flh-program, the recursive history of f is fl and, applying the algorithm above to flf |ù ε, we get ε |ù fpx, y, z, uqlpu, y, zqfpy, z, u, vq. The mutation of f is ( 2, 3, 4, 5 ) and o f " 4. Analogously we can compute o l " 3 and o h " 1.

Saturation. In the remaining part of the section we assume a fixed linear recursive program `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r

x ℓ q " L ℓ , L ˘and let o f1 , ¨¨¨, o f ℓ be the orders of the corresponding functions.

Definition 7. A history α is f-complete if α " β of ,
where β is the recursive history of f. We say that α is complete when it is f-complete, for some f. f-saturating if α " β 1 ¨¨¨β n´1 α 2 n , where β i ĺ pα i q 2 , with α i complete, and α n f-complete. We say that α is saturating when it is f-saturating, for some f.

In the flh-program, o f " 4, o l " 3, and o h " 1, and the recursive histories of f, l and h are equal to fl, to lf and to h, respectively. Then α " pflq 4 is the f-complete history and h 2 pflq 8 and hpflq 8 are f-saturating.

The following proposition is an important consequence of the theory of mutations (Theorem 1) and the semantics of lams (and their axioms). In particular, it states that, if a function invocation f 0 pĂ u 0 q is unfolded up to the order of f 0 then (i) the last invocation f 0 pr vq may be mapped back to a previous invocation by a flashback and (ii) the same flashback also maps back dependencies created by the unfolding of f 0 pr vq.

Proposition 5. Let β " f 0 f 1 ¨¨¨f n be f 0 -complete and let @ V, h F, h L 0 r α f 0 pĂ u 0 qs D ÝÑ n`1 @ V 1 , h F 1 , h L 0 r h L 1 r¨¨¨hL n r αf0¨¨¨fn f 0 p Ć u n`1 qs ¨¨¨ss D
where h F 1 " h F Y t α f 0 pĂ u 0 q, αf0 f 1 pĂ u 1 q, ¨¨¨, αf0¨¨¨fn´1 f n pĂ u n qu and f i p r u i q " L 1 i and addhpαf 0 ¨¨¨f i , L 1 i q " h L i r αf0¨¨¨fi f i`1 pĆ u i`1 qs (unfolding of the functions in the complete history of f 0 ). Then there is a αf0¨¨¨f h´1 f h pĂ u h q P h F 1 and a

V 1 -flashback ρ such that 1. f 0 pρp Ć u n`1 qq " f h pĂ u h q (hence f 0 " f h ); 2. let f 0 p Ć u n`1 q " L and 5pLq " T 1 + ¨¨¨+ T k and 5p h L 0 r h L 1 r¨¨¨hL n r αβ f 0 p Ć u n`1 qs ¨¨¨ssq " h T 1 1 + ¨¨¨+ h T 1 k 1 .
Then, for every 1 ď i ď k, there exists 1 ď j ď k 1 such that h T 1 j " addhpαf 0 ¨¨¨f h´1 , T i q h T 2 j , for some h T 2 j .

The notion of f-saturating will be used to define a "saturated" state, i.e., a state where the evaluation of programs may safely (as regards circularities) stop. Definition 8. An informative lam @ V, h F, L D is saturated when, for every h Lr s and fpr uq such that L " h Lr α fpr uqs, α has a saturating prefix.

It is easy to check that the following informative lam generated by the computation of the flh-program is saturated:

@ V 7 , h F, h 2 hpx 1 , x 2 , x 3 , x 4 q 0ďiď8 hfplfq i px i`1 , x i`3 q 0ďiď8 hpflq i px i`3 , x i`1 q hpflq 8 fpx 9 , x 10 , x 11 , x 12 q D , where V i`1 " V i ' x i`4 ăx i`5 , and h F " t ε hpx 1 , x 2 , x 3 , x 4 q, h hpx 1 , x 2 , x 3 , x 4 qu Yt hpflq i fpx i`1 , x i`2 , x i`3 , x i`4 q | 0 ď i ď 7u Y t hfplfq i lpx i`4
, x i`2 , x i`3 q | 0 ď i ď 7u. Every preliminary statement is in place for our key theorem that details the mapping of circularities created by transitions of saturated states to past circularities.

Theorem 2. Let @ I L , ∅, addhpε, Lq D ÝÑ ˚@V, h F, L D and @ V, h F, L D be a sat- urated state. If @ V, h F, L D ÝÑ @ V 1 , h F 1 , L 1 D then 1. @ V 1 , h F 1 , L 1 D is saturated; 2.
if L 1 has a circularity then L has already a circularity.

Proof. (Sketch) Item 1. directly follows from Proposition 5. However, this proposition is not sufficient to guarantee that circularities created in saturated states are mapped back to past ones. In particular, the interesting case is the one of crossover circularities, as discussed in Section 1. Therefore, let α1 px 1 , x 2 q, ¨¨¨, α h´1 px h´1 , x h q, α h px h , x h`1 q, ¨¨¨, αn px n , x 1 q be a circularity in L 1 such that α h px h , x h`1 q, ¨¨¨, αn px n , x 1 q were already present in L. Proposition 5 guarantees the existence of a flashback ρ that maps α1 px 1 , x 2 q ¨¨¨ α h´1 px h´1 , x h q to α1 pρpx 1 q, ρpx 2 qq ¨¨¨ α h´1 pρpx h´1 q, ρpx h qq. However, it is possible that α1 pρpx 1 q, ρpx 2 qq ¨¨¨ α h´1 pρpx h´1 q, ρpx h qq α h px h , x h`1 q ¨¨¨ αn px n , x 1 q is no more a circularity because, for example, ρpx h q ‰ x h (assume that ρpx 1 q " x 1 ). Let us discuss this issue. The hypothesis of saturation guarantees that transitions produce histories α 2 β, where α is complete. Additionally, α 1 , ¨¨¨, α h´1 must be equal because they have been created by

@ V, h F, L D ÝÑ @ V 1 , h F 1 , L 1 D
. For simplicity, let β " f and α " fα 1 . Therefore, by Proposition 5, ρ maps α 2 f px 1 , x 2 q ¨¨¨ α 2 f px h´1 , x h q to αf pρpx 1 q, ρpx 2 qq ¨¨¨ αf pρppx h´1 q, ρpx h qq and, ρpx h q ‰ x h when x h is created by the computation evaluating functions in α 1 .

To overcome this problem, it is possible to demonstrate using a statement similar to (but stronger than) Proposition 5 that ρ maps α h px h , x h`1 q ¨¨¨ αn px n , x 1 q to rα h s pρpx h q, ρpx h`1 qq ¨¨¨ rαns pρpx n q, ρpx 1 qq where rα i s are "kernels" of α i where every γ k in α i , with γ a complete history and k ě 2, is replaced by γ. The proof terminates by demonstrating that the term αf pρpx 1 q, ρpx 2 qq ¨¨¨ αf pρppx h´1 q, ρpx h qq rα h s pρpx h q, ρpx h`1 qq ¨¨¨ rαns pρpx n q, ρpx 1 qq is in L (and it is a circularity).

The decision algorithm for detecting circularities in linear recursive lams

The algorithm for deciding the circularity-freedom problem in linear recursive lam programs takes as input a lam program `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r x ℓ q " L ℓ , L ȃnd performs the following steps:

Step 1: find recursive histories. By parsing the lam program we create a graph where nodes are function names and, for every invocation of g in the body of f, there is an edge from f to g. Then a standard depth first search associates to every node its recursive histories (the paths starting and ending at that node, if any). The lam program is linear recursive if every node has at most one associated recursive history.

Step 2: computation of the orders. Given the recursive history α associated to a function f, we compute the corresponding mutation by running α |ù ε (see Section 4). A straightforward parse of the mutation returns the set of cycles and sinks and, therefore, gives the order o f .

Step 3: evaluation process. The main lam is unfolded till the the saturated state. That is, every function invocation fpr xq in the main lam is evaluated up-to twice the order of the corresponding mutation. The function invocation of f in the saturated state is erased and the process is repeated on every other function invocation (which, therefore, does not belong to the recursive history of f), till no function invocation is present in the state. At this stage we use the lam axioms that yield a term T 1 + ¨¨¨+ T n .

Step 4: detection of circularities. Every T i in T 1 + ¨¨¨+ T n may be represented as a graph where nodes are names and edges correspond to dependency pairs. To detect whether T i contains a circular dependency, we run Tarjan algorithm [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF] for connected components of graphs and we stop the algorithm when a circularity is found.

Every preliminary notion is in place for stating our main result; we also make few remarks about the correctness of the algorithm and its computational cost.

Theorem 3. The problem of the circularity-freedom of a lam program is decidable when the program is linear recursive.

The algorithm consists of the four steps described above. The critical step, as far as correctness is concerned, is the third one, which follows by Theorem 2 and by the diamond property in Proposition 3 (whatever other computation may be completed in such a way the final state is equal up-to a bijection to a saturated state).

As regards the computational complexity Steps 1 and 2 are linear with respect to the size of the lam program and Step 4 is linear with respect to the size of the term T 1 + ¨¨¨+ T n . Step 3 evaluates the program till the saturated state. Let o max be the largest order of a function; m max be the maximal number of function invocations in a body, apart the one in the recursive history.

Without loss of generality, we assume that recursive histories have length 1 and that the main lam consists of m max invocations of the same function. Then an upper bound to the length of the evaluation till the saturated state is p2 ˆomax ˆmmax q `p2 ˆomax ˆmmax q 2 `¨¨¨`p2 ˆomax ˆmmax q ℓ

Let k max be the maximal number of dependency pairs in a body. Then the size of the saturated state is Opk max ˆpo max ˆmmax q ℓ q, which is also the computational complexity of our algorithm.

Assessments

The algorithm defined in Section 5 has been prototyped [START_REF] Giachino | Deadlock Framework for ABS (DF4ABS) -online interface[END_REF]. As anticipated in Section 1, our analysis has been applied to a concurrent object-oriented language called ABS [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF], which is a Java-like language with futures and an asynchronous concurrency model (ASP [START_REF] Caromel | Asynchronous and deterministic objects[END_REF] is another language in the same family).

The prototype is part of a bigger framework for the deadlock analysis of ABS programs called DF4ABS (Deadlock Framework for ABS). It is a modular framework which includes two different approaches for analysing lams: DF4ABS/modelcheck (which is the one described in the current paper) and DF4ABS/fixpoint (which is the one described in [START_REF] Giachino | Deadlock analysis of concurrent objects: Theory and practice[END_REF][START_REF] Giachino | A Framework for Deadlock Detection in ABS[END_REF]).

The technique underpinning the DF4ABS/fixpoint tool derives the dependency graph(s) of lam programs by means of a standard fixpoint analysis. To circumvent the issue of the infinite generation of new names, the fixpoint is computed on models with a limited capacity of name creation. This introduces overapproximations that in turn display false positives (for example, DF4ABS/fixpoint returns a false positive for the lam of factorial). In the present work, this limitation of finite models is overcome (for linear recursive programs) by recognizing patterns of recursive behaviors, so that it is possible to reduce the analysis to a finite portion of computation without losing precision in the detection of deadlocks.

The derivation of lams from ABS programs is defined by an inference system [START_REF] Giachino | Deadlock analysis of concurrent objects: Theory and practice[END_REF][START_REF] Giachino | A Framework for Deadlock Detection in ABS[END_REF]. The inference system extracts behavioral types from ABS programs and feeds them to the analyzer. These types display the resource dependencies and the method invocations while discarding irrelevant (for the deadlock analysis) details. There are two relevant differences between inferred types and lams: (i) methods' arguments have a record structure and (ii) behavioral types have the union operator (for modeling the if-then-else statement). To bridge this gap and have some initial assessments, we perform a basic automatic transformation of types into lams.

We tested our prototype on a number of medium-size programs written for benchmarking purposes by ABS programmers and on an industrial case study based on the Fredhopper Access Server (FAS) developed by SDL Fredhoppper [START_REF]Requirement elicitation[END_REF]. This Access Server provides search and merchandising IT services to e-Commerce companies. The (leftmost three columns of the) following table reports the experiments: for every program we display the number of lines, whether the analysis has reported a deadlock (D) or not ( ), the time in seconds required for the analysis. Concerning time, we only report the time of the analysis (and not the one taken by the inference) when they run on a QuadCore 2.4GHz and Gentoo (Kernel 3. [START_REF] Brookes | A theory of communicating sequential processes[END_REF] The rightmost column of the above table reports the results of another tool that have also been developed for the deadlock analysis of ABS programs: DECO [START_REF] Flores-Montoya | May-happen-in-parallel based deadlock analysis for concurrent objects[END_REF]. The technique in [START_REF] Flores-Montoya | May-happen-in-parallel based deadlock analysis for concurrent objects[END_REF] integrates a point-to analysis with an analysis returning (an over-approximation of) program points that may be running in parallel. As for other model checking techniques, the authors use a finite amount of (abstract) object names to ensure termination of programs with object creations underneath iteration or recursion. For example, DECO (as well as DF4ABS/fixpoint) signals a deadlock in programs containing methods whose lam is1 mpx, yq " py, xq mpz, xq that our technique correctly recognizes as deadlock-free.

As highlighted by the above table, the three tools return the same results as regards deadlock analysis, but are different as regards performance. In particular DF4ABS/model-check and DF4ABS/fixpoint are comparable on small/midsize programs, DECO appears less performant (except for PeerToPeer, where DF4ABS/fixpoint is quite slow because of the number of dependencies produced by the fixpoint algorithm). On the FAS module, DF4ABS/model-check and DF4ABS/fixpoint are again comparable -their computational complexity is exponential -DECO is more performant because its worst case complexity is cubic in the dimension of the input. As we discuss above, this gain in performance is payed by DECO in a loss of precision.

Our final remark is about the proportion between linear recursive functions and nonlinear ones in programs. This is hard to assess and our answer is perhaps not enough adequate. We have parsed the three case-studies developed in the European project HATS [START_REF]Requirement elicitation[END_REF]. The case studies are the FAS module, a Trading System (TS) modeling a supermarket handling sales, and a Virtual Office of the Future (VOF) where office workers are enabled to perform their office tasks seamlessly independent of their current location. FAS has 2645 code-lines, TS has 1238 code-lines, and VOF has 429 code-lines. In none of them we found a nonlinear recursion, TS and VOF have respectively 2 and 3 linear recursions (there are recursions in functions on data-type values that have nothing to do with locks and control). This substantiates the usefulness of our technique in these programs; the analysis of a wider range of programs is matter of future work.

Related works

The solutions in the literature for deadlock detection in infinite state programs either give imprecise answers or do not scale when, for instance, programs also admit dynamic resource creation. Two basic techniques are used: type-checking and model-checking.

Type-based deadlock analysis has been extensively studied both for process calculi [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Suenaga | Type-based deadlock-freedom verification for non-blockstructured lock primitives and mutable references[END_REF][START_REF] Vasconcelos | Type inference for deadlock detection in a multithreaded polymorphic typed assembly language[END_REF] and for object-oriented programs [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]. In Section 1 we have thoroughly discussed our position with respect to Kobayashi's works; therefore we omit here any additional comment. In the other contributions about deadlock analysis, a type system computes a partial order of the deadlocks in a program and a subject reduction theorem proves that tasks follow this order. On the contrary, our technique does not compute any ordering of deadlocks, thus being more flexible: a computation may acquire two deadlocks in different order at different stages, thus being correct in our case, but incorrect with the other techniques. A further difference with the above works is that we use behavioral types, which are terms in some simple process algebras [START_REF] Laneve | The must preorder revisited[END_REF]. The use of simple process algebras to guarantee the correctness (= deadlock freedom) of interacting parties is not new. This is the case of the exchange patterns in ssdl [START_REF] Parastatidis | MEP SSDL Protocol Framework[END_REF], which are based on CSP [START_REF] Brookes | A theory of communicating sequential processes[END_REF] and pi-calculus [START_REF] Milner | A calculus of mobile processes[END_REF], of session types [START_REF] Gay | Types and typechecking for communicating quantum processes[END_REF], or of the terms in [START_REF] Nielson | Higher-order concurrent programs with finite communication topology[END_REF] and [START_REF] Chaki | Types as models: model checking message-passing programs[END_REF], which use CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. In these proposals, the deadlock freedom follows by checking either a dual-type relation or a behavioral equivalence, which amounts to model checking deadlock freedom on the types.

As regards model checking techniques, in [START_REF] Carlsson | On cyclic process dependencies and the verification of absence of deadlocks in reactive systems[END_REF] circular dependencies among processes are detected as erroneous configurations, but dynamic creation of names is not treated. An alternative model checking technique is proposed in [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF] for multi-threaded asynchronous communication languages with futures (as ABS). This technique is based on vector systems and addresses infinite-state programs that admit thread creation but not dynamic resource creation.

The problem of verifying deadlocks in infinite state models has been studied in other contributions. For example, [START_REF] Schrter | Reachability analysis using net unfoldings[END_REF] compare a number of unfolding algorithms for Petri Nets with techniques for safely cutting potentially infinite unfoldings. Also in this work, dynamic resource creation is not addressed. The techniques conceived for dealing with dynamic name creations are the so-called nominal techniques, such as nominal automata [START_REF] Segoufin | Automata and logics for words and trees over an infinite alphabet[END_REF][START_REF] Neven | Towards regular languages over infinite alphabets[END_REF] that recognize languages over infinite alphabets and HD-automata [START_REF] Montanari | An introduction to history dependent automata[END_REF], where names are explicit part of the operational model. In contrast to our approach, the models underlying these techniques are finite state. Additionally, the dependency relation between names, which is crucial for deadlock detection, is not studied.

Conclusions and future work

We have defined an algorithm for the detection of deadlocks in infinite state programs, which is a decision procedure for linear recursive programs that feature dynamic resource creation. This algorithm has been prototyped [START_REF] Giachino | Deadlock Framework for ABS (DF4ABS) -online interface[END_REF] and currently experimented on programs written in an object-oriented language with futures [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF]. The current prototype deals with nonlinear recursive programs by using a source-to-source transformation into linear ones. This transformation may introduce fake dependencies (which in turn may produce false positives in terms of circularities). To briefly illustrate the technique, consider the program `hptq " pt, xq pt, yq hpxq hpyq , hpuq ˘,

Our transformation returns the linear recursive one: `haux pt, t 1 q " pt, xq pt, x 1 q pt 1 , xq pt 1 , x 1 q h aux px, x 1 q , hpuq " h aux pu, uq , hpuq ˘.

To highlight the fake dependencies added by h aux , we notice that, after two unfoldings, h aux pu, uq gives pu, vq pu, wq pv, v 1 q pv, w 1 q pw, v 1 q pw, w 1 q h aux pv 1 , w 1 q while hpuq has a corresponding state (obtained after four steps) pu, vq pu, wq pv, v 1 q pv, v 2 q pw, w 1 q pw, w 2 q hpv 1 q hpv 2 q hpw 1 q hpw 2 q , and this state has no dependency between names created by different invocations.

It is worth to remark that these additional dependencies cannot be completely eliminated because of a cardinality argument. The evaluation of a function invocation fpr uq in a linear recursive program may produce at most one invocation of f, while an invocation of fpr uq in a nonlinear recursive program may produce two or more. In turn, these invocations of f may create names (which are exponentially many in a nonlinear program). When this happens, the creations of different invocations must be contracted to names created by one invocation and explicit dependencies must be added to account for dependencies of each invocation. [Our source-to-source transformation is sound: if the transformed linear recursive program is circularity-free then the original nonlinear one is also circularity-free. So, for example, since our analysis lets us determine that the saturated state of h aux is circularity-free, then we are able to infer the same property for h.] We are exploring possible generalizations of our theory in Section 4 to nonlinear recursive programs that replace the notion of mutation with that of group of mutations. This research direction is currently at an early stage.

Another obvious research direction is to apply our technique to deadlocks due to process synchronizations, as those in process calculi [START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. In this case, one may take advantage of Kobayashi's inference for deriving inter-channel dependency informations and manage recursive behaviors by using our algorithm (instead of the one in [START_REF] Kobayashi | [END_REF]).

There are several ways to develop the ideas here, both in terms of the language features of lams and the analyses addressed. As regards the lam language, [START_REF] Giachino | Deadlock analysis of concurrent objects: Theory and practice[END_REF] already contains an extension of lams with union types to deal with assignments, data structures, and conditionals. However, the extension of the theory of mutations and flashbacks to deal with these features is not trivial and may yield a weakening of Theorem 2. Concerning the analyses, the theory of mutations and flashbacks may be applied for verifying properties different than deadlocks, such as state reachability or livelocks, possibly using different lam languages and different notions of saturated state. Investigating the range of applications of our theory and studying the related models (corresponding to lams) are two issues that we intend to pursue.

A Java code of the factorial function

There are several Java programs implementing factorial in Section 1. However our goal is to convey some intuition about the differences between TyPiCal and our technique, rather than to analyze the possible options. One option is the code Since factorial is synchronized, the corresponding thread acquires the lock of its object -let it be this -before execution and releases the lock upon termination. We notice that factorial, in case n>0, delegates the computation of factorial to a separate thread on a new object of Maths, called y. This means that no other synchronized thread on this may be scheduled until the recursive invocation on y terminates. Said formally, the runtime Java configuration contains an object dependency pthis, yq. Repeating this argument for the recursive invocation, we get configurations with chains of dependencies pthis, yq, py, zq, ¨¨¨, which are finite by the well-foundedness of naturals.

B Proof of Theorem 2.

This section develops the technical details for proving Theorem 2. Definition 9. A history α is f-yielding if α " α h1 1 β 1 ¨¨¨α hn n β n such that, for every i, α i is a recursive history, β i ĺ α i , and α " α 1 f i implies the program has the definition f i pr x i q " Lrfpr uqs, for some r u. The kernel of α, denoted rαs, is α

h 1 1 1 β 1 ¨¨¨α h 1 n n β n , where h 1 i " minph i , 1q.
By definition, if α is f-saturating then it is also f-yielding. In this case, the kernel rαs has a suffix that is f-complete. In the flh-program, o f " 4, o l " 3, and o h " 1, and the recursive histories of f, l and h are equal to fl, to lf and to h, respectively. Then α " pflq 4 is the f-complete history and α 1 " h 2 f is l-yielding, with rα 1 s " hf.

We notice that every history of an informative lam (obtained by evaluating @ I L , ∅, addhpε, Lq D ) is a yielding sequence. We also notice that, for every f, ε is f-yielding. In fact, ε is the history of every function invocation in the initial lam, which may concern every function name of the program. As regards the kernel, in Lemma 1, we demonstrate that, if α " α h1 1 β 1 ¨¨¨α hn n β n is a f-yielding history such that every h i ě 2, then every term α fpr uq may be mapped by a flashback ρ to a term rαs fpρpr uqq; similarly for dependencies. This is the basic property that allows us to map circularities to past circularities (see Theorem 2).

Next we introduce an ordering relation over renamings, (in particular, flashbacks) and the operation of renaming composition. The definitions are almost standard:

ρ ĺ fb ρ 1 if, for every x P dompρq, ρpxq " ρ 1 pxq.

ρ ˝ρ1 be defined as follows:

pρ ˝ρ1 qpxq def " " ρ 1 pxq if ρ 1 pxq R dompρq ρpρ 1 pxqq otherwise
We notice that, if both 1. ρ and ρ 1 are flashbacks and 2. for every x P dompρq, ρ 1 pxq " x then ρ ĺ fb ρ ˝ρ1 holds. In the following, lams 5pLq and 5pLq, being + of terms that are dependencies composed with , will be written T 1 + ¨¨¨+ T m and h T 1 + ¨¨¨+ h T m , for some m, respectively, where T i and h T i contain dependencies px, yq and α px, yq. Let also ρp iPI px i , y i qq " iPI pρpx i q, ρpy i qq.

With an abuse of notation, we will use the set operation "P" for L and h L. For instance, we will write L 1 P L when there is Lr s such that L " LrL 1 s. Similarly, we will write T P T 1 + ¨¨¨+ T n when there is T i such that T P T i .

A consequence of the axiom T pL 1 + L 2 q " T L 1 + T L 2 is the following property of the informative operational semantics.

Proposition 6. Let @ V 1 , h F, h L 0 r α f 1 pĂ u 1 qs D
be a state of an informative operational semantics. For every 1 ď i ď n, let f i p r u i q " L 1 i and addhpαf 0 ¨¨¨f i , L 1 i q be h L i r αf1¨¨¨fi f i`1 pĆ u i`1 qs. Finally, let

5p h L 1 r¨¨¨hL n r αf1¨¨¨fn f n`1 p Ć u n`1 qs ¨¨¨sq " h T 1 + ¨¨¨+ h T r 5p h L n r αf1¨¨¨fn f n`1 p Ć u n`1 qsq " h T 1 1 + ¨¨¨+ h T 1 r 1 . If αf1¨¨¨fn px, yq addhpα 1 , Tq P h T 1 + ¨¨¨+ h T r then, for every 1 ď j ď r 1 , h T 1 j addhpα 1 , Tq P h T 1 + ¨¨¨+ h T r .
The next lemma allows us to map, through a flashback, terms in a saturated state to terms that have been produced in the past. The correspondence is defined by means of the (regular) structure of histories.

Lemma 1. Let @ I L , ∅, addhpε, Lq D ÝÑ ˚@V, h F, L D and @ V, h F, L D be saturated and 5pLq " h T 1 + ¨¨¨+ h T m . Then 1. if βα n`2 β 1 fpr uq P L, where βα n`2 β 1 is f-yielding, then there are n `1 V- flashbacks ρ p2q β,α,β 1 , ¨¨¨, ρ pn`2q β,α,β 1 such that: (a) βα n`1 β 1 fpρ pn`2q
β,α,β 1 pr uqq P h F; (b) jPJ addhpβα k`1 β j , T 1 j q P h T 1 + ¨¨¨+ h T m where, for every j, β j ĺ α,

implies jPJ addhpβα k β j , ρ pk`1q β,α,β 1 pT 1 j qq P h T 1 + ¨¨¨+ h T m ; (c) βα k`1 β 1 fpr uq P h F implies βα k β 1 fpρ pk`1q
β,α,β 1 pr uqq P h F. 2. if α 1 , ¨¨¨, α k are f 1 -yielding, ¨¨¨, f k -yielding, respectively, then there are flashbacks ρ α1 , ¨¨¨, ρ α k such that (a) if α1 f 1 pr uq P L or α1 f 1 pr uq P h F then rα1s fpρ α1 pr uqq

P h F; (b) if 1ďjďk addhpα j , T j q P h T 1 + ¨¨¨+ h T m then 1ďjďk addhprα j s, ρ αj pTqq P h T 1 + ¨¨¨+ h T m ; (c) if α 1 ĺ α 2 then ρ α1 ĺ fb ρ α2 .
(In particular, if α 1 " βα n`2 β 1 , with β 1 ĺ α, and α 2 " βα n`3 then ρ α1 ĺ fb ρ α2 ).

Proof. (Sketch) As regards item 1, let α " β 1 β 2 and let β 2 β 1 " ff 1 ¨¨¨f m (therefore the length of α is m `1). The evaluation

@ I L , ∅, addhpε, Lq D ÝÑ @V,
h F, L D may be decomposed as follows

@ I L , ∅, addhpε, Lq D ÝÑ ˚@V 1 , h F 1 , h Lr βα n`1 β 1 fp r u 1 qs D ÝÑ ˚@V, h F, L D
By definition of the operational semantics there is the alternative evaluation

@ V 1 , h F 1 , h Lr βα n`1 β 1 fp r u 1 qs D ÝÑ @ V 2 , h F 2 , h Lr h L 1 r βα n`1 β 1 f f 1 pĂ u 1 qss D ÝÑ ˚@V 3 , h F 3 , h Lr h L 1 r h L 1 r¨¨¨hL m r βα n`1 β 1 ff1¨¨¨fm fp Ă u 2 qs ¨¨¨sss D [notice that βα n`1 β 1 ff 1 ¨¨¨f m " βα n`2 β 1 ]. Property (1.a
) is an immediate consequence of Proposition 5; let ̺ pn`2q β,α,β 1 be the flashback for the last state. The property (1.b), when k " n, is also an immediate consequence of Propositions 5 and of 6. In the general case, we need to iterate the arguments on shorter histories and the arguments are similar for (1.c). In order to conclude the proof of item 1, we need an additional argument. By Proposition 3, there exists an evaluation

@ V 3 , h F 3 , h Lr h L 1 r h L 1 r¨¨¨hL m r βα n`1 β 1 ff1¨¨¨fm fp Ă u 2 qs ¨¨¨sss D ÝÑ ˚@V 7 , h F 7 , L 7 D such that @ V 7 , h F 7 , L 7 D and @ V, h F, L D
are identified by a bijective renaming, let it be . We define the ρ pn`2q β,α,β 1 corresponding to the evaluation

@ I L , ∅, addhpε, Lq D ÝÑ ˚@V, h F, L D as ρ pn`2q β,α,β 1 def "  ˝̺pn`2q β,α,β 1 ˝´1
. Similarly for the other ρ pk`1q β,α,β 1 . The properties of item 1 for @ V, h F, L D follow by the corresponding ones for

@ V 3 , h F 3 , h Lr h L 1 r h L 1 r¨¨¨hL m r βα n`1 β 1 ff1¨¨¨fm fp Ă u 2 qs ¨¨¨sss D .
We prove item 2. We observe that a term with history β 0 pα 1 1 q h1 β 1 ¨¨¨β n´1 pα 1 n q hn β n in h F or in L may have no corresponding term (by a flashback) with history β 0 pα 1 1 q h1´1 β 1 pα 1 2 q h2 ¨¨¨β n´1 pα 1 n q hn β n . This is because the evaluation to the saturated state may have not expanded some invocations. It is however true that terms with histories rβ 0 pα 1 1 q h1 β 1 ¨¨¨β n´1 pα 1 n q hn β n s (kernels) are either in h F or in L and the item 2 is demonstrated by proving that a flashback to terms with histories that are kernels does exist.

Let α 1 " β 0 pα 1 1 q h1 β 1 ¨¨¨β n´1 pα 1 n q hn β n be a f-yielding sequence. We proceed by induction on n. When n " 1 there are two cases: h 1 ď 1 and h 1 ě 2. In the first case there is nothing to prove because rαs " α. When h 1 ě 2, since α fits with the hypotheses of Item 1, there exist ρ

p2q β0,α 1 1 ,β1 , ¨¨¨, ρ ph1q β0,α 1 1 ,β1 . Let δ p2q β0,α 1 1 ,β1 " ρ p2q β0,α 1 1 ,β1 and δ pi`1q β0,α 1 1 ,β1 " ρ pi`1q β0,α 1 1 ,β1 rx Þ Ñ x | x P dompδ piq β0,α 1 1 ,β1 qs. We also let ρ α1 " δ p2q β0,α 1 1 ,β1 ˝¨¨¨˝δ ph1q β0,α 1
1 ,β1 and we observe that, by definition of renaming composition, if α 1 ĺ α 2 then ρ α1 ĺ fb ρ α2 . In this case, the items 2.a and 2.b follow by item 1, Proposition 6 and the diamond property of Proposition 3.

We assume the statement holds for a generic n and we prove the case n 1. Let α 1 " ββ n pα 1 n`1 q hn`1 β n`1 and h n`1 ą 0 (because

rβ n pα 1 n`1 q 1 β n`1 s " β n α 1 n`1 β n`1
). We consider the map

ρ α1 def " ρ β ˝δp2q βn,α 1 n`1 ,βn`1 ˝¨¨¨˝δ phn`1q βn,α 1 n`1 ,βn`1
where δ piq βn,α 1 n`1 ,βn`1 , 2 ď i ď h n`1 are defined as above. As before, the items 2.a and 2.b follow by item 1 for δ p2q βn,α 1 n`1 ,βn`1 ˝¨¨¨˝δ phn`1q βn,α 1 n`1 ,βn`1 and by Proposition 6 and the diamond property of Proposition 3. Then we apply the inductive hypothesis for ρ β . The property (2.c) α 1 ĺ α 2 implies ρ α1 ĺ fb ρ α2 is an immediate consequence of the definition.

Every preliminary statement is in place for our key theorem that details the mapping of circularities created by transitions of saturated states to past circularities. For readability sake, we restate the theorem.

Theorem 2. Let @ I L , ∅, addhpε, Lq D ÝÑ ˚@V, h F, L D and @ V, h F, L D be a sat- urated state. If @ V, h F, L D ÝÑ @ V 1 , h F 1 , L 1 D then 1. @ V 1 , h F 1 , L 1 D is saturated; 2.
if L 1 has a circularity then L has already a circularity.

Proof. The item 1. is an immediate consequence of Proposition 5. We prove 2. Let -L " h Lr α fpr uqs;

-fpr uq " L 1 -L 1 " h Lraddhpαf, L 1 qs; -5pLq " 5p h Lr α fpr uqsq " h T 1 + ¨¨¨+ h T p ; -5pL 1 q " T 1 1 + ¨¨¨+ T 1 p 1 ; -5pL 1 q " h T 2
1 + ¨¨¨+ h T 2 q ; -α0 px 0 , x 1 q ¨¨¨ αn px n , x 0 q P h T 2 1 + ¨¨¨+ h T 2 q (it is a circularity). Without loss of generality, we may reduce to the following case (the general case is demonstrated by iterating the arguments below).

Let αf " βpα 1 q m`2 β 1 and let α0 px 0 , x 1 q ¨¨¨ αn px n , x 0 q " 0ďjďn 1 βpα 1 q m`1 β 1 βj px j , x j`1 q

α n 1 `1 px n 1 `1, x n 1 `2q ¨¨¨ αn px n , x 0 q with ε ň β j ĺ β 2 β 1
, where β 1 β 2 " α 1 , and n 1 ă n (otherwise 2 is straightforward because the circularity may be mapped to a previous circularity by ρ pm`2q β,α 1 ,β 1 , see Lemma 1(1.b), or it is already contained in L). This is the case of crossover circularities, as discussed in Section 1.

By Lemma 1,

βpα 1 q m β 1 β0 pρ pm`2q β,α,β 1 px 0 q, ρ pm`2q β,α,β 1 px 1 qq ¨¨¨ βpα 1 q m`1 β 1 β n 1 pρ pm`2q β,α,β 1 px n 1 q, ρ pm`2q β,α,β 1 px n 1 `1qq (1)
is in some h T 2 i . There are two cases. Case 1 : for every n 1 `1 ď i ď n, α i ň βpα 1 q m`1 β 1 . Then, by Lemma 1(1), we have ρ

pm`2q β,α,β 1 px 0 q " ρ pm`1q β,α,β 1 px 0 q and ρ pm`2q β,α,β 1 px n 1 `1q " ρ pm`1q β,α,β 1 px n 1 `1q. Therefore, by Lemma 1(2), p1q α 1 n 1 `1 pρ pm`1q β,α,β 1 px n 1 `1q, ρ pm`1q β,α,β 1 px n 1 `2qq ¨¨¨ α 1 n pρ pm`1q β,α,β 1 px n q, ρ pm`1q β,α,β 1 px 0 qq with suitable α 1 n 1 `1, ¨¨¨, α 1 n , is a circularity in h T 2 1 + ¨¨¨+ h T 2 q .
In particular, whenever, for every n 1 `1 ď i ď n, α i " βpα 1 q m β 1 β i with ε ň β i ĺ β 2 β 1 , the flashback ρ pm`1q β,α,β 1 maps dependencies αi px i , x i`1 q to dependencies

βpα 1 q m´1 β 1 βi pρ pm`1q β,α,β 1 px i q, ρ pm`1q β,α,β 1 px i`1 qq if m ą 0. It is the identity, if m " 0.
Case 2 : there is n 1 `1 ď i ď n such that α i ł βpα 1 q m`2 β 1 . Let this i be n 1 `1. For instance, β " β 1 1 pα 2 q m 1 β 2 1 and α n 1 `1 " β 1 1 pα 2 q m 1 `1β 2 1 pα 3 q m 2 β 3 1 with m 1 ě 2 and m 2 ě 2. In this case it is possible that there is no pair γ py, y 1 q, with γ ľ β 1 1 pα 2 q m 1 , to which map α n 1 `1 px n 1 `1, x n 1 `2q by means of a flashback. To overcome this issue, we consider the flashbacks ρ α0 , ¨¨¨, ρ α n 1 , ρ α n 1 `1 and we observe that

rα0s pρ α0 px 0 q, ρ α0 px 1 qq ¨¨¨ rα n 1 s pρ α n 1 px n 1 q, ρ α n 1 px n 1 `1qq rα n 1 `1 s pρ α n 1 `1 px n 1 `1q, ρ α n 1 `1 px n 1 `2qq ¨¨¨ rαns pρ αn px n q, ρ αn px 1 qq (2)
verifies (a) for every 0 ď i ă n, ρ αi px i`1 q " ρ αi`1 px i`1 q and ρ αn px 0 q " ρ α0 px 0 q; (b) the term ( 2) is a subterm of h T 2 1 + ¨¨¨+ h T 2 q . As regards (a), the property derives by definition of the flashbacks ρ αi and ρ αi`1 in Lemma 1. As regards (b), it follows by Lemma 1(2.b) because α0 px 0 , x 1 q ¨¨¨ αn px n , x 1 q P h T 2 1 + ¨¨¨+ h T 2 q .

C Nonlinear programs: technical aspects

When the lam program is not linear recursive, it is not possible to associate a unique mutation to a function. In the general case, our technique for verifying circularity-freedom consists of transforming a nonlinear recursive program into a linear recursive one and then running the algorithm of the previous section. As we will see, the transformation introduces inaccuracies, e.g. dependencies that are not present in the nonlinear recursive program.

C.1 The pseudo-linear case

In nonlinear recursive programs, recursive histories are no more adequate to capture the mutations defined by the functions. For example, in the nonlinear recursive program (called f 1 g 1 -program) `f1 px, y, zq " px, yq g 1 py, zq, g 1 px, yq " g 1 px, zq f 1 pz, y, yq, L the recursive history of f 1 is f 1 g 1 . The sequence f 1 g 1 g 1 is not a recursive history because it contains multiple occurrences of the function g 1 . However, if one computes the sequences of invocations f 1 px, y, zq ¨¨¨f 1 pr uq, it is possible to derive the two sequences f 1 px, y, zqg 1 py, zqf 1 pz 1 , z, zq and f 1 px, y, zqg 1 py, zq g 1 py, uqf 1 pu 1 , u, uq that define two different mutations ( 4, 3, 3 ) and ( 6, 5, 5 ) (see the definition of mutation of a function). Definition 10. A program `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r

x ℓ q " L ℓ , L ˘is pseudo-linear recursive if, for every f i , the set of functions tf | closurepfq " closurepf i qu contains at most one function with a number of recursive histories greater than 1.

The f 1 g 1 -program above is pseudo-linear recursive, as well as the fibonacci program in Section 1 and the following l 1 -program `l1 px, y, zq " px, yq l 1 py, z, xq + px, uq l 1 pu, u, yq, L ˘.

In these cases, functions have a unique recursive history but there are multiple recursive invocations. On the contrary, the f 1, which we discuss below. Let `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r x ℓ q " L ℓ , L ˘be a lam program, let rechispf i q be the set of recursive histories of f i , and let head pεq " ε and head pfαq " f.

Transformation plÞ Ñl

ú ùñ 1 : Removing multiple recursive histories. We repeatedly apply the rule defining plÞ Ñl ú ùñ 1 . Every instance of the rule selects a function f i with a number of recursive histories greater than one -the hypotheses rechispf i q " tf i f k α, f i β 0 , ¨¨¨, f i β n u and thead pβ 0 q, ¨¨¨, head pβ n quzf k ‰ ∅ -and expands the invocation of f k , with f k ‰ f i . By definition of pseudo-linearity, the other function names in rechispf i q have one recursive history. At each application of the rule the sum of the lengths of the recursive histories of f i decreases. Therefore we eventually unfold the (mutual) recursive invocations of f i till the recursive history of f i is unique. For example, the program `fpxq " px, yq gpxq , gpxq " px, yq fpxq + gpyq , L ȋs transformed into `fpxq " px, yq gpxq , gpxq " px, yq px, zq gpxq + gpyq , L ˘. ú ùñ 2 expands the bodies of pseudo-linear recursive functions till the histories of nonlinear recursive functions have length one. In this rule (and in the following ), we use lam contexts with multiple holes, written Lr s ¨¨¨r s. We write f R Lwhenever there is no invocation of f in L.

Transformation

By the hypotheses of the rule, it applies to a function f i whose next element in the recursive history is f k (by definition of the recursive history, f i ‰ f k ) and whose body L i contains at least two invocations of f k . The rule transforms L i by expanding every invocation of f k . For example, the functions h 2 and l 2 in the h 2 l 2 -program are transformed into h 2 px, yq " px, zq l 2 py, zq + l 2 py, xq , l 2 px, yq " py, xq ppy, z 1 q l 2 pz, z 1 q + l 2 pz, yqq ppz, z 2 q l 2 px, z 2 q + l 2 px, zqq.

The arguments about the termination of the transformation ú ùñ 2 we are reduced to pseudo-linear recursive programs where the nonlinearity is due to recursive, but not mutually-recursive functions (such as fibonacci). The transformation plÞ Ñl ú ùñ 3 removes multiple recursive invocations of nonlinear recursive programs. This transformation is the one that introduces inaccuracies, e.g. pairs that are not present in the nonlinear recursive program.

In the rule of plÞ Ñl ú ùñ 3 we use the auxiliary operator 5 f pLq defined as follows: 5 f p0q " 0, 5 f ppx, yqq " px, yq, 5 f pfpr xqq " 0, 5 f pgpr xqq " gpr xq, if pf ‰ gq, 5 f pL L 1 q " 5 f pLq 5 f pL 1 q, 5 f pL + L 1 q " 5 f pLq + 5 f pL 1 q.

The rule of plÞ Ñl ú ùñ 3 selects a function f i whose body contains multiple recursive invocations and extracts all of them -the term 5 fi pL i q. This term is put in parallel with an auxiliary function invocation -the function f aux i -that collects the arguments of each invocation f i (with names that have been properly renamed). The resulting term, called L aux i is the body of the new function f aux i that is invoked by f i in the transformed program. For example, the function fibonacci fibonaccipr, sq " pr, sq pt, sq fibonaccipr, tq fibonaccipt, sq is transformed into fibonaccipr, sq " fibonacci aux pr, s, r, sq, fibonacci aux pr, s, r 1 , s 1 q " pr, sq pr 1 , s 1 q fibonacci aux pr, t, t, s 1 q where different invocations (fibonaccipr, sq and fibonaccipr 1 , s 1 q) in the original program are contracted into one auxiliary function invocation (fibonacci aux pr, s, r 1 , s 1 q). As a consequence of this step, the creations of names performed by different invocations are contracted to names created by one invocation. This leads to merging dependencies, which, in turn, reduces the precision of the analysis. (As discussed in Section 1, a cardinality argument prevents the inaccuracies introduced by plÞ Ñl ú ùñ 3 from being totally eliminated.) As far as the correctness of the transformations in Table 1 is concerned, we begin by defining a correspondence between states of a pseudo-linear program and those of a linear one. We focus on plÞ Ñl ú ùñ 3 because the proofs of the correctness of the other transformations are straightforward. Definition 11. Let L 2 be the linear program returned by the Transformation 3 of Table 1

applied to L 1 . A state @ V 1 , L 1 D of L 1 is linearized to a state @ V 2 , L 2 D of L 2 , written @ V 1 , L 1 D Ţ lin @ V 2 , L 2 D
, if there exists a surjection σ such that:

1. if px, yq P V 1 then pσpxq, σpyqq P V 2 . 2. if 5pL 1 q " T 1 + ¨¨¨+ T m and 5pL 2 q " T 1 1 + ¨¨¨+ T 1 n , then for every 1 ď i ď m, there exists 1 ď j ď n, such that σpT i q P T 1 j ; 3. if fpr x 1 q P L 1 then either (1) fpσpr x 1 qq in L 2 or (2) there are fpr x 2 q ¨¨¨fpr x k q in L 1 and f aux pr y 1 , ¨¨¨, r y h q in L 2 such that, for every 1 ď k 1 ď k there exists h 1 with σpr x k 1 q " r y h 1 ;

In the following lemma we use the notation LrL 1 s ¨¨¨rL n s defined in terms of standard lam context by p¨¨¨ppLrL 1 sqrL 2 sq ¨¨¨qrL n s.

Lemma 2. Let @ V 1 , L 1 D Ţ lin @ V 2 , L 2 D . Then, @ V 2 , L 2 D ÝÑ @ V 1 2 , L 1 2 D implies there exists @ V 1 , L 1 D ÝÑ ˚@V 1 1 , L 1 1 D such that @ V 1 1 , L 1 1 D Ţ lin @ V 1 2 , L 1 2 D
Proof. Base case. Initially L 1 " L 2 because the main lam is not affected by the transformation. Therefore the first step can only be an invocation of a standard function belonging to both programs. We have two cases:

1. the function was linear already in the original program, thus it was not modified by the transformation. In this case the two programs performs the same reduction step and end up in the same state. 2. the function has been linearized by the transformation. In this case the invocation at the linear side will reduce to an invocation of an aux-function and it will not produce new pairs nor new names. The corresponding reduction in

@ V 1 , L 1 D is a zero-step reduction. It is easy to verify that @ V 1 , L 1 D Ţ lin @ V 1 2 , L 1 2 D .
Inductive case. We consider only the case in which the selected function is an aux-function. The other case is as in the base case. Let

@ V pnq 1 , L pnq 1 rfpr v 1 qs ¨¨¨rfpr v k qs D Ţ lin @ V pnq 2 , L pnq 2 rf aux pr u 1 , ¨¨¨, r u h qs D
Without loss of generality we can assume that L pnq 1

does not contain other invocations to f and the "linearized to" relationship makes fpr v 1 q ¨¨¨ fpr v k q correspond to f aux pr u 1 , ¨¨¨, r u h q.Then we have @

V pnq 2 , L pnq 2 rf aux pr u 1 , ¨¨¨, r u h qs D ÝÑ @ V pnq 2 ' r u 1 , ¨¨¨, r u h ă r w, L pnq 2 rL f aux r r w { r z sr r u1, ¨¨¨, r u h { r y1, ¨¨¨, r y h ss D Proof. A straightforward induction on the length of @ V 1 , L 1 D ÝÑ ˚@V 1 1 , L 1 1 D
. In the inductive step, we need to expand the recursive invocations "at a same level" in order to mimic the behavior of functions f aux . Theorem 4. Let L 1 be a pseudo-linear program and L 2 be the result of the transformations in Table 1

@ V 2 , L 2 D reached by evaluating L 2 , there is @ V 1 , L 1 D that is reached by evaluating L 1 such that @ V 1 , L 1 D Ţ lin @ V 2 , L 2 D
. This guarantees that every circularity in

@ V 1 , L 1 D is also present in @ V 2 , L 2 D
. We conclude by Lemma 3 and Theorem 2.

We observe that, our analysis returns that the fibonacci program is circularity-free.

C.2 The general case

In non-pseudo-linear recursive programs, more than one mutual recursive function may have several recursive histories. The transformation nplÞ Ñpl ú ùñ in Table 2 takes a non-pseudo-linear recursive program and returns a program where the "non-pseudo-linearity" is simpler. Repeatedly applying the transformation, at the end, one obtains a pseudo-linear recursive program.

More precisely, let `f1 pĂ x 1 q " L 1 , ¨¨¨, f ℓ p r x ℓ q " L ℓ , L ˘be a non-pseudo-linear recursive program. Therefore, there are at least two functions with more than one recursive history. One of this function is f j , which is the one that is being explored by the rule nplÞ Ñpl ú ùñ . Let also f i be another function such that closurepf j q " closurepf i q (this f i must exists otherwise the program would be already pseudo-linear recursive). These constraints are those listed in the first line of the premises of the rule. The idea of this transformation is to defer the invocations of the functions in thead pα 1 f j q, ¨¨¨, head pα h`1 f j quzf i , i.e., the functions different from f i that can be invoked within f j 's body, to the body of the function f i . The meaning of the second and third lines of the premises of the rule is to identify the p k different invocations of these m functions (k ě m). Notice that every α 1 , ¨¨¨, α h`1 could be empty, meaning that f j is directly called. At this point, what we need to do is (1) to store the arguments of each invocation of f i1 , ¨¨¨, f im into those of an invocation of f i -actually, a suitable tuple of them, thus the arity of f i is augmented correspondingly -and (2) to perform suitable expansions in the body of f i . In order to augment the arguments of the invocations of f i that occur in the other parts of the program, we use the auxiliary rule fi,n ú ùñ that extends every invocation of f i with n additional arguments that are always fresh names. The fourth line of the premises calculates the number n of additional arguments, based on the number of arguments of the functions that are going to be moved into f i 's body. The last step, described in the last

f R L Ă z1, ¨¨¨, Ą zm are n-tuple of fresh names Lrfp Ă u1qs ¨¨¨rfpĄ umqs f,n ú ùñ Lrfp Ă u1, Ă z1qs ¨¨¨rfpĄ um, Ą zmqs rechispfj q " tfj fiα0, fj α1, ¨¨¨, fj α h`1 u f P fiα0 7prechispfqq ą 1 tfi 1 , ¨¨¨, fi m u " theadpα1fj q, ¨¨¨, headpα h`1 fj quzfi Lj " Lrfp 1 p Ă u1qs ¨¨¨rfp k p Ă u k qs tfp 1 , ¨¨¨, fp k u " tfi 1 , ¨¨¨, fi m u fi 1 , ¨¨¨, fi m R L n " 7p Ă u1 ¨¨¨Ă u k q pL h f i ,n ú ùñ L 1 h q hPt1,¨¨¨,ℓ`1u L 1 j " L 1 rfi 1 p Ă u1qs ¨¨¨rfi m p Ă u k qs Ă z 1 1 , ¨¨¨, Ă z 1 k , ¨¨¨, Ă z k 1 , ¨¨¨, Ă z k k , Ă z1, ¨¨¨, Ă z k , are fresh L 2 j " L 1 rfip Ă z 1 1 , Ă u1, Ă z 1 2 , ¨¨¨, Ă z 1 k qs ¨¨¨rfip Ă z k 1 , ¨¨¨, Ă z k k , Ă u k qs `f1p Ă
x1q " L1, ¨¨¨fipĂ xiq " Li, ¨¨¨, fj pĂ xj q " Lj , ¨¨¨, f ℓ pĂ x ℓ q " L ℓ , L ℓ`1 ˘nplÞ Ñpl ú ùñ `f1p Ă x1q " L 1 1 , ¨¨¨fipĂ xi, Ă z1, ¨¨¨, Ă z k q " L 1 i p qP1..k fp q pĂ zqqq, ¨¨¨, fj pĂ xj q " L 2 j , ¨¨¨, f ℓ pĂ x ℓ q " L 1 ℓ , L 1 ℓ`1 Table 2. Non-pseudo-linear to pseudo-linear transformation line of the premises of the rule, is to replace the invocations of the functions f i1 , ¨¨¨, f im with invocations of f i . Notice that, in each invocation, the position of the actual arguments is different. In the body of f i , after the transformation, the invocations of those functions will be performed passing the right arguments. For example, the f 2 g 2 -program `f2 px, yq " px, zq f 2 py, zq + g 2 py, xq , g 2 px, yq " py, xq f 2 py, zq g 2 pz, xq , f 2 px 1 , x 2 q ȋs rewritten into `f2 px, yq " px, zq g 2 px 1 , y 1 , y, zq + g 2 py, x, z 1 , z 2 q , g 2 px, y, u, vq " py, xq f 2 py, zq g 2 pz, x, x 1 , y 1 q f 2 pu, vq , f 2 px 1 , x 2 q ˘.

The invocation f 2 py, zq is moved into the body of g 2 . The function g 2 has an augmented arity, so that its first two arguments refer to the arguments of the invocations of g 2 in the original program, and the last two arguments refer to the invocation of f 2 . Looking at the body of g 2 , the unchanged part (with the augmented arity of g 2 ) covers the first two arguments; whilst the last two arguments are only used for a new invocation of f 2 .

The correctness of

nplÞ Ñpl ú ùñ is demonstrated in a similar way to the proof of the correctness of plÞ Ñl ú ùñ 3 . We begin by defining a correspondence between states of a non-pseudo-linear program and those of a pseudo-linear one. Definition 12. Let L 2 be the pseudo-linear program returned by the transformation of Table 2

applied to L 1 . A state @ V 1 , L 1 D of L 1 is pseudo-linearized to a state @ V 2 , L 2 D of L 2 , written @ V 1 , L 1 D Ţ pl @ V 2 , L 2 D
, if there exists a surjection σ such that:

1. if px, yq P V 1 then pσpxq, σpyqq P V 2 . 2. if 5pL 1 q " T 1 + ¨¨¨+ T m and 5pL 2 q " T 1 1 + ¨¨¨+ T 1 n , then for every 1 ď i ď m, there exists 1 ď j ď n, such that σpT i q P T 1 j ;

3. if fpr xq P L 1 then either (1) fpσpr xqq in L 2 or (2) there is fpr y 1 ¨¨¨r y k q in L 2 such that, for some 1 ď i ď k, σpr xq " r y i ;

We use the same notational convention for contexts as in Lemma 2.

Lemma 4. Let @ V 1 , L 1 D Ţ pl @ V 2 , L 2 D . Then, @ V 1 , L 1 D ÝÑ @ V 1 1 , L 1 1 D implies there exists @ V 2 , L 2 D ÝÑ `@V 1 2 , L 1 2 D such that @ V 1 1 , L 1 1 D Ţ pl @ V 1 2 , L 1 2 D
Proof. Base case. L 1 is the main lam of the nonlinear program, and L 2 its pseudolinear transformation.

L 1 " L 1 rf 1 pr u 1 qs ¨¨¨rf m pr u k qs, where L 1 does not contain any other function invocations, and m ď k, meaning that some of the f i , 1 ď i ď m, can be invoked more than once on different parameters.

After the transformation, L 2 contains the same pairs as L 1 and the same function invocations, but with possibly more arguments:

L 2 " L 1 rf 1 pr u 1 , r z 1 qs ¨¨¨rf m pr u k , r z k qs.
Notice that some of the r z j , 1 ď j ď k, may be empty if the corresponding function has not been expanded during the transformation. Moreover V 1 and V 2 contains only the identity relations on the arguments, so we have

V 1 Ď V 2 .
Therefore, all conditions of definition 12 are trivially verified.

Inductive case. We have L 1 " L 1 rf 1 pr u 1 qs ¨¨¨rf m pr u k qs, where L 1 does not contain any other function invocations, and m ď k, meaning that some of the f i , 1 ď i ď m, can be invoked more than once on different parameters.

We have L 2 " L 2 rf 1 pr u 1 , r z 1 qs ¨¨¨rf m pr u k , r z k qs.

where L 2 may contain other function invocations, but by inductive hypothesis we know that Definition 12 is verified. In particular condition 3 guarantees that at least the invocations of f 1 , . . . , f m , with suitable arguments, are in L 2 . Now, let us consider the reduction

@ V 1 , L 1 D ÝÑ @ V 1 1 , L 1 1 D .
Without loss of generality, we can assume the reduction step performed an invocation of function f 1 pr u 1 q.

We have different cases:

2. the function's lam L f1 has been affected only in that some function invocations in it have an updated arity. Meaning that it was only trasformed by g,l ú ùñ, for some g and l, as a side effect of other function expansions. It follows that 5pL f1 q " 5pL 1 f1 q, where L 1 f1 is the body of f 1 after the transoformation has been applied. This satisfies condition 2 of Definition 12. Those function invocations that have not been modified satisfy trivially the condition 3 of Definition 12. Regarding the other function invocations we have, by construction, that if gpr xq P L f1 then gpr x, r yq P L 1 f1 , where r y are fresh names. This satisfies condition 3 of Definition 12, as well. As for condition 1, we have

V 1 1 " V 1 ' pr u 1 ă r w 1 q,
where r w are fresh names created in L f1 , and V 1 2 " V 2 ' pr u 1 , r z 1 ă r w 1 , r y 1 , ¨¨¨, r y s q, where r y 1 , ¨¨¨, r y s are the fresh names augmenting the function arities within L 1 f1 . We choose the same fresh names r w 1 and condition 1 is satisfied. 3. the function's lam L f1 has been subject of the expansion of a function. Let L f1 " L f1 rg 1 pr v 1 qs ¨¨¨rg h pr v n qs, where L f1 contains only pairs, then, assuming without loss of generality that g 1 was expanded:

L 1
f1 " L f1 rg 1 pr v 1 , r z 1 1 , . . . , r z 1 r qs ¨¨¨rg 1 pr v n , r z r 1 , . . . , r z r r qs, where r is obtained by subtracting from the number of invocations n the number of occurrences of invocations of g 1 in L 1 f1 . Now, the psedulinear program has to perform the r invocations of g 1 that were not present in the original program, since they have been replaced r invocations of g 2 ¨¨¨g h , in order to reveal the actual invocations g 2 ¨¨¨g h that has been delegated to g 1 body. By construction, the arguments of the invocations where preserved by the transformation, so that if g 2 pr xq is produced by reduction of the nonlinear program, then the pseudolinear program will produce g 2 pr x, r yq, with r y fresh and possibily empty. This satisfy condition 3 of Definition 12. However the body of g 1 may have been transformed in a similar way by expanding another method, let us say g 2 . Then all the invocations of g 2 in g 1 's body that corresponds to the previously delegated function invocations g 2 ¨¨¨g h have to be invoked as well. This procedure has to be iterated until all the corresponding invocations are encountered. Each step of reduction will produce spurious pairs and function invocations, but all of these will be on different new names.

Lemma 5. Let @ V 1 , L 1 D Ţ pl @ V 2 , L 2 D and @ V 1 , L 1 D ÝÑ ˚@V 1 1 , L 1 1 D . Then there are @ V 1 1 , L 1 1 D ÝÑ ˚@V 2 1 , L 2 1 D and @ V 2 , L 2 D ÝÑ ˚@V 1 2 , L 1 2 D such that @ V 2 1 , L 2 1 D Ţ pl @ V 1 2 , L 1 2 D 38
Proof. A straightforward induction on the length of

@ V 1 , L 1 D ÝÑ ˚@V 1 1 , L 1 1 D .
Every preliminary result is in place for the correctness of the transformation nplÞ Ñpl ú ùñ .

Theorem 5. Let L 1 be a non-pseudo-linear program and L 2 be the result of the transformations in Table 2. If L 2 is circularity-free then L 1 is circularity-free.

Proof. By Lemma 4, for every

@ V 1 , L 1 D reached by evaluating L 1 , there is @ V 2 , L 2 D that is reached by evaluating L 2 such that @ V 1 , L 1 D Ţ pl @ V 2 , L 2 D
. This guarantees that every circularity in

@ V 1 , L 1 D is also present in @ V 2 , L 2 D
. We conclude by Lemma 5.

Fig. 2 .

 2 Fig. 2. Flashbacks of circularities

plÞ Ñl ú ùñ 2

 2 are straightforward. Transformation plÞ Ñl ú ùñ 3 : Removing nonlinear recursive invocations. By plÞ Ñl

Table 1 .

 1 2 g 2 -program below `f2 px, yq " px, zq f 2 py, zq + g 2 py, xq , g 2 px, yq " py, xq f 2 py, zq g 2 pz, xq , f 2 px 1 , x 2 q ȋs not pseudo-linear recursive. Pseudo-linearity has been introduced because of the easiness of transforming them into linear recursive programs. The transformation consists of the three rechispfiq " tfif k α, fiβ0, ¨¨¨, fiβnu thead pβ0q, ¨¨¨, head pβnquzf k ‰ ∅ Li " Lrf k pr uqs var pL k qzĂ x k " r Pseudo-linear to linear transformation steps specified in Table

	z	r w are fresh

  , we are reduced to functions that have one recursive history. Yet, this is not enough for a program to be linear recursive, such as the l 1 -program or the following h 2 l 2 -program `h2 px, yq " px, zq l 2 py, zq + l 2 py, xq ,l 2 px, yq " py, xq h 2 py, zq h 2 pz, xq , h 2 px 1 , x 2 q ˘31(the reason is that the bodies of functions may have different invocations of a same function). Rule

	tions. By	plÞ Ñl ú ùñ 2 : Reducing the histories of pseudo-linear recursive func-ú ùñ 1 plÞ Ñl plÞ Ñl

  . If a saturated state of L 2 has no circularity then no state of L 1 has a circularity.

	Proof. The transformations	plÞ Ñl ú ùñ 1 and	plÞ Ñl ú ùñ 2 perform expansions and do not
	introduce inaccuracies. By Lemma 2, for every

The code of a corresponding ABS program is available at the DF4ABS tool website[START_REF] Giachino | Deadlock Framework for ABS (DF4ABS) -online interface[END_REF], c.f. UglyChain.abs.

the function's lam L f1 has not been modified by the transformation. In this case the result follows trivially.

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

where, f aux pr y 1 , ¨¨¨, r y h q " L f aux , var pL f aux qzr y 1 ¨¨¨r y h " r z and r w are fresh names. By construction, L f aux " f aux p r y 1 1 r r y1 { r y s, ¨¨¨, r y 1 k r Ă y k { r y sq iP1..k p5 f pL f qr r yi { r y sq

where fpr yq " L f rfp r y 1 1 qs ¨¨¨rfp r y 1 k qs " L f and f R L f . The corresponding reduction steps of @ V pnq 1 , L pnq 1 rfpr v 1 qs ¨¨¨rfpr v k qs D are the following ones:

and r w i are the fresh names created by the invocation fpr v i q, 1 ď i ď k. We need to show that:

To this aim we observe that:

for every 1 ď k 1 ď k there exists h 1 such that σpr v k 1 q " r u h 1 ; moreover r w " σpĂ w 1 q " ¨¨¨" σp Ă w k q. This satisfies condition 1 of Definition 11; -if pa, bq P L f r r vi { r y s, with a, b P r w i , r v i , then pσpaq, σpbqq P 5 f pL f qr r ui { r y sr r w { r z s, being σ defined as in the previous item, therefore σpaq, σpbq P r w, r u i . Notice that, due to the iP1..k composition in the body of f aux , two pairs sequentially composed in L f may end up in parallel (through σ). The converse never happens. Therefore condition 2 of Definition 11 is satisfied.

if gpr aq P L f we can reason as in the previous item. We notice that function invocations gpr uq that have no counterpart (through σ) in L f r r vi { r y s may be cointained in iP1..k p5 f pL f qr r ui { r y sqr r w { r z s. We do not have to mind about them because the lemma guarantees the converse containment.

in L f r r vi { r y s we have k new invocations of fp r b i,1 q ¨¨¨fp r b i,k q, where r b i,j " r y 1 j r r vj { r y sr r wj { r z s. Therefore in the pseudolinear lam we have k 2 invocations of f, while in the corresponding linear lam we find just one invocation of

We notice that the surjection σ is such that p r y 1 j r Ă uj { r y sr r w { r z s " σp r b 1,j q " ¨¨¨" σp r b k,j q, with 1 ď j ď k. This, together with the previous item, satisfies condition 3 of Definition 11.