Beniamino Accattoli
email: beniamino.accattoli@inria.fr

The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus

It has been a long-standing open problem whether the strong λ-calculus is a reasonable computational model, i.e. whether it can be implemented within a polynomial overhead with respect to the number of β-steps on models like Turing machines or RAM. Recently, Accattoli and Dal Lago solved the problem by means of a new form of sharing, called useful sharing, and realised via a calculus with explicit substitutions. This paper presents a new abstract machine for the strong λ-calculus based on useful sharing, the Useful Milner Abstract Machine, and proves that it reasonably implements leftmost-outermost evaluation. It provides both an alternative proof that the λ-calculus is reasonable and an improvement on the technology for implementing strong evaluation.

Introduction

The higher-order computational model of reference is the λ-calculus, that comes in two variants, weak or strong. Introduced at the inception of computer science as a mathematical approach to computation, it later found applications in the theoretical modelling of programming languages and, more recently, proof assistants. The weak λ-calculus is the backbone of functional languages such as LISP, Scheme, OCAML, or Haskell. It is weak because evaluation does not enter function bodies and, usually, terms are assumed to be closed. By removing these restrictions one obtains the strong λ-calculus, that underlies proof assistants like Coq, Isabelle, and Twelf, or higher-order logic programming languages such as λ-prolog or the Edinburgh Logical Framework. Higher-order features nowadays are also part of mainstream programming languages like Java or Python.

The abstract, mathematical character is both the advantage and the drawback of the higher-order approach. The advantage is that it enhances the modularity and the conciseness of the code, allowing to forget about low-level details at the same time. The drawback is that the distance from low-level details makes its complexity harder to analyse, in particular its main computational rule, called βreduction, at first sight is not an atomic operation. In particular, β can be nasty, and make the program grow at an exponential rate. The number of β-steps, then, does not even account for the time to write down the result, suggesting that it is not a reasonable cost model. This is the size-explosion problem [START_REF] Accattoli | Leftmost-Outermost) Beta Reduction is Invariant, Indeed[END_REF], and affects both the weak and the strong λ-calculus.

The λ-Calculus is Reasonable, Indeed A cornerstone of the theory is that, nonetheless, in the weak λ-calculus the number of β-steps is a reasonable cost model for time complexity analyses [START_REF] Blelloch | Parallelism in sequential functional languages[END_REF]25,[START_REF] Dal Lago | The weak lambda calculus as a reasonable machine[END_REF], where reasonable formally means that it is polynomially related to the cost model of RAM or Turing machines.

For the strong λ-calculus, the techniques developed for the weak one do not work, as wilder forms of size-explosion are possible. A natural candidate cost model from the theory of λ-calculus is the number of (Lévy) optimal parallel steps, but it has been shown by Asperti and Mairson that such a cost model is not reasonable [START_REF] Asperti | Parallel beta reduction is not elementary recursive[END_REF].

It is only very recently that the strong case has been solved by Accattoli and Dal Lago [START_REF] Accattoli | Leftmost-Outermost) Beta Reduction is Invariant, Indeed[END_REF], who showed that the number of leftmost-outermost β-steps to full normal form is a reasonable cost model. The proof of this result relies on two theoretical tools. First, the Linear Substitution Calculus (LSC), an expressive and simple decomposition of the λ-calculus via linear logic and rewriting theory, developed by Accattoli and Kesner [START_REF] Accattoli | A Nonstandard Standardization Theorem[END_REF] as a variation over a calculus by Robin Milner [START_REF] Milner | Local bigraphs and confluence: Two conjectures[END_REF]. Second, useful sharing, a new form of shared evaluation introduced by Accattoli and Dal Lago on top of the LSC. Roughly, the LSC is a calculus where the meta-level operation of substitution used by β-reduction is internalised and decomposed in micro steps, i.e. it is what is usually called a calculus with explicit substitutions. The further step is to realise that some of these micro substitution steps are useless: they do not lead to the creation of other β-redexes, their only aim is to unshare the result and provide the full normal form. Useful evaluation then performs only those substitution steps that are useful, i.e. not useless. By avoiding useless unsharing steps, it computes a shared representation of the normal form of size linear in the number of steps, whose unsharing may cause an exponential blow up in size. This is how the size-explosion problem is circumvented, see [START_REF] Accattoli | Leftmost-Outermost) Beta Reduction is Invariant, Indeed[END_REF] for more explanations. This Paper In this paper we provide an alternative proof that the strong λcalculus is reasonable (actually only of the hard half, that is the simulation of λ-calculus on RAM, the other half being much easier, see [START_REF] Accattoli | On the invariance of the unitary cost model for head reduction[END_REF]), by replacing the LSC with the Useful Milner Abstract Machine. The aim of the paper is threefold:

1. Getting Closer To Implementations: the LSC decomposes β-reduction in micro-steps but omits details about the search for the next redex to reduce. Moreover, in [START_REF] Accattoli | Leftmost-Outermost) Beta Reduction is Invariant, Indeed[END_REF] useful sharing is used as a sort of black box on top of the LSC. Switching to abstract machines provides a solution closer to implementations and internalises useful sharing. 2. The First Reasonable Strong Abstract Machine: the literature on abstract machines for strong evaluation is scarce (see below) and none of the machines in the literature is reasonable. This work thus provides an improvement of the technology for implementing strong evaluation. 3. Alternative Proof : the technical development in [START_REF] Accattoli | Leftmost-Outermost) Beta Reduction is Invariant, Indeed[END_REF] is sophisticated, because a second aim of that paper is to connect some of the used tools (namely useful sharing and the subterm property) with the seemingly unrelated notion of standardisation from rewriting theory. Here we provide a more basic, downto-earth approach, not relying on advanced rewriting theory.

The Useful MAM The Milner Abstract Machine (MAM) is a variant with just one global environment of the Krivine Abstract Machine (KAM), introduced in [1] by Accattoli, Barenbaum, and Mazza. The same authors introduce in [START_REF] Accattoli | A Strong Distillery[END_REF] the Strong MAM, i.e. the extension of the MAM to strong evaluation, that is a version with just one global environment of Cregut's Strong KAM [START_REF] Crégut | Strongly reducing variants of the Krivine abstract machine[END_REF], essentially the only other abstract machine for strong (call-by-name) evaluation in the literature. Both are not reasonable. The problem is that these machines do not distinguish between useful and useless steps.

The Useful MAM introduced in this paper improves the situation, by refining the Strong MAM. The principle is quite basic, let us sketch it. Whenever a β-redex (λx.t)u is encountered, the Strong MAM adds an entry [x u] to the environment E. The Useful MAM, additionally, executes an auxiliary machine on u-the Checking Abstract Machine (Checking AM)-to establish its usefulness. The result of this check is a label l that is attached to the entry [x u] l . Later on, when an occurrence of x is found, the Useful MAM replaces x with u only if the label on [x u] l says that it is useful. Otherwise the machine backtracks, to search for the next redex to reduce.

The two results of the paper are:

1. Qualitative (Theorem 2): the Useful MAM correctly and completely implements leftmost-outermost (LO for short) β-evaluation-formally, the two are weakly bisimilar. 2. Quantitative (Theorem 5): the Useful MAM is a reasonable implementation, i.e. the work done by both the Useful MAM and the Checking AM is polynomial in the number of LO β-steps and in the size of the initial term.

Related Work Beyond Crégut's [START_REF] Crégut | An abstract machine for lambda-terms normalization[END_REF][START_REF] Crégut | Strongly reducing variants of the Krivine abstract machine[END_REF] and Accattoli, Barenbaum, and Mazza's [START_REF] Accattoli | A Strong Distillery[END_REF], we are aware of only two other works on strong abstract machines, García-Pérez, Nogueira and Moreno-Navarro's [START_REF] García-Pérez | Deriving the full-reducing krivine machine from the small-step operational semantics of normal order[END_REF] (2013), and Smith's [27] (unpublished, 2014). Two further studies, de Carvalho's [START_REF] De Carvalho | Execution time of lambda-terms via denotational semantics and intersection types[END_REF] and Ehrhard and Regnier's [START_REF] Ehrhard | Böhm trees, Krivine's machine and the Taylor expansion of lambda-terms[END_REF], introduce strong versions of the KAM but for theoretical purposes; in particular, their design choices are not tuned towards implementations (e.g. rely on a naïve parallel exploration of the term). Semi-strong machines for call-by-value (i.e. dealing with weak evaluation but on open terms) are studied by Grégoire and Leroy [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF] and in a recent work by Accattoli and Sacerdoti Coen [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] (see [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] for a comparison with [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF]). More recent work by Dénès [START_REF] Dénès | Étude formelle d'algorithmes efficaces en algèbre linéaire[END_REF] and Boutiller [START_REF] Boutiller | De nouveaus outils pour manipuler les inductif en Coq[END_REF] appeared in the context of term evaluation in Coq. None of the machines for strong evaluation in the literature is reasonable, in the sense of being polynomial in the number of β-steps. The machines developed by Accattoli and Sacerdoti Coen in [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] are reasonable, but they are developed in a semi-strong setting only. Another difference between [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] and this work is that call-by-value simplifies the treatment of usefulness because it allows to compute the labels for usefulness while evaluating the term, that is not possible in call-by-name. Global environments are explored by Fernández and Siafakas in [START_REF] Fernández | New developments in environment machines[END_REF], and used in a minority of works, e.g. [25,[START_REF] Danvy | A synthetic operational account of call-by-need evaluation[END_REF]. Here we use the terminology for abstract machines coming from the distillation technique in [START_REF] Accattoli | Distilling Abstract Machines[END_REF], related to the refocusing semantics of Danvy and Nielsen [START_REF] Danvy | Refocusing in reduction semantics[END_REF] and introduced to revisit the relationship between the KAM and weak linear head reduction pointed out by Danos and Regnier [START_REF] Danos | Head linear reduction[END_REF]. We do not, however, employ the distillation technique itself.

Proofs All proofs have been omitted. Those of the main lemmas and theorems concerning the Useful MAM can be found in the appendix. The other ones can be found in the longer version on the author's web page.

λ-Calculus and Leftmost-Outermost Evaluation

The syntax of the λ-calculus is given by the following grammar for terms: We define β-reduction → β as follows:

λ-Terms t,
C ::= • | λx.C | Ct | tC • t := t (Cu) t := C t u (λx.C) t := λx.C t (uC
Rule at Top Level Contextual closure (λx.t)u → β t{x u} C t → β C u if t → β u
A term t is a normal form, or simply normal, if there is no u such that t → β u, and it is neutral if it is normal and it is not of the form λx.u (i.e. it is not an abstraction). The position of a β-redex C t → β C u is the context C in which it takes place. To ease the language, we will identify a redex with its position. A derivation d : t → k u is a finite, possibly empty, sequence of reduction steps. We write |t| for the size of t and |d| for the length of d.

Leftmost-Outermost Derivations

The left-to-right outside-in order on redexes is expressed as an order on positions, i.e. contexts.

Definition 1 (Left-to-Right Outside-In Order).

1. The outside-in order: (a) Root:

• ≺ O C for every context C = • ; (b) Contextual closure: If C ≺ O C then C C ≺ O C C for any C .
C ≺ LO C if C ≺ O C or C ≺ L C :
The following are a few examples. For every context C, it holds that

(ax-iLO) • is iLO C is iLO C = λx.C (@l-iLO) Ct is iLO C is iLO (λ-iLO) λx.C is iLO t is neutral C is iLO (@r-iLO) tC is iLO As expected, Lemma 2 (→ LOβ -steps and Contexts). Let t be a λ-term and C a redex in t. C is the LO β redex in t iff C is LO iff C is iLO.

Preliminaries on Abstract Machines

We study two abstract machines, the Useful MAM (Fig. 4) and an auxiliary machine called the Checking AM (Fig. 2).

The Useful MAM is meant to implement LO β-reduction strategy via a decoding function • mapping machine states to λ-terms. Machine states s are given by a code t, that is a λ-term t not considered up to α-equivalence (which is why it is over-lined), and some data-structures like stacks, frames, and environments. The data-structures are used to implement the search for the next LO-redex and a form of micro-steps substitution, and they decode to evaluation contexts for → LOβ . Every state s decodes to a term s, having the shape C s t , where t is the code currently under evaluation and C s is the evaluation context given by the data-structures.

The Checking AM tests the usefulness of a term (with respect to a given environment) and outputs a label with the result of the test. It uses the same states and data-structures of the Useful MAM.

The Data-Structures First of all, our machines are executed on well-named terms, that are those α-representants where all variables (both bound and free) have distinct names. Then, the data-structures used by the machines are defined in Fig. 1,namely: -Stack π: it contains the arguments of the current code; -Frame F : a second stack, that together with π is used to walk through the term and search for the next redex to reduce. The items φ of a frame are of two kinds. A variable x is pushed on the frame F whenever the machines starts evaluating under an abstraction λx. A head argument context t♦π is pushed every time evaluation enters in the right subterm u of an application tu. The entry saves the left part t of the application and the current stack π, to restore them when the evaluation of the right subterm u is over.

-Global Environment E: it is used to implement micro-step evaluation (i.e.
the substitution on a variable occurrence at the time), storing the arguments of β-redexes that have been encountered so far. Most of the literature on abstract machines uses local environments and closures. Having just one global environment E removes the need for closures and simplifies the machine. On the other hand, it forces to use explicit α-renamings (the operation t α in e red and e abs in Fig. 4), but this does not affect the overall complexity, as it speeds up other operations, see [START_REF] Accattoli | Distilling Abstract Machines[END_REF]. The entries of E are of the form [x t] l , i.e. they carry a label l used to implement usefulness, to be explained later on in this section. We write E(x) = [x t] l when E contains [x t] l and E(x) = ⊥ when in E there are no entries of the form [x t] l .

The Decoding Every state s decodes to a term s (see Fig. 3), having the shape

C s t → E , where -t → E is a λ-term
, roughly obtained by applying to the code the substitution induced by the global environment E. More precisely, the operation t → E is called unfolding and it is properly defined at the end of this section.

-C s is a context, that will be shown to be a LO context, obtained by decoding the stack π and the dump F and applying the unfolding. Note that, to improve readability, π is decoded in postfix notation for plugging.

The Transitions According to the distillation approach of [START_REF] Accattoli | Distilling Abstract Machines[END_REF] we distinguish different kinds of transitions, whose names reflect a proof-theoretical view, as machine transitions can be seen as cut-elimination steps [START_REF] Ariola | Sequent calculi and abstract machines[END_REF][START_REF] Accattoli | Distilling Abstract Machines[END_REF]:

-Multiplicatives m : they fire a β-redex, except that if the argument is not a variable then it is not substituted but added to the environment; -Exponentials e : they perform a clashing-avoiding substitution from the environment on the single variable occurrence represented by the current code. They implement micro-step substitution.

-Commutatives c : they locate and expose the next redex according to the LO evaluation strategy, by rearranging the data-structures.

Both exponential and commutative transitions are invisible on the λ-calculus. Garbage collection is here simply ignored, or, more precisely, it is encapsulated at the meta-level, in the decoding function.

Labels for Useful Sharing A label l for a code in the environment can be of three kinds. Roughly, they are:

-Neutral, or l = neu: it marks a neutral term, that is always useless as it is β-normal and its substitution cannot create a redex, because it is not an abstraction; -Abstraction, or l = abs: it marks an abstraction, that is a term that is at times useful to substitute. If the variable that it is meant to replace is applied, indeed, the substitution of the abstraction creates a β-redex. But if it is not applied, it is useless. -Redex, or l = red: it marks a term that contains a β-redex. It is always useful to substitute these terms.

Actually, the explanation we just gave is oversimplified, but it provides a first intuition about labels. In fact in an environment [x t] l : E it is not really t that has the property mentioned by its label, rather the term t → E obtained by unfolding the rest of the environment on t. The idea is that [x t] red states that it is useful to substitute t to later on obtain a redex inside it (by potential further substitutions on its variables coming from E). The precise meaning of the labels will be given by Definition 6, and the properties they encode will be made explicit by Lemma 11. A further subtlety is that the label red for redexes is refined as a pair (red, n), where n is the number of substitutions in E that are needed to obtain the LO redex in t → E . Our machines never inspect these numbers, they are only used for the complexity analysis of Sect. 5.2.

Grafting and Unfoldings

The unfolding of the environment E on a code t is defined as the recursive capture-allowing substitution (called grafting) of the entries of E on t. Given an environment E we define the unfolding of E on a code t as follows:

t → := t t → [x u] l :E := t{{x u}} → E
or equivalently as:

(uw) → E := u → E w → E x → [x u] l :E := u → E (λx.u) → E := λx.u → E x → [y u] l :E := x → E x → := x
For instance, (λx.y)

→ [y xx] neu = λx.(xx).
The unfolding is extended to contexts as expected (i.e. recursively propagating the unfolding and setting • → E = E). Let us explain the need for grafting. In [START_REF] Accattoli | A Strong Distillery[END_REF], the Strong MAM is decoded to the LSC, that is a calculus with explicit substitutions, i.e. a calculus able to represent the environment of the Strong MAM. Matching the representation of the environment on the Strong MAM and on the LSC does not need grafting but it is, however, a quite technical affair. Useful sharing adds many further complications in establishing such a matching, because useful evaluation computes a shared representation of the normal form and forces some of the explicit substitutions to stay under abstractions. The difficulty is such, in fact, that we found much easier to decode directly to the λ-calculus rather than to the LSC. Such an alternative solution, however, has to push the substitution induced by the environment through abstractions, which is why we use grafting.

Lemma 3 (Properties of Grafting and Unfolding).

1. If the bound names of t do not appear free in u then t{x u} = t{{x u}}.

If moreover they do not appear free in

E then t → E {x u → E } = t{x u} → E .

The Checking Abstract Machine

The Checking Abstract Machine (Checking AM) is defined in Fig. 2. It starts executions on states of the form ( , t, , E, ), with the aim of checking the usefulness of t with respect to the environment E, i.e. it walks through t and whenever it encounters a variable x it looks up its usefulness in E.

The Checking AM has six commutative transitions, noted ci with i = 1, .., 6, used to walk through the term, and five output transitions, noted oj with j = 1, .., 5, that produce the value of the test for usefulness, to be later used by the Useful MAM. The exploration is done in two alternating phases, evaluation and backtracking . Evaluation explores the current code towards

' & $ % Frame Code Stack Env Ph Frame Code Stack Env Ph F tu π E c 1 F t u : π E F λx.t u : π E o 1 output (red, 1) F λx.t E c 2 F : x t E F x π E o 2 output (red, n + 1) if E(x) = [x t] (red,n) F x u : π E o 3 output (red, 2) if E(x) = [x t] abs F x π E c 3 F x π E if E(x) = ⊥ or E(x) = [x t] neu or (E(x) = [x t] abs and π = ) F : x t E c 4 F λx.t E F : t♦π u E c 5 F tu π E F t u : π E c 6 F : t♦π u E tu E o 4 output neu λx.t E o 5
output abs Fig. 2: The Checking Abstract Machine (Checking AM).

:= • Cs := F π → E u : π := • u π s := F t π → E = Cs t → E F : t♦π := F t • π F : x := F λx. • where s = (F, t, π, E)
Fig. 3: Decoding.

the head, storing in the stack and in the frame the parts of the code that it leaves behind. Backtracking comes back to an argument that was stored in the frame, when the current head has already been checked. Note that the Checking AM never modifies the environment, it only looks it up.

Let us explain the transitions. First the commutative ones:

-c1 : the code is an application tu and the machine starts exploring the left subterm t, storing u on top of the stack π. -c2 : the code is an abstraction λx.t and the machine goes under the abstraction, storing x on top of the frame F . -c3 : the machine finds a variable x that either has no associated entry in the environment (if E(x) = ⊥) or its associated entry [x t] l in the environment is useless. This can happen if either l = neu, i.e. substituting t would only lead to a neutral term, or l = abs, i.e. substituting t would provide an abstraction, but the stack is empty, and so it is useless to substitute the abstraction because no β-redexes will be obtained. Thus the machine switches to the backtracking phase ( ), whose aim is to undo the frame to obtain a new subterm to explore. -c4 : it is the inverse of c2 , it puts back on the code an abstraction that was previously stored in the frame.

-c5 : backtracking from the evaluation of an argument u, it restores the application tu and the stack π that were previously stored in the frame.

-c6 : backtracking from the evaluation of the left subterm t of an application tu, the machine starts evaluating the right subterm (by switching to the evaluation phase ) with an empty stack , storing on the frame the pair t♦π of the left subterm and the previous stack π.

Then the output transitions:

-o1 : the machine finds a β-redex, namely (λx.t)u and thus outputs a label saying that it requires only one substitution step (namely substituting the term the machine was executed on) to eventually find a β-redex.

-o2 : the machine finds a variable x whose associated entry [x t] (red,n) in the environment is labeled with (red, n), and so outputs a label saying that it takes n + 1 substitution steps to eventually find a β-redex (n plus 1 for the term the machine was executed on).

-o3 : the machine finds a variable x whose associated entry [x t] abs in the environment is labeled with abs, so t is an abstraction, and the stack is nonempty. Since substituting the abstraction will create a β-redex, the machine outputs a label saying that it takes two substitution steps to obtain a β-redex, one for the term the machine was executed on and one for the abstraction t.

-o4 : the machine went through the whole term, that is an application, and found no redex, nor any redex that can be obtained by substituting from the environment. Thus that term is neutral and so the machine outputs the corresponding label. -o5 : as for the previous transition, except that the term is an abstraction, and so the output is the abs label.

The fact that commutative transitions only walk through the code, without changing anything, is formalised by the following lemma, that is crucial for the proof of correctness of the Checking AM (forthcoming Theorem 1).

Lemma 4 (Commutative Transparency).

Let s = (F, u, π, E, ϕ) c1,2,3,4,5,6 (F , u , π , E, ϕ ) = s . Then 1. Decoding Without Unfolding: F u π = F u π , and 2. Decoding With Unfolding: s = s .

For the analysis of the properties of the Checking AM we need a notion of well-labeled environment, i.e. of environment where the labels are consistent with their intended meaning. It is a technical notion also providing enough information to perform the complexity analysis, later on. Moreover, it includes two structural properties of environments: 1) in [x t] l the code t cannot be a variable, and 2) there cannot be two entries associated to the same variables.

-if n = 1 then u is a β-redex, -if n > 1 then u = x and E = E : [y u] l : E with • if n > 2 then l = (red, n -1)
• if n = 2 then l = (red, 1) or (l = abs and C is applicative).

Remark 1. Note that by the definition it immediately follows that if E = E : [x t] (red,n) : E is well-labeled then the length of E , and thus of E, is at least n. This fact is used in the proof of Theorem 3.1.

The study of the Checking AM requires some terminology and two invariants. A state s is initial if it is of the form ( , t, , E, ϕ) with E well-labeled and it is reachable if there are an initial state s and a Checking AM execution ρ : s * s. Both invariants are used to prove the correctness of the Checking AM: the normal form invariant to guarantee that codes labeled with neu and abs are indeed normal or neutral, while the decoding invariant is used for the redex labels.

Lemma 5 (Checking AM Invariants

). Let s = F | u | π | E | ϕ be a
Checking AM reachable state and E be a well-labeled environment.

Normal Form:

(a) Backtracking Code: if ϕ = , then u → E is normal, and if π is non-empty, then u

→ E is neutral; (b) Frame: if F = F : w♦π : F , then w → E is neutral. 2. Decoding: C s is a LO context.
Finally, we can prove the main properties of the Checking AM, i.e. that when executed on t and E it provides a label l to extend E with a consistent entry for t (i.e. such that [x t] l : E is well-labeled), and that such an execution takes time linear in the size of t.

F : x t E F x π E e red F t α π E if E(x) = [x t] (red,n) F x u : π E e abs F t α u : π E if E(x) = [x t] abs F x π E c 3 F x π E if E(x) = ⊥ or E(x) = [x t] neu or (E(x) = [x t] abs and π = ) F : x t E c 4 F λx.t E F : t♦π u E c 5 F tu π E F t u : π E c 6 F : t♦π u E
t α is any code α-equivalent to t such that it is well-named and its bound names are fresh with respect to those in the other machine components.

Fig. 4: The Useful Milner Abstract Machine (Useful MAM).

The Useful Milner Abstract Machine

The Useful MAM is defined in Fig. 4. It is very similar to the Checking AM, in particular it has exactly the same commutative transitions, and the same organisation in evaluating and backtracking phases. The difference with respect to the Useful MAM is that the output transitions are replaced by micro-step computational rules that reduce β-redexes and implement useful substitutions.

Let us explain them:

-Multiplicative Transition m1 : when the argument of the β-redex (λx.t)y is a variable y then it is immediately substituted in t. This happens because 1) such substitution are not costly and 2) because in this way the environment stays compact, see also Remark 2 at the end of the paper. -Multiplicative Transition m2 : if the argument u is not a variable then the entry [x u] l is added to the environment. The label l is obtained by running the Checking AM on u and E. -Exponential Transition e red : the environment entry associated to x is labeled with (red, n) thus it is useful to substitute t. The idea is that in at most n additional substitution steps (shuffled with commutative steps) a β-redex will be obtained. To avoid variable clashes the substitution α-renames t. -Exponential Transition e abs : the environment associates an abstraction to

x and the stack is non empty, so it is useful to substitute the abstraction (again, α-renaming to avoid variable clashes). Note that if the stack is empty the machine rather backtracks using c3 . The Useful MAM starts executions on initial states of the form ( , t, , ), where t is such that any two variables (bound or free) have distinct names, and any other component is empty. A state s is reachable if there are an initial state s and a Useful MAM execution ρ : s * s, and it is final if no transitions apply.

Qualitative Analysis

The results of this subsection are the correctness and completeness of the Useful MAM. Four invariants are required. The normal form and decoding invariants are exactly those of the Checking AM (and the proof for the commutative transitions is the same). The environment labels invariant follows from the correctness of the Checking AM (Theorem 1.2). The name invariant is used in the proof of Lemma 7.

Lemma 6 (Useful MAM Qualitative Invariants). We can now show how every single transition projects on the λ-calculus, and in particular that multiplicative transitions project to LO β-steps. We also need to show that the Useful MAM computes β-normal forms.

Let s = F | u | π | E | ϕ be a
Lemma 8 (Progress, Proof at Page 18). Let s be a reachable final state. Then s is β-normal.

The theorem of correctness and completeness of the machine with respect to → LOβ follows. The bisimulation is weak because transitions other than m are invisible on the λ-calculus. For a machine execution ρ we denote with |ρ| (resp. |ρ| x ) the number of transitions (resp. x-transitions for x ∈ {m, e, c, . . .}) in ρ.

Theorem 2 (Weak Bisimulation, Proof at Page 18). Let s be an initial Useful MAM state of code t.

Quantitative Analysis

The complexity analyses of this section rely on two additional invariants of the Useful MAM, the subterm and the environment size invariants.

The subterm invariant bounds the size of the duplicated subterms and it is crucial. For us, u is a subterm of t if it does so up to variable names, both free and bound. More precisely: define t -as t in which all variables (including those appearing in binders) are replaced by a fixed symbol * . Then, we will consider u to be a subterm of t whenever u -is a subterm of t -in the usual sense. The key property ensured by this definition is that the size |u| of u is bounded by |t|.

Lemma 9 (Useful MAM Quantitative Invariants). Let s = F | u | π | E |
ϕ be a state reachable by the execution ρ from the initial code t 0 .

Subterm:

(a) Evaluating Code:

if ϕ = , then u is a subterm of t 0 ; (b) Stack: any code in the stack π is a subterm of t 0 ; (c) Frame: if F = F : w♦π : F , then any code in π is a subterm of t 0 ; (d) Global Environment: if E = E : [x w] l : E , then w is a subterm of t 0 ; 2. Environment Size: the length of the global environment E is bound by |ρ| m .
The proof of the polynomial bound of the overhead is in three steps. First, we bound the number |ρ| e of exponential transitions of an execution ρ using the number |ρ| m of multiplicative transitions of ρ, that by Theorem 2 corresponds to the number of LO β-steps on the λ-calculus. Second, we bound the number |ρ| c of commutative transitions of ρ by using the number of exponential transitions and the size of the initial term. Third, we put everything together.

Multiplicative vs Exponential Analysis This step requires two auxiliary lemmas.

The first one essentially states that commutative transitions eat normal and neutral terms, as well as LO contexts.

Lemma 10. Let s = F | t | π | E | be a state and E be well-labeled. Then 1. If t → E is a normal term and π = then s * c F | t | π | E | . 2. If t → E is a neutral term then s * c F | t | π | E | . 3. If t = C u with C → E a LO context then there exist F and π such that s * c F | u | π | E | ;
The second lemma uses Lemma 10 and the environment labels invariant (Lemma 6.1) to show that the exponential transitions of the Useful MAM are indeed useful, as they head towards a multiplicative transition, that is towards β-redexes.

Lemma 11 (Useful Exponentials Lead to Multiplicatives). Let s be a reachable state such that s e (red,n) s . e (red,n-1) s . Finally, using the environment size invariant (Lemma 9.2) we obtain the local boundedness property, that is used to infer a quadratic bound via a standard reasoning (already employed in [START_REF] Accattoli | Leftmost-Outermost) Beta Reduction is Invariant, Indeed[END_REF]). Commutative vs Exponential Analysis The second step is to bound the number of commutative transitions. Since the commutative part of the Useful MAM is essentially same as the commutative part of the Strong MAM of [START_REF] Accattoli | A Strong Distillery[END_REF], the proof of such bound is essentially the same as in [START_REF] Accattoli | A Strong Distillery[END_REF]. It relies on the subterm invariant (Lemma 9.1).

|ρ| c ≤ 3 • (1 + |ρ| e ) • |t|.
The Main Theorem Putting together the matching between LO β-steps and multiplicative transitions (Theorem 2), the quadratic bound on the exponentials via the multiplicatives (Theorem 3.2) and the bilinear bound on the commutatives (Theorem 4.3) we obtain that the number of the Useful MAM transitions to implement a LO β-derivation d is at most quadratic in the length of d and linear in the size of t. Moreover, the subterm invariant (Lemma 9.1) and the analysis of the Checking AM (Theorem 1.2) allow to bound the cost of implementing the execution on RAM.

Theorem 5 (Useful MAM Overhead Bound, Proof at Page 20). Let d : t → * LOβ u be a leftmost-outermost derivation and ρ be the Useful MAM execution simulating d given by Theorem 2.2. Then:

1. Length: |ρ| = O((1 + |d| 2 ) • |t|). 2. Cost: ρ is implementable on RAM in O((1 + |d| 2 ) • |t|) steps.
Remark 2. Our bound is quadratic in the number of the LO β-steps but we believe that it is not tight. In fact, our transition m1 is a standard optimisation, used for instance in Wand's [28] (section 2), Friedman et al.'s [START_REF] Friedman | Improving the lazy krivine machine[END_REF] (section 4), and Sestoft's [26] (section 4), and motivated as an optimization about space. In Sands, Gustavsson, and Moran's [25], however, it is shown that it lowers the overhead for time from quadratic to linear (with respect to the number of βsteps) for call-by-name evaluation in a weak setting. Unfortunately, the simple proof used in [25] does not scale up to our setting, nor we have an alternative proof that the overhead is linear. We conjecture, however, that it does.

Proofs of the Main Lemmas and Theorems

Proof of One-Step Weak Bisimulation Lemma (Lemma 7, p. 13)

1. Commutative: the proof is exactly as the one for the Checking AM (Lemma 4.2), that can be found in the longer version of this paper on the author's webpage. 2. Exponential : n) . Then E = E : [x t] (red,n) : E for some environments E , and E . Remember that terms are considered up to α-equivalence.

-Case s = (F, x, π, E, ) e red (F, t α , π, E, ) = s with E(x) = [x t] (red,
s = C s x → E = C s t → E = C s t → E = s
In the chain of equalities we can replace t → E with t → E because by welllabeledness the variables bound by E are fresh with respect to t.

-Case s = (F, x, u : π, E, ) e abs (F, t α , u : π, E, ) = s with E(x) = [x t] abs . The proof that s = s is exactly as in the previous case.

Multiplicative:

-Case s = (F, λx.t, y : π, E, ) m1 (F, t{x y}, π, E, ) = s . Note that C s = F π → E is LO by the decoding invariant (Lemma 6.4). Note also that by the name invariant (Lemma 6.3b) x can only occur in t. Then:

(F, λx.t, y : π, E, ) = F λx.t y : π → E = F (λx.t)y π → E = C s (λx.t → E )y → E → LOβ C s t → E {x y → E } = L.6.3b&L.3.2 C s t{x y} → E = (F, t{x y}, π, E, ) -Case s = (F, λx.t, u : π, E, ) m2 (F, t, π, [x u] l : E, ) = s with u not a variable. Note that C s = F • π → E = F → E • π → E is
LO by the decoding invariant (Lemma 6.4). Note also that by the name invariant (Lemma 6.3b) x can only occur in t. Then:

(F, λx.t, u : π, E, ) = F λx.t u : π → E = F (λx.t)u π → E = F → E (λx.t → E )u → E π → E → LOβ F → E t → E {x u → E } π → E = L.6.3b&L.3.2 F → E t{x u} → E π → E = F t{x u} π → E = L.6.3b&L.3.1 F t{{x u}} π → E = L.6.3b F t π {{x u}} → E = F t π → [x u] l :E = (F, t, π, [x u] l : E, )
Proof of the Progress Lemma (Lemma 8, p. 13)

A simple inspection of the machine transitions shows that final states have the form ( , t, , E, ). Then by the normal form invariant (Lemma 6.2a)

s = t → E is β-normal.

  ) t := uC t As usual, plugging in a context can capture variables, e.g. (λy.( • y)) y = λy.(yy). The plugging C C of a context C into a context C is defined analogously. A context C is applicative if C = C • u for some C and u.

2 .

 2 The left-to-right order: C ≺ L C is defined by: (a) Application: If C ≺ p t and C ≺ p u then Cu ≺ L tC ; (b) Contextual closure: If C ≺ L C then C C ≺ L C C for any C . 3. The left-to-right outside-in order:

Definition 5 (

 5 Fig. 1: Grammars.

Lemma 7 (

 7 One-Step Weak Simulation, Proof at Page 17). Let s be a reachable state. 1. Commutative: if s c1,2,3,4,5,6 s then s = s ; 2. Exponential: if s e red ,e abs s then s = s ; 3. Multiplicative: if s m1,m2 s then s → LOβ s .

1 .

 1 Simulation: for every execution ρ : s * s there exists a derivation d : s → * LOβ s such that |d| = |ρ| m ; 2. Reverse Simulation: for every derivation d : t → * LOβ u there is an execution ρ : s * s such that s = u and |d| = |ρ| m .

1 .; 2 .

 12 If n = 1 then s * c m s If n = 2 then s * c e abs m s or s * c e (red,1) s ; 3. If n > 1 then s * c

Theorem 3 ( 1 . 2 .

 312 Exponentials vs Multiplicatives, Proof at Page 19). Let s be an initial Useful MAM state and ρ : s * s . Local Boundedness: if σ : s * s and |σ| m = 0 then |σ| e ≤ |ρ| m ; Exponentials are Quadratic in the Multiplicatives: |ρ| e ∈ O(|ρ| 2 m ).

  25. Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. pp. 60-84 (2002) 26. Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231-264 (1997) 27. Smith, C.: Abstract machines for higher-order term sharing, Presented at IFL 2014 28. Wand, M.: On the correctness of the krivine machine. Higher-Order and Symbolic Computation 20(3), 231-235 (2007)

  Proof of the Weak Bisimulation Theorem (Thm 2, p. 13) 1. By induction on the length |ρ| of ρ, using the one-step weak simulation lemma (Lemma 7). If ρ is empty then the empty derivation satisfies the statement. If ρ is given by σ : s * s followed by s s then by i.h. there exists e : s → * LOβ s s.t. |e| = |σ| m . Cases of s s : (a) Commutative or Exponential. Then s = s by Lemma 7.1 and Lemma 7.2, and the statement holds taking d := e because |d| = |e| = i.h. |σ| m = |ρ| m . (b) Multiplicative. Then s → LOβ s by Lemma 7.3 and defining d as e followed by such a step we obtain |d| = |e| + 1= i.h. |σ| m + 1 = |ρ| m . 2.We use nf ec (s) to denote the normal form of s with respect to exponential and commutative transitions, that exists and is unique because c ∪ e terminates (termination is given by forthcoming Theorem 3 and Theorem 4, that are postponed because they actually give precise complexity bounds, not just termination) and the machine is deterministic (as it can be seen by an easy inspection of the transitions). The proof is by induction on the length of d. If d is empty then the empty execution satisfies the statement. If d is given by e : t → * LOβ w followed by w → LOβ u then by i.h. there is an execution σ : s * s s.t. w = s and |σ| m = |e|. Note that since exponential and commutative transitions are mapped on equalities, σ can be extended as σ : s * s * e red ,e abs ,c1,2,3,4,5,6 nf ec (s ) with nf ec (s ) = w and |σ | m = |e|. By the progress property (Lemma 8) nf ec (s ) cannot be a final state, otherwise w = nf ec (s ) could not reduce. Then nf ec (s ) m s (the transition is necessarily multiplicative because nf ec (s ) is normal with respect to the other transitions). By the one-step weak simulation lemma (Lemma 7.3) nf ec (s ) = w → LOβ s and by determinism of → LOβ (Lemma 1) s = u. Then the execution ρ defined as σ followed by nf ec (s ) m s satisfy the statement, as |ρ| m = |σ | m + 1 = |σ| m + 1 = |e| + 1 = |d|. Proof of the Exponentials vs Multiplicatives Theorem (Thm 3, p. 15) 1. We prove that |σ| e ≤ |E|. The statement follows from the environment size invariant (Lemma 9.2), for which |E| ≤ |ρ| m . If |σ| e = 0 it is immediate. Then assume |σ| e > 0, so that there is a first exponential transition in σ, i.e. σ has a prefix s * c e s followed by an execution τ : s * s such that |τ | m = 0. Cases of the first exponential transition e : -Case e abs : the next transition is necessarily multiplicative, and so τ is empty. Then |σ| e = 1. Since the environment is non-empty (otherwise e abs could not apply), |σ| e ≤ |E| holds. -Case e (red,n) : we prove by induction on n that |σ| e ≤ n, that gives what we want because n ≤ |E| by Remark 1. Cases: • n = 1) Then τ has the form s * c s by Lemma 11.1, and so |σ| e = 1. • n = 2) Then τ is a prefix of * c e abs or * c e (red,1) by Lemma 11.2. In both cases |σ| e ≤ 2. • n > 2) Then by Lemma 11.3 τ is either shorter or equal to * c e (red,n-1) , and so |σ| e ≤ 2, or it is longer than * c e (red,n-1) , i.e. it writes as * c followed by an execution τ starting with e (red,n-1) . By i.h. |τ | ≤ n -1 and so |σ| ≤ n. 2. This is a standard reasoning: since by local boundedness (the previous point) m-free sequences have a number of e-transitions that are bound by the number of preceding m-transitions, the sum of all e-transitions is bound by the square of m-transitions. It is analogous to the proof of Theorem 7.2.3 in [6]. Proof of Commutatives vs Exponentials Theorem (Thm 4, p. 15) 1. We prove a slightly stronger statement, namely |ρ| c + |ρ| m ≤ (1 + |ρ| e ) • |t|, by means of the following notion of size for stacks/frames/states: | | := 0 |x : F | := |F | |t : π| := |t| + |π| |t♦π : F | := |π| + |F | |(F, t, π, E, )| := |F | + |π| + |t| |(F, t, π, E, )| := |F | + |π| By direct inspection of the rules of the machine it can be checked that: -Exponentials Increase the Size: if s e s is an exponential transition, then |s | ≤ |s| + |t| where |t| is the size of the initial term; this is a consequence of the fact that exponential steps retrieve a piece of code from the environment, which is a subterm of the initial term by Lemma 9.1; -Non-Exponential Evaluation Transitions Decrease the Size: if s a s with a ∈ {m 1 , m 2 , c 1 , c 2 , c 3 } then |s | < |s| (for c 3 because the transition switches to backtracking, and thus the size of the code is no longer taken into account); -Backtracking Transitions do not Change the Size: if s a s with a ∈ { c 4 , c 5 , c 6 } then |s | = |s|. Then a straightforward induction on |ρ| shows that |s | ≤ |s| + |ρ| e • |t| -|ρ| c -|ρ| m i.e. that |ρ| c + |ρ| m ≤ |s| + |ρ| e • |t| -|s |. Now note that | • | is always non-negative and that since s is initial we have |s| = |t|. We can then conclude with |ρ| c + |ρ| m ≤ |s| + |ρ| e • |t| -|s | ≤ |s| + |ρ| e • |t| = |t| + |ρ| e • |t| = (1 + |ρ| e ) • |t| 2. We have to estimate |ρ| c = |ρ| c4 + |ρ| c5 + |ρ| c6 . Note that (a) |ρ| c4 ≤ |ρ| c2 , as c4 pops variables from F , pushed only by c2 ; (b) |ρ| c5 ≤ |ρ| c6 , as c5 pops pairs t♦π from F , pushed only by c6 ; (c) |ρ| c6 ≤ |ρ| c3 , as c6 ends backtracking phases, started only by c3 . Then |ρ| c ≤ |ρ| c2 + 2|ρ| c3 ≤ 2|ρ| c . 3. We have |ρ| c = |ρ| c + |ρ| c ≤ P.2 |ρ| c + 2|ρ| c ≤ P.1 3 • (1 + |ρ| e ) • |t|. Proof of the Useful MAM Overhead Bound Theorem (Thm 5, p. 15) 1. By definition, the length of the execution ρ simulating d is given by |ρ| = |ρ| m + |ρ| e + |ρ| c . Now, by Theorem 3.2 we have |ρ| e = O(|ρ| 2 m ) and by Theorem 4.3 we have |ρ| c = O((1 + |ρ| e ) • |t|) = O((1 + |ρ| 2 m ) • |t|). Therefore, |ρ| = O((1 + |ρ| e ) • |t|) = O((1 + |ρ| 2 m ) • |t|). By Theorem 2.2 |ρ| m = |d|, and so |ρ| = O((1 + |d| 2 ) • |t|). 2. The cost of implementing ρ is the sum of the costs of implementing the multiplicative, exponential, and commutative transitions. Remember that the idea is that variables are implemented as references, so that environment can be accessed in constant time (i.e. they do not need to be accessed sequentially): (a) Commutative: every commutative transition evidently takes constant time. At the previous point we bounded their number with O((1 + |d| 2 ) • |t|), which is then also the cost of all the commutative transitions together. (b) Multiplicative: a m1 transition costs O(|t|) because it requires to rename the current code, whose size is bound by the size of the initial term by the subterm invariant (Lemma 9.1a). A m2 transition also costs O(|t|) because executing the Checking AM on u takes O(|u|) commutative steps (Theorem 1.2), commutative steps take constant time, and the size of u is bound by |t| by the subterm invariant (Lemma 9.1b). Therefore, all together the multiplicative transitions cost O(|d| • |t|). (c) Exponential : At the previous point we bounded their number with |ρ| e = O(|d| 2 ). Each exponential step copies a term from the environment, that by the subterm invariant (Lemma 9.1d) costs at most O(|t|), and so their full cost is O((1 + |d|) • |t| 2 ) (note that this is exactly the cost of the commutative transitions, but it is obtained in a different way). Then implementing ρ on RAM takes O((1 + |d|) • |t| 2 ) steps.

  u, w, r ::= x | λx.t | tu.We use t{x u} for the usual (meta-level) notion of substitution. An abstraction λx.t binds x in t, and we silently work modulo α-equivalence of bound variables, e.g. (λy.(xy)){x y} = λz.(yz). We use fv(t) for the set of free variables of t.Contexts. One-hole contexts C and the plugging C t of a term t into a context C are defined by:

	Contexts	Plugging

  • ≺ L C. Moreover (λx. • )t ≺ O (λx.( • u))t and ( • t)u ≺ L (wt) • . Let t be a λ-term and C a redex of t. C is the leftmost-outermost β-redex (LO β for short) of t if C ≺ LO C for every other β-redex C of t. We write t → LOβ u if a step reduces the LO β-redex. Lemma 1 (Totality of ≺ LO ). If C ≺ p t and C ≺ p t then either C ≺ LO C or C ≺ LO C or C = C . Therefore, → LOβ is deterministic. LO Contexts For the technical development of the paper we need two characterisations of when a context is the position of the LO β-redex. The first, following one, is used in the proofs of Lemma 5.2 and Lemma 6.4. Right Application: whenever C = C tC then t is neutral, and 2. Left Application: whenever C = C C t then C = λx.C . The second characterisation is inductive, and it used to prove Lemma 10.3.

	Definition 2 (LO β-Reduction). The next immediate lemma guarantees that we defined a total order.
	Definition 3 (LO Contexts). A context C is LO if
	1. Definition 4 (iLO Context). Inductive LO β (or iLO) contexts are defined
	by induction as follows:

  Termination and Complexity: the execution of the Checking AM on t and E always terminates, taking O(|t|) steps, moreover 3. Correctness: if E is well-labeled, x is fresh with respect to E and t, and l is the output then [x t] l : E is well-labeled.

	Theorem 1 (Checking AM Properties). Let t be a code and E a global environment. 1. Determinism and Progress: the Checking AM is deterministic and there al-ways is a transition that applies; & Frame Code Stack Env Ph Frame Code Stack Env Ph F tu π E c 1 F t u : π E F λx.t y : π E m 1 F t{x y} π E F λx.t u : π E m 2 F t π [x u] l : E if u is not a variable and l is the output of the Checking AM on u and E 2. ' F λx.t E c 2	$ %

  state reachable from an initial term t 0 . Then: Frame: if F = F : w♦π : F , then w →

	1. Environment Labels: E is well-labeled.
	2. Normal Form:
	(a) Backtracking Code: if ϕ = , then u → E is normal, and if π is non-empty,
	(b)	then u → E is neutral;

E is neutral. 3. Name: (a) Substitutions: if E = E : [x t] : E then x is fresh wrt t and E ; (b) Abstractions and Evaluation: if ϕ = and λx.t is a subterm of u, π, or π (if F = F : w♦π : F ) then x may occur only in t; (c) Abstractions and Backtracking: if ϕ = and λx.t is a subterm of π or π (if F = F : w♦π : F ) then x may occur only in t. 4. Decoding: C s is a LO context.

  Theorem 4 (Commutatives vs Exponentials, Proof at Page 20). Let ρ : s * s be a Useful MAM execution from an initial state of code t. Then: 1. Commutative Evaluation Steps are Bilinear: |ρ| c ≤ (1 + |ρ| e ) • |t|. 2. Commutative Evaluation Bounds Backtracking: |ρ| c ≤ 2 • |ρ| c . 3. Commutative Transitions are Bilinear:


Ali Hassan

El Moussawi

Steven Derrien
email: sderrien@irisa.fr

Superword Level Parallelism aware Word Length Optimization

Many embedded processors do not support floatingpoint arithmetic in order to comply with strict cost and power consumption constraints. But, they generally provide support for SIMD as a mean to improve performance for little cost overhead. Achieving good performance when targeting such processors requires the use of fixed-point arithmetic and efficient exploitation of SIMD data-path. To reduce time-to-market, automatic SIMDization -such as superword level parallelism (SLP) extraction -and float-to-fixed-point conversion methodologies have been proposed. In this paper we show that applying these transformations independently is not efficient. We propose a SLPaware word length optimization algorithm to jointly perform float-to-fixed-point conversion and SLP extraction. We implement the proposed approach in a source-to-source compiler framework and evaluate it on several embedded processors. Experimental results illustrate the validity of our approach.

I. INTRODUCTION

Even though, many embedded processors (such as ARM cortex-A), provide hardware support for floating-point arithmetic, a good number of ultra low power embedded processors (such as ARM cortex-M0/1/3, TI TMS320C64x, Recore XEN-TIUM) do not, in order to reduce die area and/or minimize power consumption. This comes for the cost of restraining programmability to the use of fixed-point arithmetic. However, application prototyping in many domains, such as signal processing and telecommunication applications, employs floating-point representation. Although floating-point can be soft-emulated on such processors, it drastically degrades performance. Instead, fixed-point implementations are preferably used. Hence, float-to-fixed-point conversion is a crucial step for an efficient implementation when targeting such processors. Though, keeping full fixed-point operations precision requires increasingly large word-lengths (WLs) which, unless supported by the target processor, would require software emulation. Rather, quantizations are applied to limit WLs growth and consequently improving performance, for the cost of degrading the application's quality by introducing errors. The conversion process must account for these errors and carefully select WLs that keep the computation's accuracy within an "acceptable" limit while maximizing performance.

This Performance/Accuracy trade-off has been identified and exploited when targeting customizable architectures, in the context of High-level synthesis [START_REF] Kum | Word-length optimization for high-level synthesis of digital signal processing systems[END_REF] for instance, where the designer has more flexibility in customizing WLs supported by the architecture. This is not the case when targeting processors with predefined data-path. However, most embedded processors nowadays provide support for small-scale SIMD. This allows the use of smaller data WLs than the word size (sub-word) and allows the application of an operation on several such (packed) data simultaneously, to ultimately improve performance. Intuitively, using narrower WLs in this context, should translate to better performance on one side -due to increased vectorization factor -but lower quality on the other side. Previous work [START_REF] Menard | Floating-to-fixed-point conversion for digital signal processors[END_REF] follows this intuition when applying float-to-fixed-point conversion. They aim at minimizing WLs without taking into account SLP, which can be applied, independently, later on.

However, this intuition is unrealistically optimistic since, selecting narrower WLs during word-length optimization (WLO) does not necessarily result in performance improvement after applying SLP extraction mainly because WLO is unaware of SLP grouping possibilities and the associated overhead.

In this work, we address this problem by jointly considering SLP extraction and WLO. More specifically:

• We propose a new SLP-aware WLO algorithm. To the best of our knowledge this is the first work to jointly consider both, WLO and SLP extraction. • We implement it as an automated source-to-source compilation flow.

• We test our approach on several embedded processors against some signal processing applications. The paper is organized as follows. In section II, we present some contextual background and related work. Then we present our SLP-aware WLO algorithm and the corresponding source-to-source compilation flow in sections III and IV. Finally we present some experimental results in section V.

II. BACKGROUND AND RELATED WORK A. Superword Level Parallelism

Taking advantage of SIMD capabilities of a processor to improve performance is not an easy task. Fortunately, many approaches to automatically exploit SIMD have been proposed. Among which, superword level parallelism (SLP) which unlike conventional loop vectorization techniques, exploits SIMD opportunities at the basic block level. The aim is to find groups of scalar operations that can be combined together into SIMD groups. An SIMD group is a set of independent and isomorphic operations (performing the same operation type (add, sub, ...)) of the same size that can be implemented using SIMD instructions. The main limiting factor of SLP performance is the overhead associated with data packing/unpacking operations in case the data is not properly organized in memory. Mainly if the data to be loaded from (stored to) memory are not contiguous and properly aligned. If not handled carefully, the overhead of these operations may easily overcome the benefit of SLP, resulting in performance degradation. That's why all SLP extraction algorithms focus on minimizing packing/unpacking operations when selecting SIMD groups.

Larsen and Amarasinghe introduced SLP and proposed an extraction algorithm [START_REF] Larsen | Exploiting Superword Level Parallelism with Multimedia Instruction Sets[END_REF] based on a local heuristic. Many enhancements [START_REF] Larsen | Increasing and Detecting Memory Address Congruence[END_REF], [START_REF] Kudriavtsev | Generation of Permutations for SIMD Processors[END_REF], [START_REF] Shin | Superword-Level Parallelism in the Presence of Control Flow[END_REF] have since been proposed.

In 2012, Liu et al. proposed an alternative SLP extraction algorithm [START_REF] Liu | A Compiler Framework for Extracting Superword Level Parallelism[END_REF] based on a estimation of the global superwords reuse. In a given a basic block, it first constructs the set of all possible SIMD group candidates of size 2, among them, it aims at selecting the "best" conflict-free sub-set. Two SIMD group candidates are in conflict if they contain a common operation or they have a cyclic dependency. The groups are selected iteratively based on an estimation of their contribution to the overall superword reuse over packing/unpacking cost ratio. Whenever a group is selected, all remaining candidates in conflict with it are eliminated, until all conflicts are resolved. In order to extend the groups size beyond 2, the group selection is repeated, after replacing the selected groups in the original basic block, as long as groups size is supported. In this work we use a similar SLP extraction algorithm.

B. Floating-to-fixed-point Conversion

Floating-to-fixed-point conversion generally consists of three main parts: (i) Integer word-length (IWL) determination which is specified based on the data values range. The later can be obtained either by gathering simulation statistics [START_REF] Kum | Autoscaler for c: An optimizing floating-point to integer c program converter for fixed-point digital signal processors[END_REF] or using analytical methods, such as interval arithmetic. The IWL determination is generally used to specify the binarypoint position and the required scaling operations (which are needed to align fixed-point formats and are implemented using shift operations). (ii) Word-length (WL) determination, which together with IWL determine the fixed-point specification. The fractional word-length (FWL) is implicitly obtained from WL and IWL. Hence, WL determination directly affects the computation's accuracy, which can be evaluated by simulation [START_REF] Keding | Fridge: a fixed-point design and simulation environment[END_REF] or using analytical methods [START_REF] Lopez | Fast and accurate computation of the roundoff noise of linear time-invariant systems[END_REF], [START_REF] Menard | Automatic Evaluation of the Accuracy of Fixed-point Algorithms[END_REF], [START_REF] Caffarena | Sqnr estimation of fixed-point dsp algorithms[END_REF]. WLO algorithms [START_REF] Nguyen | Novel algorithms for word-length optimization[END_REF] are used to perform WL determination and generally trade accuracy for performance. (iii) Fixed-point code generation which converts the floating-point code into fixed-point code that implements the fixed-point specification.

Many floating-to-fixed-point conversion methodologies targeting embedded processors have been proposed. Cilio and Corporaal [START_REF] Cilio | Floating Point to Fixed Point Conversion of C Code[END_REF] and Kum et al. [START_REF] Kum | Autoscaler for c: An optimizing floating-point to integer c program converter for fixed-point digital signal processors[END_REF] presented similar methods allowing the conversion of floating-point C code into fixedpoint C code targeting embedded processors with different methods for determining IWLs. However, both approaches consider only the target's native data WL and consequently no WLO is performed.

Menard et al. [START_REF] Menard | Floating-to-fixed-point conversion for digital signal processors[END_REF] proposed a float-to-fixed-point conversion methodology targeting embedded processors and taking into account their SIMD capabilities. Indeed, they consider the different WLs (due to SIMD) supported by the target processor and they perform a WLO that aims at selecting for each operation, the instruction (i.e. the WL) that minimizes the overall execution time, subject to an accuracy constraint. The relative execution time associated to an instruction is directly related to the WL of data on which it can operate. For example an execution time of 1 and 0.5, respectively, is associated to 32-bit scalar instruction and 2x16-bit SIMD instruction performing the same operation type. While this approach exposes potential SLP opportunities, by favoring the selection of smaller WLs, it still considers SLP extraction as a completely independent transformation that can be applied afterward. Consequently, during WLO it assumes that, when an SIMD instruction is selected to implement a (scalar) operation, N (depending on the SIMD vector size) such operations will ultimately be executed in parallel by the same instruction -if SLP extraction is later applied -without actually knowing whether or not this is possible. Furthermore, this also ignores the potential overhead associated with data packing/unpacking operations. These assumptions are very optimistic and unrealistic.

To the best of our knowledge, no other work dealing with WLO and SIMD has been proposed.

III. JOINT WLO AND SLP EXTRACTION

Applying WLO without taking into account SLP extraction constraints will most likely yield inefficient solutions. That is because WLO decisions directly dictate the search space of SLP extraction. It may prevent, otherwise possible, SIMD grouping candidates by attributing different WLs for operations that can be, otherwise, grouped together (all operations in a SIMD group must have the same WL).

It is very important to note that WLO is performed under accuracy constraint. In another word, only a limited accuracydegradation budget can be used by WLO to try to improve performance as much as possible. In this context, the impact on performance greatly depends on how well SIMD capabilities are being exploited. It is not wise for the WLO to spend the accuracy-degradation budget on optimizing operations that cannot be efficiently exploited by SLP to improve performance. If WLO is unaware of SIMD grouping possibilities and their associated overhead, it may blindly optimize WLs of operations that cannot form a SIMD group (either due to dependencies or conflicts with other groups) or have a high packing/unpacking overhead.

Besides, the scaling operations can have a major impact on performance, so they should be taken into account as well.

In order to address these problems, we propose an approach that jointly performs WLO and SLP extraction. We couple an accuracy-aware SLP extraction algorithm with a SLP-aware WLO algorithm. In the remainder of this section we present these algorithms.

A. SLP-aware WLO algorithm

The fixed-point specification, representing the set of fixedpoint formats of each data and operation in the system, is taken as input, along with the accuracy constraint. The IWLs of all data and operations (called nodes from now on) in the fixedpoint specification are pre-determined based on values range evaluation using interval arithmetic (any alternative method can be used instead). The accuracy constraint, specified by the user, represents the maximum allowed noise power of the quantization error at the system's output.

The pseudo code of the SLP-aware WLO algorithm is listed in figure 1a. We start by initializing the WL of all nodes to the maximum WL, say M , supported by the target processor for the corresponding operation (lines 1-3). This generally corresponds to the case where minimum SLP is available, but on the other hand, it represents the most accurate fixed-point specification (that can be obtained using natively supported WLs only).

Next, we process each basic block to be considered for SLP extraction, starting by the higher priority ones. Priority here depends on the contribution of the basic block to the overall execution time. This is to ensure that the accuracy-degradation budget is wisely spent on optimizing most performance impacting basic blocks first. In this work we consider that the selection and sorting of basic blocks to be considered for SLP extraction is performed earlier. It can be done based on profiling analysis for instance.

For each basic block we iteratively apply the accuracyaware SLP extraction (presented in the next subsection), which yields the set of selected SIMD groups, taking into account data packing/unpacking cost. Each time a new SIMD group is selected, the WL of all its elements is reduced to the maximum supported WL, say m, such that:

m * N elem <= SIM D size (1)
Where N elem is the number of elements in the group. This is performed by procedure SETMAXWL in algorithm 1c. For example, consider a processor supporting 2x16-bit and 4x8bit SIMD in addition to 32-bit scalar instructions. In this case M = 32. Now when a group of two operations is selected (N elem = 2) during SLP extraction, the WL of each one of them is reduced to m = 16 bits, since 16 is the maximum supported WL in this case such as 16 * 2 <= 32.

The elements of each selected group are then replaced by a new operation (representing the group) in the basic block (line 11) in order to prepare for the next SLP extraction iteration which allows the extension of the groups size when possible, otherwise the processing of the basic block is completed and we move to the next one (lines 8-10).

The global set of selected groups (G) is updated (lines 12-13) and is later used to optimize scaling operations (line 15). The scaling optimization algorithm is presented later on.

As an output we obtain a complete fixed-point specification for the system, along with the set of selected SIMD groups. These information are later used to generate fixed-point and SIMD C code.

B. Accuracy-aware SLP extraction

The pseudo code of the accuracy-aware SLP extraction algorithm is listed in figure 1c.

First we construct the set of SIMD group candidates (C) in the specified basic block and we identify the conflicts (Conf ) between them. A group candidate is a pair of isomorphic and independent operations. Two groups are in conflict if they contain the same operation or if they have a cyclic dependency. (C, Conf ) represents the solution space of SLP. This is similar to the approach presented by Liu et al. [START_REF] Liu | A Compiler Framework for Extracting Superword Level Parallelism[END_REF]. However, in our accuracy constrained context, some candidates in C may not be valid. This is the case of a candidate c that when selected (i.e. the WL of all its elements is set to m as specified by equation 1) while all other nodes are set to maximum WL (M ), the accuracy constraint is violated. In this case, c can never be implemented as SIMD instruction without violating the accuracy constraint. Therefore, we eliminate all invalid candidates in C (lines 6-12). Furthermore, Conf does not represent all the conflicts in our context. In fact, two candidates can also be in conflict if, when both selected while all other nodes are set to maximum WLs (M ), the accuracy constraint is violated. In this case both candidates cannot coexist without violating the accuracy constraint, hence they are in conflict (lines 16-21).

After the set of candidates and conflicts have been determined, the group selection process estimates the global benefit associated with the selection of each remaining candidate and then selects the most beneficial one, g. The benefit of a candidate is the ratio of superwords reuse it enables, if it get selected, to the overall packing/unpacking cost [START_REF] Liu | A Compiler Framework for Extracting Superword Level Parallelism[END_REF]. The WL of g's elements is specified as described earlier using equation [START_REF] Kum | Word-length optimization for high-level synthesis of digital signal processing systems[END_REF], and all candidates in conflict with g are eliminated (line 30-31). This iterative process continues until all conflicts have been resolved (lines 25-33).

C. Scalings Optimization

Another major impact on the performance of a fixed-point implementation is the cost of scaling operations. Their impact depends on how well the target processor supports shifting operations. For example, a barrel shifter can generally perform a shift operation of any amount in constant time. Whereas shift registers require a variable time depending on the shifting amount.

In the context of SLP an additional critical factor is the fact that scaling operations may break some superword (vector) reuse chains and hence require the introduction of packing/unpacking operations. Thus, severely impacting the performance, not only due to the scalings cost but also to the additionally introduced packing/unpacking overhead. This is, in fact, because most embedded processors only support SIMD shifting instructions by the same amount of all the vector elements. Therefore in case two elements of the same vector have to be shifted by different amounts, they need to be unpacked first, shifted independently and then repacked, before being able to be used by an SIMD instruction 1 .

In this work, we address this problem by using an SLPaware, accuracy-aware scaling optimization algorithm. The goal is to try to make all elements of an SIMD group operand (superword) scalable by the same amount, so that the scaling operations can be grouped together and implemented using an SIMD instruction without the need for packing/unpacking.

For each superword reuse, the list of scaling amounts corresponding to each one of the superword elements is determined, as a function of fractional word-lengths (FWLs) of the elements of the source and destination SIMD groups. For instance, in the example of figure 2, the output superword (s) of group the {+1, +2} is reused by the group {+3, +4}. Assuming truncation is used as quantization mode, the elements of s should be right shifted by f 1 -f 3 and f 2 -f 4, respectively. Where f x is the FWL of the corresponding operand of operation x. When the scaling amount is zero, it

+1 +2 <i1,f1> <i2,f2> +3 +4 <i3,f3> <i4,f4> f1-f3 = f2-f4 >>(f1-f3) +1 +2 +3 +4 f1-f3 ≠ f2-f4 PACK UNPACK >>(f2-f4) >>(f1-f3) +1 +2 +3 +4
Fig. 2: Example of the impact of scaling operations on packing/unpacking. On the left, an extraction of a data flow graph with 4 operations and their fixed-point formats <IWL,FWL>; dashed lines represent SIMD groups. The center part illustrates the case where scaling operations can be grouped, the other case is illustrated on the right. 1 In case masking operations are supported, packing/unpacking are not required but multiple SIMD instructions would still be needed to perform such operations. Though masking operations are rarely supported.

GeCoS

Fig. 3: SLP-aware WLO compiler flow diagram.

indicates that no scaling is required. If it is positive a right shift is required. In case f 1-f 3 = f 2-f 4, the scaling amounts are different, thus the shifting operations cannot be grouped and therefore packing/unpacking operations are required as shown in figure 2. To avoid this case, we reduce the FWLs while keeping WLs intact (by increasing the corresponding IWLs) so that the scaling amounts of all elements in a group become equal. By reducing the FWLs, the accuracy of the fixedpoint specification may degrade, therefore this optimization is performed as long as the accuracy constraint is not violated. IV. SOURCE-TO-SOURCE COMPILATION FLOW The proposed joint WLO and SLP extraction algorithm is implemented as an automated source-to-source transformation in the compiler framework, GeCoS [START_REF]GeCoS[END_REF]. The flow diagram is depicted in figure 3. Starting from an annotated floating-point C code, we first construct an intermediate representation (IR).

For analyzing the data dynamic ranges and estimating the fixed-point specification accuracy, we use IDFix [START_REF]IDFix[END_REF], a floating-to-fixed-point conversion framework integrated to GeCoS. IDFix analyzes the IR and creates the corresponding fixed-point specification, which associate a fixed-point format to each variable and operation (called nodes from now on) in the system. It then determines the dynamic ranges of all nodes, by propagating the values range intervals of the system's inputs, specified using pragma annotations. The IWL of each node is then specified by selecting the minimum IWL that covers the entire corresponding values range, in such way to avoid overflows.

Besides, the analytical expression of the system's output noise power is generated as a function of the fixed-point specification [START_REF] Menard | Automatic Evaluation of the Accuracy of Fixed-point Algorithms[END_REF]. This is used during WLO as a metric to evaluate the fixed-point specification's accuracy and compare it against the user specified constraint. Note that any alternative way for evaluating the fixed-point specification's accuracy can be used instead since our proposed WLO is completely decoupled. The proposed WLO and SLP extraction are used to obtain the fully specified fixed-point specification and the set of SIMD groups. These information are finally used by the backend to convert the floating-point code into fixed-point using integer C types and explicit cast/scalings in order to match the fixed-point specification. Furthermore, it implements the SIMD groups using an abstract C macros API and generates the API's implementation for the specified target processor using its corresponding SIMD intrinsics.

V. EXPERIMENTAL RESULTS

A. Test Setup

In order to evaluate the proposed SLP-aware WLO flow, we compared it against a compilation flow performing, first, float-to-fixed-point conversion using the same framework (ID.Fix [START_REF]IDFix[END_REF]), except for WLO. We used the Tabu search algorithm presented by Nguyen et al. [START_REF] Nguyen | Novel algorithms for word-length optimization[END_REF] with a cost relative to the operators WL similar to the approach used by Menard et al. [START_REF] Menard | Floating-to-fixed-point conversion for digital signal processors[END_REF]. For example, if the target processor provides the possibility to implement an addition using 32-bit or 16-bit word-lengths, then the corresponding cost for 32-bit is set as the double of that for 16-bit. Once the fixed-point specification is obtained, we apply SLP extraction using the same SLP extraction algorithm except that it is not accuracy aware since it is decoupled from the float-to-fixed-point conversion step. Finally, we used the same back-end to generate both fixedpoint and SIMD C codes for the target processor. The overview of this baseline flow is represented in figure 5. From now on, we will refer to it as WLO-First as opposite to our approach WLO-SLP.

Contrary to our approach, WLO-First performs WLO independently from SLP i.e. without considering the actual SLP opportunities and the associated overhead due to data packing/unpacking.

Starting from the benchmark's single-precision floatingpoint C code, we apply WLO-First and WLO-SLP. The resulting fixed-point C code of WLO-First is used as baseline to compare the performance of the SIMD version of

B. Target Processors

We considered several embedded processors for this experimental setup.

XENTIUM [START_REF] Systems | Xentium VLIW DSP IP core[END_REF] is an ultra low power 32-bit 12-issue wide Very Long Instruction Word (VLIW) core from Recore Systems. It has no support for floating-point arithmetic but provides support for 2x16-bit SIMD operations.

ST240 is a 32-bit 4-issue wide VLIW media processor from the ST200 family of ST Microelectronics. ST240 also supports 2x16-bit integer SIMD operations. Additionally, it supports single precision floating-point arithmetic. VEX [START_REF]VEX[END_REF] is a parameterizable and extensible VLIW architecture model. We use it in two configurations; VEX-1 and VEX-4 with an issue width of 1 and 4 respectively. Since VEX does not provide support for SIMD, we implemented a 16-bit and 8-bit SIMD instruction extensions for supporting integer arithmetic, shift and data manipulation operations.

C. Benchmarks

A 64-tap FIR and a 10th order IIR filters as well as a 2d (3x3) image convolution (CONV) are used as benchmarks. The C code of each benchmark is annotated to specify the values range of the inputs. The innermost loop in FIR and IIR is partially unrolled by 4 to expose SLP, whereas the convolution kernel (3x3) is fully unrolled. The input samples are pre-normalized to [-1, 1].

D. Results

The graphics of figure 4 plot the speedup of SIMD versions of WLO-First and WLO-SLP over the baseline scalar fixedpoint version (of WLO-First), for each benchmark on each target processor, against the accuracy constraint. The later represents the maximum tolerable quantization noise power at the system's output, specified in dB.

The overall results clearly show the advantage of our approach across all benchmarks on all processors.

For FIR, we can see our approach trading accuracy for performance improvement. It manages to efficiently exploit SIMD to achieve performance improvement (up to 1.5 on VEX-1), whereas WLO-First mostly result in performance degradation after applying SLP extraction, illustrating the fact that WLO is blindly optimizing without considering SLP. The few points where our approach yields performance degradation, on XENTIUM and ST240 at -65 db, are due to a reduction in the execution time of the baseline fixed-point version, where the Tabu WLO algorithm manages to find a better fixed-point solution, also at this high accuracy constraint not many SLP opportunities are available. Table I reports the number of cycles of the SIMD versions for FIR. The number of cycles for WLO-SLP increases, as expected, when the accuracy constraint becomes more strict (smaller values), whereas the number of cycles for WLO-First varies randomly. Besides, we can notice the impact of instruction level parallelism (ILP) by comparing the results on VEX-4 against VEX-1: on VEX-4, with higher ILP capabilities, the performance improvement is less important than on VEX-1.

For IIR, our approach also yields consistently better performance improvement, up to 2x on XENTIUM and 1.3x on ST240. WLO-First still mostly result in performance degradation after applying SLP extraction.

The same is true for CONV except on XENTIUM between -25 dB and -40 dB where our approach results in slight performance degradation. In this case, the selected SLP solution has a high packing/unpacking cost compared to the performance gain it achieves. However, a performance estimation of the obtained SLP grouping solution, as suggested in [START_REF] Liu | A Compiler Framework for Extracting Superword Level Parallelism[END_REF], can be used to discard the solution in case a performance degradation is detected. In this setup, we intentionally skipped this step in order to emphasize the fact that selecting smaller WLs, which does effectively increase SLP opportunities, does not however always translate to performance improvement.

The graphics of figure 6 plot the speedup of WLO-SLP over the original floating-point code for both XENTIUM and ST240. On XENTIUM, a speedup of 15x to 45x is recorded. This is expected since this processor does not have a hardware support for floating-point arithmetic which needs to be softemulated. On ST240, even though it has hardware support for floating-point, a speedup up to 1.4x is obtained. It is mainly due to the exploitation of SIMD capabilities.

VI. CONCLUSION

In this paper we presented a new SLP-aware WLO algorithm targeting embedded processors with SIMD capabilities. We implemented our approach in an automated source-tosource compilation framework. Experimental results show the advantage of our approach for efficient exploration of the performance/accuracy tradeoff.

while not done do 7 :

 7 Input: BBs: sorted list (by priority) of basic blocks for SLP extraction.SP EC: fixed-point specification with IWLs pre-determined. A: accuracy constraint Output: G, set of selected SIMD groups. Determine WLs in spec. 1: for node in SP EC do 2: Set node to maximum WL supported by the target processor 3: end for 4: for b in BBs do visit in priority order 5: Selected ← SLP(b, spec, A) Update b and prepare it for next iteration 12: G ← G \ {e1, e2 : {e1, e2} ∈ Selected} 13: G ← G ∪ Selected 14: end while 15: SCALOPTIM(G, SP EC, A) 16: end for (a) SLP-aware WLO algorithm

C

  17: end procedure (b) SLP-aware Scalings optimization 1: EVALACC(SP EC): evaluates the accuracy of the current fixed-point specification 2: SETMAXWL(c, SP EC): set all elements of c to maximum possible WL as defined by equation 1 3: procedure SLP(b, SP EC, A) ← extract SIMD group candidates from b 6: for c in C do 7: SETMAXWL(c, SP EC)

Fig. 1 :

 1 Fig. 1: SLP-aware WLO pseudo code.

Fig. 4 :

 4 Fig. 4: Speedup comparison between SIMD version of WLO-First and WLO-SLP vs. accuracy constraint expressed in dB.

Fig. 5 :

 5 Fig. 5: WLO-First compiler flow diagram WLO-First (which perform float-to-fixed-point conversion first then SLP extraction independently) against the one obtained by applying our joint float-to-fixed-point conversion and SLP extraction flow.The generated C codes are then compiled (with -O3) and simulated on the target processor simulators. The number of cycles spent executing the benchmark is retrieved and used to compute the speedup of the SIMD versions for both WLO-First and WLO-SLP, over the baseline fixed-point version (of WLO-First).speedup = number of cycles f ixedpoint version number of cycles SIM D version(2)

Fig. 6 :

 6 Fig. 6: Speedup of WLO-SLP over the original (singleprecision) floating-point version vs. accuracy constraint.

TABLE I :

 I Number of cycles of SIMD versions for FIR.