: A Language for Describing Optimization Strategies]A Language for Describing Optimization Strategies

Bastian Hagedorn

University of Münster, Germany

Johannes Lenfers

University of Münster, Germany

Thomas Koehler

University of Glasgow, UK

Sergei Gorlatch

University of Münster, Germany

Michel Steuwer

University of Glasgow, UK

Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications.
The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations.
This results in a nightmare for portability which is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.

Many emerging DSLs used in performance demanding domains such as deep learning, automatic differentiation, or image processing attempt to simplify or even fully automate the optimization process.
Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way.
In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized.
Unfortunately, these schedules are not written in well-defined programming languages.
Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.

In this paper, we present : a functional language for describing optimization strategies.
follows a tradition of prior systems used in different contexts that express optimization strategies as composition of rewrites.
In contrast to systems with scheduling APIs, in programmers are not restricted to a set of built-in optimizations but define their own optimization strategies freely in a composable way.
We show how user-defined optimization strategies in enable the effective optimization of programs expressed in a functional data-parallel language demonstrating competitive performance with Halide and TVM.

§ INTRODUCTION

The tremendous gains in performance and efficiency that computer hardware continues to make are a key driving force for innovation in computing.
This enables entire new areas of computing such as deep learning to deliver applications unthinkable even just a few years ago.
With the end of Moore's law and Denard's scaling <cit.>, these gains no longer come for free for software writers.
Programs have to be optimized for an increasing diverse set of hardware devices by exploiting many subtle details of the computer architecture.
Performance portability has emerged as a crucial concern as software naturally outlives the faster cycle of hardware generations.
In addition, specialized hardware has proven to offer extreme benefits for performance and energy efficiency - if the specially optimized software exploits it.

The predominant imperative and low-level programming approaches such as C, CUDA, or OpenCL force programmers to intertwine the code describing the functional behavior of the program with optimization decisions.
This makes them – by design – non performance portable.
As an alternative, higher level domain-specific approaches have emerged that allow programmers to declaratively describe the functional behavior without committing to a specific implementation.
Popular examples of this approach are virtually all machine learning systems such as TensorFlow <cit.> or PyTorch <cit.>.
For these approaches, the compilers and runtime systems are responsible to optimize the computations that are expressed as data-flow graphs.
Programmers have limited control about the optimization process.
Instead large teams of engineers at Google and Facebook provide fast implementations for the most common hardware platforms, for TensorFlow including Google's specialized TPU hardware.
This labour intensive support of new hardware devices is currently only sustainable for the biggest companies in the market – and even they struggle <cit.>.
To overcome this innovation obstacle and to achieve automated performance portability we will need to rethink how we separate, describe, and apply optimizations in a more principled way.

Encoding program transformations as rewrite rules has been a long established idea.
<cit.> studied an algebraic programming approach where functional programs are rewritten by exploiting algebraic properties.
The Glasgow Haskell Compiler allows the specification of rewrite rules for program optimizations <cit.>.

More recently,  <cit.> encodes optimization and implementation choices as rewrite rules for optimizing a high-level pattern-based data-parallel functional language using an automated stochastic search method applying the rewrites.
Rewrite based approaches, such as , have the advantage of being easily extensible towards new application domains (such as stencils <cit.>) as well as supporting new hardware features (such as specialized vector instructions which are encoded as new low-level patterns and introduced by a rewrite rule <cit.>).
Unfortunately, these rewrite approaches are limited in their practicality to deliver the high performance required in many real-world applications.
They lack control over the rewriting process and the automated rewriting using stochastic search processes takes a long time to find a high performance implementation.
In this paper, we are going to address these practical limitations of rewrite-based approaches for optimizing high-performance real-world applications by defining a strategy language that allows the definition of optimization strategies that precisely controls the rewrite process.

Halide <cit.> has introduced the concept of separating programs into functional descriptions and schedules in the area of high-performance domain-specific code generators.
A schedule describes the optimizations to be applied to the Halide algorithm that defines the functional behavior of the computation.
Halide's schedules – as well similar schedules in TVM <cit.> – are implemented using a set of predefined APIs that expose a fixed set of optimization options.
Halide's authors describe these APIs as a scheduling language but it lacks many desirable properties of a programming language.

Most crucially, programmers are not able to define their own abstractions.
Even the composition of existing optimization primitives is in some cases unintuitive due to the lack of a clear semantics and Halide's compiler has default and implicit behavior limiting experts' control.

All of these reasons make writing schedules in Halide significantly harder than writing algorithms.
Furthermore, for some desirable optimizations it is not sufficient to change the schedule but the algorithm itself has to be redefined – violating the promise of separating algorithm and schedule.

In this paper, we build upon Halide's general idea but provide a proper functional strategy language, called , with clear semantics of individual primitives and how they compose.
It enables programmers to define their own abstractions for building optimization strategies in a composable and reusable way.

The design of  is heavily inspired by research on strategy languages for rewrite systems used in other contexts – and largely unknown to the high-performance code generation community – such as Stratego <cit.>.
<cit.> provides a recent overview of the research of the rewriting community.
We claim no novelty in the design foundations of strategy languages but instead in the strategies we present and their usage to facilitate the generation of highly efficient code on modern hardware.

Our paper makes the following key contributions:

* Description of the design of , a functional language for describing optimization strategies for high-performance code generation (<Ref>);

* demonstration of  using three case studies: automatic differentiation (<ref>), image processing (<ref>) and deep learning (<ref>).
They show the flexibility and extensibility of  and experimentally evaluate the practicality of a rewrite based approach for achieving competitive high performance.

§ MOTIVATION AND BACKGROUND

We motivate the need for a strategy language with a closer look at Halide.

We then argue for a more principled language approach for describing optimizations strategies.

§.§ Halide: Decoupling Algorithm from Schedules

Halide <cit.> has originally been designed to generate high performance code for image processing pipelines <cit.>, but has since inspired similar approaches in other contexts such as TVM in deep leaning <cit.>.
A crucial idea is the separation of a program in two parts:
the algorithm describing the functional behavior, and
the schedule specifying how the program should be optimized by the underlying Halide compiler.

Matrix matrix multiplcation in Halide. Lines <ref>–<ref> define the computation $A \times B$, the other lines define the schedule specifying the optimizations to be applied by the compiler.
From:  <https://github.com/halide/Halide/blob/master/apps/cuda_mat_mul/mat_mul_generator.cpp>.
// functional description of matrix multiplication
Var x("x"), y("y"); Func prod("prod"); RDom r(0, size);$\label{lst:halide-mm:computation:begin}$
prod(x, y) += A(x, r) * B(r, y);$\label{lst:halide-mm:computation}$
out(x, y)  = prod(x, y);$\label{lst:halide-mm:computation:end}$

// schedule for Nvidida GPUs
const int warp_size = 32; const int vec_size = 2;
const int x_tile    =  3; const int y_tile   = 4;
const int y_unroll  =  8; const int r_unroll = 1;
Var xi,yi,xio,xii,yii,xo,yo,x_pair,xiio,ty; RVar rxo,rxi;
out.bound(x, 0, size).bound(y, 0, size)
.tile(x, y, xi, yi, x_tile * vec_size * warp_size,
y_tile * y_unroll)
.split(yi, ty, yi, y_unroll)
.vectorize(xi, vec_size)
.split(xi, xio, xii, warp_size)
.reorder(xio, yi, xii, ty, x, y)
.gpu_blocks(x, y).gpu_threads(ty).gpu_lanes(xii);
prod.store_in(MemoryType::Register).compute_at(out, x)
.split(x, xo, xi, warp_size * vec_size, RoundUp)$\label{lst:halide-mm:repeat1:start}$
.split(y, ty, y, y_unroll)
.gpu_threads(ty).unroll(xi, vec_size).gpu_lanes(xi)$\label{lst:halide-mm:repeat1:end}$
.split(x, xo, xi, warp_size * vec_size, RoundUp)$\label{lst:halide-mm:repeat2:start}$
.split(y, ty, y, y_unroll)
.gpu_threads(ty).unroll(xi, vec_size).gpu_lanes(xi)$\label{lst:halide-mm:repeat2:end}$
.split(r.x, rxo, rxi, warp_size)
.unroll(rxi, r_unroll).reorder(xi, xo, y, rxi, ty, rxo)
Var Bx = B.in().args()[0], By = B.in().args()[1];
Var Ax = A.in().args()[0], Ay = A.in().args()[1];
B.in().compute_at(prod, ty).split(Bx, xo, xi, warp_size)
A.in().compute_at(prod, rxo).vectorize(Ax, vec_size)
A.in().in().compute_at(prod, rxi).vectorize(Ax, vec_size)
.split(Ax, xo, xi, warp_size).gpu_lanes(xi)

<Ref> shows a snippet of Halide code used for generating an efficient matrix-matrix multiplication for an Nvidia GPU.
Halide is a DSL embedded in C++, so the syntax used here is C++.
The lines <ref>–<ref> define the matrix-matrix multiplication computation:
$A$ and $B$ are multiplied by performing the dot product for each coordinate pair $(x,y)$.
The dot product is expressed as pairwise multiplications and reducing over the reduction domain $r$ using the  operator (line <ref>).

The other lines in the listing define the schedule specifying the optimizations to be performed.
The Halide compiler takes this C++ program and produces efficient GPU code coming close to highly optimized low-level library code.

By looking at the code it is immediately clear that writing a schedule is significantly more challenging than writing the algorithm describing matrix-matrix multiplication.
Schedules are written using a sequence of API calls on the C++ objects that represent the input (, ) and output () data.
represents the reduction operation in Halide's internal representation.
While the algorithm and schedule are separated they still share the same C++ identifiers and must, therefore, be written in the same C++ scope limiting the reuse of schedules across algorithms.

This schedule uses 12 built-in optimization primitives (, , , , , , , , , , , ).
Some of these optimizations are specific for the hardware (like  or ), others are generally useful algorithmic optimizations for many applications (like  to increase data locality), and others are low-level optimizations (like  and  that transform loop nests).
Halide is not easily extensible.
Adding a new optimization primitive to the schedule API requires extending the Halide compiler.
Even a primitive like  that can be implemented with  and [See: <https://halide-lang.org/tutorials/tutorial_lesson_05_scheduling_1.html>] is represented as a composition but provided as a built-in abstraction.
Halide's schedules lack the ability for user-defined abstractions.

The behavior of some primitives is not intuitive and the documentation provides only informal descriptions, e.g., for : “Get a handle on an update step for the purposes of scheduling it”.
The lack of clear descriptions of the optimization primitives makes reasoning about the schedule difficult.
For example, is it unclear to us why lines <ref>–<ref> are repeated at lines <ref>–<ref> with calls to  and  in between.

Var x, y; Func out; Func in = BC::repeat_edge(input);
out(x, y) = (
1.f * in(x-1,y-1) + 2.f * in(x,y-1) + 1.f * in(x+1,y-1) +
2.f * in(x-1,y)   + 4.f * in(x,y)   + 2.f * in(x+1,y)   +
1.f * in(x-1,y+1) + 2.f * in(x,y+1) + 1.f * in(x+1,y+1)
) * (1.f/16.f);

Var x,y; Func b_x,b_y,out; Func in=BC::repeat_edge(input);
b_y(x, y) =  in(x, y-1) + 2.f * in(x, y)  +  in(x, y+1);
b_x(x, y) = b_y(x-1, y) + 2.f * b_y(x, y) + b_y(x+1, y);
out(x, y) = b_x(x, y) * (1.f/16.f);

Two-dimensional binomial filter in Halide (top) and separated version (bottom).

<Ref> shows the implementation of a two-dimensional binomial filter in Halide.
The listing on top shows the basic Halide algorithm implementation by computing every output pixel as a weighted sum of the $3\times{}3$ surrounding pixels.
A more efficient way is shown below where the computation is separated into a vertical and horizontal filter operating on $3$ pixels each.
Separability is a well known domain-specific optimization in image processing and only valid for appropriate weights.
Halide does not offer this optimization as a scheduling primitive and, therefore, programmers are forced to change the algorithm for this optimization – clearly violating the promise of separating algorithm and schedule.

If no schedules are provided (as in <ref>), the Halide compiler employs a set of implicit default optimizations that are out of reach of the control of the user.
This sometimes leads to the surprising behavior that algorithms without a schedule perform better (e.g., due to auto-vectorization) than ones where a schedule is provided.

§.§ Towards an Optimization Strategy Language

Out of the shortcoming of the API approach we identify the following desirable features for a strategy language:

* Optimization strategies should be defined clearly separated from the computational program facilitating reusablility of strategies across programs;

* Strategies should be written as compositions of user-defined strategies (possibly domain-specific ones); the language should facilitate the creation of higher-level abstractions;

* All strategies should have a clear semantics allowing reasoning about their application and implicit default behavior should be avoided to empower users to be in control.

Essentially we argue that a strategy language should be build with the same standards as a language describing computation.
In this paper we present such a language: .

val bf = fun(3.3.float)(weights2d => fun(N.M.float)(img =>
img |> pad2D(1) |> slide2D(3)(1) |> map2D(fun(nbh =>
dot(join(weights2d))(join(nbh)) ))))

val sbf = (topDown(separateDot) `;` lowerToC)(bf)

2D binomial filter in a -like language (top) and the separating optimization strategy in (bottom).

<Ref> shows an example of an  strategy (bottom) that optimizes a program (top) written in a completely separate pattern-based language similar to  <cit.> called .
The optimization strategy is a sequential composition (`;`) of user defined strategies providing a higher level of abstraction.
Strategies are build as compositions of rewrite rules with a clear semantics and no implicit behavior.

In the remainder of the paper, we will explain the language for writing such strategies and defining custom abstractions.

§ : A LANGUAGE FOR DESCRIBING OPTIMIZATION STRATEGIES

In this section, we describe our language for describing optimization strategies: .
It is heavily inspired by earlier works on strategy languages for term rewriting systems, particularly Stratego <cit.>.

Our key contribution is not the design of itself but rather its application to define optimization for high-performance code generators.
In this section, we focus on introducing as a practical programming language.
For a more formal treatment of strategy languages see <cit.>.

§.§ Language Features and Types

is a functional language with a standard feature set including function recursion, algebraic data types and pattern matching.
Besides the standard scalar data types such as int, types of interests are function types, tuple types and list types.

Our current implementation is an embedded DSL in Scala and we use Scala-like notation in the paper.

§.§ Strategies

A strategy is the fundamental building block of .
Strategies encode program transformations and are modeled as functions with the following type:
type Strategy[P] = P => RewriteResult[P]

Here P is the type of the program that is rewritten.
P could for example be Rise for programs written in the language from <ref>.
A RewriteResult[P] is an algebraic datatype encoding the success or failure of applying a strategy to a program:
RewriteResult[P] = Success[P](p: P)
| Failure[P](s: Strategy[P])

In case of a successful application, Success contains the transformed program, in case of a failure, Failure contains the strategy that has been unsuccessful.

The simplest example of a strategy is the id strategy which always succeeds and returns its input program:
def id[P]: Strategy[P] = (p: P) => Success(p)

The fail strategy does the opposite and always fails while recording that the fail strategy was the one failing:
def fail[P]: Strategy[P] = (p: P) => Failure(fail)

§.§ Rewrite Rules as Strategies

In , rewrite rules are also strategies, i.e., functions satisfying the same type given above.
Let's look at a concrete type of programs, such as which is a pattern-based functional programming language where we want to apply well-known rewrite rules such as the fusion of two map calls: $(map~f) \circ (map~g) \mapsto map~(f\circ g)$.
In , the left-hand side of the rule is expressed as:
val p: Rise = fun(xs => map(f)(map(g)(xs)))

The AST representation of the body of this is shown in <ref> on the left, with function applications explicit as app nodes.

's map-fusion rule as an AST transformation.

This is the implementation of the fusion rule in :
def mapFusion: Strategy[Rise] = p => p match
case app(app(map, f), app(app(map, g), xs)) =>
Success( map(fun(x => f(g(x))))(xs) )
case _ => Failure(mapFusion)

Note that we are mixing expressions of the language (i.e., map(f)) and .
The expression nested inside Success is the rewritten expression shown in <ref> on the right.

§.§ Strategy Combinators

A key idea that inherits from Stratego <cit.> is to describe strategies as compositions of other strategies.
Therefore, we introduce strategy combinators.

The seq combinator is given two strategies fs and ss and applies the first strategy to the input program p.
Afterwards, the second strategy is applied to the result.
[style=elevate-rise-short, basicstyle=]
def seq[P]: Strategy[P] => Strategy[P] => Strategy[P] =
fs => ss => p => fs(p).flatMapSuccess(ss)

The seq strategy is only successful when both strategies are successfully applied in succession, otherwise seq fails.

In the implementation of seq, we make use of the monadic interface of strategies:
the RewriteResult ADT provides two versions of [basicstyle=]map/flatMap to compose strategies – one in case of a successful strategy application and one in case of failure.

The lChoice combinator is given two strategies and applies the second strategy only if the first strategy failed.
[style=elevate-rise-short, basicstyle=]
def lChoice[P]: Strategy[P] => Strategy[P] => Strategy[P] =
fs => ss => p => fs(p).flatMapFailure(_ => ss(p))

We use <+ as notation for lChoice and `;` for seq and define two more combinators:

The try combinator applies a strategy and in case of failure applies the identity strategy.
Therefore, try never fails.
[style=elevate-rise-short, basicstyle=]
def try[P]: Strategy[P] => Strategy[P] =
s => p => (s <+ id)(p)

repeat applies a strategy until it is no longer applicable.
[style=elevate-rise-short, basicstyle=]
def repeat[P]: Strategy[P] => Strategy[P] =
s => p => try(s `;` repeat(s) )(p)

§.§ Traversal Strategies

Two possible locations for applying the map-fusion rule within the same program.

The mapFusion strategy we saw in the previous subsection is implemented as a function in .
Therefore, its match statement will try to pattern match its argument – the entire program.
This means that a strategy on its own is very hard to reuse in different circumstances.

In addition, a strategy is often applicable at multiple places within the same program or only applicable at a specific location.
For example, the mapFusion strategy is applicable twice in the following program:

val threemaps = fun(xs => map(f)(map(g)(map(h)(xs))))

We may fuse the first or last two maps as shown in <ref>.

In , we use traversal strategies to describe at which exact location a strategy is applied.

<cit.> proposed three basic traversal strategies:
def  all[P]: Strategy[P] => Strategy[P]
def  one[P]: Strategy[P] => Strategy[P]
def some[P]: Strategy[P] => Strategy[P]

all applies a given strategy to all sub-expressions of the current expression and fails if the strategy is not applicable to all sub-expressions.
one applies a given strategy to exactly one sub-expression and fails it the strategy is not applicable to any sub-expression.
some applies a given strategy to at least one sub-expression but potentially more if possible.
one and some are allowed to non-deterministically choose sub-expressions.

In , we see these three basic traversal strategies as a type class:
an interface that has to be implemented for each program type P.
The implementation for is straightforward.
programs are represented by ASTs such as the one in <ref>, therefore, all, one, and some correspond to the obvious implementations on the tree-based representation.

To fuse the first two maps in <ref> we use the one traversal strategy: one(mapFusion)(threemaps).
This will apply the mapFusion strategy not at the root of the AST, but instead one level down first trying to apply the strategy (unsuccsessfully) to the function parameter and then (successfully) to the function body highlighted in the upper-right blue box.

To fuse the last two maps we use the one traversal strategy twice to apply mapFusion two levels down in the AST: one(one(mapFusion))(threemaps).

This sucessfully applies the fusion strategy to the expression highlighed in the lower-left purple box in <ref>.

§.§ Language-Specific Traversal Strategies

The traversals we have discussed so far are not specific to a particular language, such as .
These traversals are flexible, but offer only limited control as for one and some the selection of sub-expressions is either non-deterministic, or implementation-dependent (as for ) and in our context it makes rarely sense to apply a strategy to all sub-expressions.

In , one can easily specify program language specific traversal primitives.
is a functional language using $\lambda$-calculus as its representation.
Therefore, it makes sense to introduce traversals that navigate the two core concepts of $\lambda$-calculus: [style=elevate-rise-short, basicstyle=]function abstraction and [style=elevate-rise-short, basicstyle=]application.

To apply a strategy to the body of a function abstraction we define the following traversal strategy:
def body(s: Strategy[Rise]): Strategy[Rise] =
p => p match
case fun(x,b) => s(b).mapSuccess(nb => fun(x,nb))
case _ => Failure(s)

A strategy s is applied to the function body and if successful a function is build around the transformed body.

Similarly we define traversals function and argument to traverse function applications:
def function(s: Strategy[Rise]): Strategy[Rise] =
p => p match
case app(f,a) => s(f).mapSuccess(nf => app(nf, a))
case _ => Failure(s)

def argument(s: Strategy[Rise]): Strategy[Rise] =
p => p match
case app(f,a) => s(a).mapSuccess(na => app(f, na))
case _ => Failure(s)

For the program shown in <ref>, we are now able to precisely describe a traversal path in the AST.
To fuse the first two maps we may write body(mapFusion)(threemaps), and to fuse the others body(argument(mapFusion))(threemaps).

The traversals defined here are specific to but similar traversals are obviously possible for any functional language.
If the program is not a functional language, say e.g., a computational graph as used by Tensorflow, different language-specific traversals (e.g., leftOperand and rightOperand) could be defined to describe language-specific traversals.

§.§ Complete Expression Traversal Strategies

All of the traversal primitives introduced so far apply their given strategies only to immediate sub-expressions.

Using strategy combinators and traversals, we are able to define recursive strategies which traverse entire expressions:
def topDown[P](s: Strategy[P]): Strategy[P] =
p => (s <+ one(topDown(s)))(p)
def bottomUp[P](s: Strategy[P]): Strategy[P] =
p => (one(bottomUp(s)) <+ s)(p)
def allTopDown[P](s: Strategy[P]): Strategy[P] =
p => (s `;` all(allTopDown(s)))(p)
def allBottomUp[P](s: Strategy[P]): Strategy[P] =
p => (all(allBottomUp(s)) `;` s)(p)
def tryAll[P](s: Strategy[P]): Strategy[P] =
p => (all(tryAll(try(s))) `;` try(s))(p)

topDown and bottomUp are useful strategies traversing an expression either from the top or from the bottom, trying to apply a given strategy at every sub-expression and stopping at the first successful application.
If the strategy is not applicable at any sub-expression, topDown and bottomUp fail.

allTopDown and allBottomUp do not use lChoice insisting on applying the given strategy to every sub-expression.

The tryAll strategy is often more useful as it wraps its given strategy in a try and thus never fails but applies the strategy wherever possible.
Also note that the tryAll strategy traverses the AST bottom-up instead of top-down.

These traversals have also been proposed by <cit.> and we use them here with slightly different names more fitting for our use cases.

§.§ Normalization, Confluence and Termination

When implementing rewrite rules, such as the mapFusion rule, as strategies, the match statement expects the program expression to be in a particular syntactic form.
For a functional language like , we might for example expect that expressions are fully $\beta$-reduced.
To ensure that expressions satisfy a normal form we define:
def normalize[P](s: Strategy[P]): Strategy[P] =
p => repeat(topDown(s))(p)

The normalize strategy applies a given strategy repeatedly at every possible sub-expression until it can not be applied any more.
Therefore, after normalize successfully finishes it is not possible to apply the given strategy to any sub-expression any more.
By defining a strategy for $\beta$-reduction and using it together with normalize we ensure that expressions are in $\beta$-normal-form.

Confluence (multiple non-deterministic rewrite paths eventually produce the same result) and termination are desirable properties for normal forms in term rewriting systems <cit.>.

In , confluence only becomes a factor when the implementation of one and some are non-deterministic.
This can often be avoided such as for the use cases we consider with and that we will discuss in <ref>.

Termination of normal forms critically depends on the chosen set of strategies.
Therefore, reasoning about terminating normal forms must be done on a case by case basis.
For example, it is trivial to build a non-terminating normal form using the id strategy that is always applicable.
We currently, do not prevent the creation of non-terminating strategies similar as almost all general purpose computational languages do not prevent writing non-terminating programs.
In the future, we are interested to introduce a richer type system for to better assist the user in writing well behaved strategies.

§.§ Summary

We have introduced , a language for describing optimization strategies.
In the next three sections we discuss three case studies of using in the domains of automatic differentiation, image processing, and deep learning.

§ CASE STUDY 1: AUTOMATIC DIFFERENTIATION

So far we have seen as the only example of a language that we transform with , but is flexible and not restricted to a single language.
In this first case study, we will look at the language that has been introduced in <cit.>.

is a small functional language capable of automatically computing the derivative of arbitrary functions.
Implementing automatic differentiation is not too difficult but making it efficient is non-trivial.
achieves efficiency by rewriting the differentiated code.
In the paper, rewrite rules are specified alongside examples.
Example 5 in the paper shows that a program transposing a matrix twice can be rewritten into a program without transposition, see <ref>.

let MT = build (length M[0]) (fun i ->
build (length M) (fun j -> M[j][i] ) ) in
build (length MT[0])(fun i ->
build (length MT) (fun j -> MT[j][i] ) )

build (length M) (fun i ->
build (length M[0]) (fun j -> M[i][j] ) )

Transposing a matrix twice in (top) and the rewritten program without transposition (bottom). From <cit.>

The paper does not provide an explanation how the rewriting between these programs happens or is specified.
The authors only state “by applying the loop fusion rules and performing further partial evaluation the expression is derived”.

We are interested in exploring the flexibility of and if we can specify the rewrite rule applications programmatically.
We implemented the language representing expressions using an algebraic data type FSmooth.
We implemented the rewrite rules from the paper, such as fusion rules:
(build e$_0$ e$_1$)[e$_2$] $\qquad\leadsto\quad$ e$_1$ e$_2$
length (build e$_0$ e$_1$) $\,\leadsto\quad$ e$_0$

These fusion rules are implemented as strategies:
[style=elevate-rise-short, basicstyle=]
def buildGet(p: FSmooth): Strategy[FSmooth] = p match
case app(get,(app(build,(e0,e1)),e2)) => Success(app(e1,e2))
case _ =>                                Failure(buildGet)  @
def lenBuild(p: FSmooth): Strategy[FSmooth] = p match
case app(length, app(build, (e0, e1))) => Success(e0)
case _                                 => Failure(lenBuild)

Using these rewrite rules encoded as strategies, we use normalize and lChoice to specify multiple strategies that should be applied repeatedly at every sub-expression:
normalize(buildGet <+ lenBuild <+ letPartialEval <+
letApp <+ funToLet)(mt)

This program successfully rewrites the doubly-transposed program into the non-transposed form.
By tracing the execution of the program we get a sequence of 12 basic rewrite rule applications explaining the program transformation step-by-step.
A full version of the trace is shown in the supplementary material.

We also implemented the other examples in the paper which contain rewriting in – and identifying a minor bug in the description of example 6.

This case study shows 's flexibility to implement an existing rewrite system.
It also demonstrates 's ease of use:
we did not have to think about where to apply the individual rewrite rules thanks to the abstraction provided by normalize.
It is important to stress, that this is not a built-in abstraction but defined itself in terms of the smaller building blocks repeat and topDown.
In the next case-study, we discuss how the ability to leverage these abstractions and build custom ones enables the definition of optimization strategies for image processing.

§ CASE STUDY 2: IMAGE PROCESSING

In this case study, we are interested to see how our extensible strategy language compares directly to Halide.
We will look at the binomial filter example which we already briefly showed in <ref> and <ref>.
We will use as our computational language.
is a  <cit.>-like language that is compiled by rewriting high-level pattern-based programs into a low-level representation encoding implementation and optimization choices.
It then uses a compilation process similar to <cit.> to compile the low-level pattern-based code into parallel imperative code.

§.§ Halide Schedules for the Binomial Filter

For Halide, we saw two algorithms describing the computation of the binominal filter in <ref>.
The naive version on the top is a straightforward implementation as a two-dimensional stencil.
The separated version on the bottom specifies the computation as a composition of vertical and horizontal one-dimensional stencils.
In Halide, it is not possible to take the naive algorithm and use a schedule to specify the separability optimization.
When we do not specify a schedule in Halide, a default schedule is chosen that inlines computations as much as possible.
Therefore, the naive and the separated version with the default schedule result in code executing two nested loops and accessing 9 elements of the input image.
We can instruct Halide not to fully inline the vertical filter by writing: b_y.compute_at(out, y);
This schedule uses the variable names from the Halide algorithm implementing the separated version of binomial filter.
The compute_at schedule instruction tells the compiler to perform the computation of the vertical filter (b_y) inside the for loop iterating over the y dimension of the out image.
This computation will be stored in a temporary that is consumed in the nested loop iterating over the x dimension of out.
We call this version scanline as the temporary stores an entire line of the image.

For all versions, it is possible to parallelize the outermost loop with: out.parallel(y);

§.§ Strategies Optimizing Binomial Filter

To compare with Halide, we express the binomial filter with as shown at the top of <ref>.
This formulation is the naive way to describe a two-dimensional filter in .
The filter is expressed using two-dimensional variations of the pad, slide, and map high-level patterns in the style of <cit.>.
pad models the boundary handling, the sliding window pattern slide describes a neighborhood of values each of which is then processed by the map pattern.
The 2D versions of these pattens are just macros defined as compositions of the one-dimensional versions and a few additional basic patterns.
The dot product computation is also defined as a composition:
dot(x)(y) = reduce(add)(0)(map(mult)(zip(x)(y)))

To express the separability as an strategy we introduce an image-processing specific rewrite rule that describes how the dot product of the weights and the neighborhood inside the binomial filter is separated:
def separateDot(w2d:Rise, wh:Rise, wv:Rise): Strategy[Rise] =
p => p match
case app(app(app(reduce, @add@), @0@), app(app(map, @mult@),
app(app(zip, app(join, w)), app(join, nbh)))) if w==w2d =>
Success(nbh |> map(dot(wh)) |> dot(wv))
case _ => Failure(sepDot)

The underlined values in the pattern matching indicate that these must match for the pattern matching to succeed.

The strategy takes three parameters that are all expressions in the computational language .
w2d represents the two-dimensional weights and wh and wv are the separated horizontal and vertical weights.
does not automatically attempt to separate the weights nor does it attempt to prove that the horizontal and vertical weights are a valid separation of the two-dimensional weights.
These considerations are left to the user.
We aim to empower users to extend which such domain-specific strategies.

To rewrite the naive binominal filter into the separated one, we apply separateDot with topDown as shown earlier as an strategy at the bottom of <ref> resulting in:

img |> pad2D(1) |> slide2D(3)(1) |> map2D(fun(nbh =>
nbh |> map(dot(weightsH)) |> map(dot(weightsV)) ))

We express the lowering of high-level expressions with strategies that encode low-level implementation choices such as whether we would like to parallelize or not.
In Halide, the built-in compute_at primitive is used for the scanline version.
In a user-defined strategy encodes the same transformation.

We will investigate more complex optimization and low-level implementation strategies in more detail in the third case study in <ref>.

§.§ Performance Evaluation

Even though this paper discusses and not we want to evaluate whether a rewrite-based approach by combining them is capable of achieving competitive performance compared to the industry-strength Halide compiler that uses more traditional compiler techniques.
We have seen that allows the definition of optimization strategies in an extensible way and that this allows to express optimizations as strategies that are not expressible as Halide schedules (such as separability).
We are now interested to see if these strategies encoding the same optimization decisions lead to competitive performance when compiled with and compared to Halide.

ytick=0, 30, 60, 90, 120,
ylabel=Runtime in ms,
bar width=7pt,

symbolic x coords=

enlarge y limits=0.15,upper,
legend style=at=(0.8,0.9),anchor=north,legend columns=1,font=,
y label style=font=,
y tick label style=font=,
x tick label style=rotate=0, font=, align=center,
cycle list/Paired,
every axis plot/.append style=fill,draw=black,no markers
[fill = Paired-G]
(,          101.463)
(,       24.9694)
(,     90.9039)
(,  21.9345)
(,      87.1208)
(,   23.9888)

[fill = Paired-F]
(,          113.4875)
(,       27.1324)
(,     103.9173)
(,  25.872)
(,      97.1703)
(,   23.7972)

Halide, Elevate+Rise

Performance evaluation of Halide and generated code for the binomial filter application. Optimization decisions for are implemented as strategies.

<Ref> shows the performance of the Halide and generated code measured on a ARM Cortex A7 quad-core[The 4 LITTLE cores of a Samsung Exynos 5 Octa 5422].
We can see – not surprisingly – that the non-parallel versions on the left are significantly slower than the parallel versions.
The Halide generated code is 10-15% faster than the generated code.
Improvements to the compiler might close this gap in the future.
Crucially, we observe the same trend for performance improvements due to optimizations.
This demonstrates that our extensible and rewrite based approach is capable of achieving competitive performance.

§ CASE STUDY 3: DEEP LEARNING

In our first two case studies, we looked at fairly simple strategies.
In our final case study, we are interested to explore the practicability and scalability of .
We are looking at the domain of deep learning where performance optimizations are particularly important.
In this section, we explore the implementation of a scheduling language with using the ability to define custom abstractions.
We use TVM <cit.> as an example for a state-of-the-art optimizing deep learning compiler with a scheduling API implemented in Python, similar to Halide.
We use again as the target language for the strategies we develop.

We start by looking at how TVM represents schedules and how we implement simple scheduling primitives such as parallel and vectorize in .
Then we show how to implement more complex scheduling primitives like tile using composition in whereas it is built-in in TVM.
We follow a tutorial from the TVM authors[<https://docs.tvm.ai/tutorials/optimize/opt_gemm.html>] that discusses seven differently optimized versions of matrix multiplication.
For each one, we show an equivalent strategy implemented with and evaluate the performance achieved.

§.§ TVM Schedules for Matrix Multiply

In TVM, computations are expressed similar to TensorFlow:
C = tvm.compute((M, N), lambda x, y:
tvm.sum(A[x,k] * B[k,y], axis=k), name='C')

The “How to optimize GEMM on CPU”[3] tutorial discusses seven versions applying different optimizations.
The baseline version uses a default schedule with no instructions.
The blocking version tiles the two outermost loops computing matrix $C$ and then splits the reduction loop before reordering the loop nest:

# blocking version
xo, yo, xi, yi = s[C].tile(C.op.axis[0],C.op.axis[1],32,32)
k,             = s[C].op.reduce_axis
ko, ki         = s[C].split(k, factor=4)
s[C].reorder(xo, yo, ko, ki, xi, yi)

The vectorized version vectorizes the innermost loop and, in addition, the loop permutation version changes to a cache friendly access of matrix $A$ by reordering loops in a different way (switching ki and xi):

# loop permutation version
xo, yo, xi, yi = s[C].tile(C.op.axis[0],C.op.axis[1],32,32)
k,             = s[C].op.reduce_axis
ko, ki         = s[C].split(k, factor=4)
s[C].reorder(xo, yo, ko, xi, ki, yi)
s[C].vectorize(yi)    # added already @in@ vectorized version

The array packing version enables better memory accesses to matrix $B$ by introducing a temporary packedB but requires changing the description of the computation in TVM:

packedB = tvm.compute((N / 32, K, 32), lambda x, y, z:
B[y, x * 32 + z], name='packedB')
C       = tvm.compute((M, N), lambda x, y:
tvm.sum(A[x,k] * packedB[y // 32, k, tvm.indexmod(y,32)],
axis=k), name='C')

With this rewritten computation we can now also describe the schedule affecting the computation of the temporary packedB matrix.
Contrary to Halide, this computation is not inlined by default in TVM and results in a separate loop nest.

# same as loop permutation version
x, y, z = s[packedB].op.axis

The write cache for blocks version allocates memory for the reduction accumulator and unrolls loops.
Building up on this, the fully parallel version parallelizes the outermost loop:

# parallel version
CC = s.cache_write(C, 'global')
xo, yo, xi, yi = s[C].tile(C.op.axis[0],C.op.axis[1],32,32)
xc, yc         = s[CC].op.axis
k,             = s[CC].op.reduce_axis
ko, ki         = s[CC].split(k, factor=4)
s[CC].reorder(ko, xc, ki, yc)
s[CC].compute_at(s[C], yo)
x, y, z        = s[packedB].op.axis

In the rest of the case study, we attempt to implement a similar looking scheduling language in for rewriting programs.
We define abstractions ourselves similar to the built-in scheduling primitives provided by TVM.

§.§ Basic Scheduling Primitives as Strategies

The TVM scheduling primitives parallel, split, vectorize, and unroll can be implemented as rewrite rules for .

def parallel: Strategy[Rise] = p => p match
case map => Success( mapPar )
case _   => Failure( parallel )

In , low-level implementation choices such as performing a computation in parallel are encoded with low-level patterns.
For example, the map pattern that applies a function to each element of an array might be performed in a data-parallel fashion as indicated by the mapPar variant of the pattern.
This is precisely what the parallel strategy encodes: rewriting a map pattern into its parallel variant.
A rewrite into the sequential variant mapSeq is defined in the same style.

def @split@(n: Int): Strategy[Rise] = p => p match
case app(map, f) =>
Success( split(n) >> map(map(f)) >> join )
case app(app(reduce, op), init) =>
Success( split(n) >> reduce(fun(a => fun(y =>
op(a, reduce(op)(init)(y)) )))(init) )
case _ => Failure( @split@(n) )

TVM's split scheduling primitive implements loop-blocking (also known as strip-mining).
In , this is achieved by transforming the computation over an array expressed by map(f):
first the input is split into an 2D array using split(n), then f is mapped twice to apply the function to all elements of the now nested array, and finally the resulting array is flattened into the original one-dimensional form using join.
We write f >> g to indicate reverse function composition, i.e.,: fun(x => g(f(x))).
It is important to note, that does not materialize the intermediate two-dimensional array in memory, but only uses this representation inside the compiler for code generation.
There is a second case for splitting reduce resulting in two nested reductions.

def vectorize(n: Int): Strategy[Rise] = p => p match
case app(map, f) if isScalarFun(f) =>
Success(asVector(n) >> map(mapVec(f)) >> asScalar)
case _ => Failure( vectorize(n) )

Vectorization is most efficient when applied to the innermost loop of a loop-nest.
In , this corresponds to applying the vectorize strategy to the innermost map of potentially nested maps.
This is achieved in by bottomUp(vectorize).
The extra constraint isScalarFun(f) ensures that only functions operating on scalars are vectorized by inspecting f's type.
The restriction to scalar functions for vectorization is a current limitation of .

def unroll: Strategy[Rise] = p => p match
case map    => Success( mapSeqUnroll )
case reduce => Success( reduceSeqUnroll )
case _      => Failure( unroll )

The unroll strategy rewrites the high-level map and reduce patterns into low-level patterns that will be unrolled by the compiler.

Identifying Locations

In TVM, named identifiers describe the location at which the optimization should be applied.
For example, TVM's parallel is invoked with an argument specifying the loop to parallelize.
Using named identifiers allows writing invalid schedules, e.g., trying to vectorize a reduction axis failing at runtime when TVM detects the error.

does not use names to identify locations, but instead uses the traversals we defined in <ref>.
The vectorize strategy is – by construction – only applicable at valid locations within the AST.

By using 's traversal strategies, we can apply the basic scheduling strategies in a much more flexible way: e.g., topDown(parallel) traverses the AST from top to bottom and will thus always parallelize the outermost map, corresponding to the outermost for loop.
tryAll(parallel) traverses the whole AST instead and all possible maps are parallelized.
Depending on the desired use case users are free to combine different traversals with the basic scheduling strategies.

§.§ Tiling as an Strategy

Tiling is an important optimization improving the cache hit rate by exploiting locality within a small neighborhood of elements.
TVM's tile is a more complicated scheduling primitive to implement because it is essentially a combination of two traditional loop transformations: loop-blocking and loop-interchange.
In fact, tile in TVM is a built-in combination of split for loop-blocking and reorder for loop-interchange.
We already saw how to implement split using and we will now discuss how to implement tile using a combination of rules, normal-forms and domain-specific traversals.

We use matrix-matrix multiplication as the illustrative example to explain the optimization steps.

Since we use as the target language for the tiling strategy, we need to consider how matrix multiplication is expressed there:

val dot = fun((a,b) => zip(a,b) |> map(*) |> reduce(+,0))
val mm = fun(a :: M.K.float => fun(b :: K.N.float =>
map( fun(arow =>     // iterating over M
map( fun(bcol =>     // iterating over N
dot(arow, bcol)      // iterating over K

Essentially, the dot product is computed for each combination of rows and columns of matrix $A$ and $B$.

In the following, we show how to use to systematically construct a strategy out of simple building blocks that has the same effect as TVM's tile scheduling primitive.
Specifically, we construct a generalized strategy that is able to tile an arbitrary number of dimensions whereas TVM's tile only tiles in two-dimensions.
def tileND: List[Int] => Strategy[Rise]

This strategy expects a list of tile sizes, one per tiled dimension.
The two-dimensional tiling, that is equivalent to TVM's built-in tile scheduling primitives, is expressed as tileND(List(x,y))(mm) for this 2D case we also write tile(x,y)(mm).

The intuition for our tileND implementation is simple:
First, we ensure that the required rules are applicable to the input expression by normalizing the expression using the DFNF normal form.
Then, we apply the previously introduced split strategy to every map to be blocked, recursively going from innermost to outermost.
Finally, we interchange dimensions accordingly.

def tileND(n: List[Int]): Strategy[Rise] =
DFNF `;` (n.size match
case 1 => function(split(n.head)) // loop-blocking
case i =>
fmap(tileND(d-1)(n.tail)) `;`   // recurse
function(split(n.head))   `;`   // loop-blocking
interchange(i)     )           // loop-reorder

In the following, we first introduce the required normal-forms (e.g., DFNF), then explain how we recursively traverse (fmap) to apply loop-blocking and finally briefly explain how we interchange dimensions in (interchange).

Normal forms
In , we introduced normalize to ensure that expressions are in a particular form expected by the implementation of rewrite rules.

$\lambda$-calculus (and ) allows for semantically equivalent but syntactically different expressions.

For example, fun(x => f(x)) is equivalent to f iff x does not appear free in f.
Transforming between these representations is called $\eta$-reduction and $\eta$-abstraction.

The simplest normal-form we use is the $\beta\eta$-normal-form (BENF) which exhaustively applies $\beta$- and $\eta$-reduction:
def BENF = normalize(betaReduction <+ etaReduction)

As not every function abstraction is $\eta$-reducible, the function arguments of 's higher-order patterns map and reduce might have different forms.
Therefore, we introduce a normal form making the data flow explicit by ensuring a function abstraction is present in every higher order pattern:

def DFNF = BENF `;`
// the argument of a map is a function abstraction
normalize(argOf(map, not(isFun)`;`etaAbstraction))`;`
// ... similar normalization for reduce primitive

The definition shows the normalization for map.
A similar case exists for reduce.

Using the not and isFun predicates, that are themselves strategies, we describe the desired form in a natural and elegant way.

Recursively Applying Loop-Blocking
In order to recursively apply the loop blocking strategy to nested maps, we make use of the -specific traversal fmap:
[style=elevate-rise-short, xleftmargin=.25]
def fmap(s:Strategy[Rise])=function(argOf(map,body(s)))

fmap essentially traverses to the function argument of a map primitive and applies the given strategy s. For example,

skips two maps applying loop-blocking to the innermost map.

Interchange in
After recursively blocking all maps, we use interchange to rearrange the dimensions in the correct order.
For simplicity, we describe the two dimensional case:
after loop-blocking the data is four-dimensional and we must swap the two inner dimensions.
To achieve this we introduce two transpose patterns and then move one of the transpose into the right position.
Doing it this way every strategy is a semantics-preserving transformation ensuring the correctness of the overall optimization.

§.§ Reordering as an Strategy

Due to the loopless nature of , implementing TVM's reorder primitive as a strategy is more complicated.
Instead of simply interchanging perfectly nested loops, the same is achieved in by interchanging the nesting of map and reduce patterns.
Therefore, there are multiple possible combinations to consider and the implementation of each rewrite rule requires reasoning about why exchanging the specific patterns is possible in the first place.

We implemented a reorder strategy in but its implementation is non-trivial and, therefore, it is not discussed here.
While it is possible to implement TVM's reorder primitive, this particular loop transformation is just not a good fit for the pattern-based abstractions in the language.

§.§ Matrix Multiply Schedules as Strategies

Using the TVM-like scheduling abstractions implemented as strategies, we are now able to discuss how we combine them together to describe entire schedules in .

For baseline, TVM does not provide a schedule, but we describe the implicit behaviour of the compiler explicitly:
(DFNF `;` topDown(fuseReduceMap) `;` lowerToC)(mm)

The TVM algorithm computes the dot product in a single statement.
The program describes the dot product with separate patterns which are fused using fuseReduceMap.
The lowerToC strategy lowers every high-level pattern into its low-level sequential version:
map is rewritten into mapSeq and reduce into reduceSeq.

For the blocking version, we reuse the same lowerToC strategy but first we leverage the abstractions that we have build emulating the TVM schedule in a similar style:
val blocking = ( topDown(tile(32,32)) `;;`
topDown(isReduce `;` @split@(4)) `;;`
topDown(reorder(Seq(1,2,5,6,3,4))) )
(blocking `;` lowerToC)(mm)

First we tile, then we split and then we reorder, just as specified in the TVM schedule.
We describe locations using the topDown traversal and the isReduce strategy predicate that applies the following split only if the current expression is a reduction.
We use the `;;' combination to normalize using DFNF between each step.

The loop permutation version incorporates the changes of the vectorized version by adding vectorize and a different reordering of dimensions.
In contrast to TVM we identify dimensions by index rather than by name.
val loopPerm = (topDown(tile(32,32)) `;;`
topDown(isReduce `;` @split@(4)) `;;`
topDown(reorder(Seq(1,2,5,3,6,4)))) `;;`
(loopPerm `;` lowerToC)(mm)

For the array packing version, we are not required to change the program manually, but can apply the array packing of matrix $B$ as a rewrite step.
Afterwards, we can reuse the loopPerm strategy before the packed representation of $B$ is vectorized and then copied in parallel.
val arrayPacking = (packB `;;` loopPerm `;;`
topDown(vectorize(32)) `;;`
(arrayPacking `;` lowerToC)(mm)

For the parallel version, we reuse the prior array packing strategy only changing the way we lower the high-level code.
We parallelize the outermost loop with topDown(parallel) and unroll the innermost reduction using bottomUp(isReduce `;` unroll) before lowering the remaining high-level patterns to sequential code as before.
(arrayPacking `;;` topDown(parallel) `;;`
bottomUp(isReduce `;` unroll) `;` lowerToC)(mm)

We have demonstrated that it is feasible to implement a TVM-like scheduling language in by expressing schedules as compositions of reusable strategies.

§.§ Experimental Evaluation

In order to evaluate the practicability and the scalability of , we performed two experiments.

/pgf/number format/fixed,
scaled y ticks = false,
ylabel=Rewrite Steps,
bar width=14pt,

symbolic x coords=

y label style=font=,
y tick label style=font=,
x tick label style=rotate=0, font=, align=center,
cycle list/Paired,
every axis plot/.append style=fill,draw=black,no markers
[fill = Paired-F]
(,         211)
(,       92980)
(,  94030)
(,  143270)
(,   144183)
(,      144074)

Total number of successful rewrite steps when applying different optimization strategies.

Number of Rewrite Steps
In the first experiment, we are interested in the scalability of our approach by counting the number of successfully applied rewrites steps performed when applying a strategy to the matrix multiplication expression.
<Ref> shows this number for every strategy shown in the previous subsection.
Since no major optimization strategies are applied to the baseline version, only 211 rewrite steps are performed.
However, as soon as interesting optimizations are applied, we easily reach about 100,000 steps for the next three versions and about 150,000 for the most complicated optimizations.
The loop-permutation case slightly drops in numbers of applied rewrite rules because the specific nesting prescribed in TVM's schedule required fewer loop-interchanges.

These high numbers clearly show that abstractions are required to control this many rewrite steps.
It also shows the scalability of our compositional approach in which complex optimizations are composed out of a small set of fundamental building blocks.
The high-level strategies encode practical optimizations and hide massive numbers of individual rewrite steps that are actually performed.

Overall, applying the strategies to the expression took less than 50 seconds per version on a commodity notebook.

/pgf/number format/fixed,
scaled y ticks = false,
ylabel=Absolute Runtime (ms),

ytick=0, 50, 100, 200, 500, 1000, 2000,
log ticks with fixed point,
y tick label style=
/pgf/number format/.cd,
fixed zerofill,
bar width=7pt,

symbolic x coords=

legend style=at=(0.8,0.9),anchor=north,legend columns=1,font=,
y label style=font=,
y tick label style=font=,
x tick label style=rotate=0, font=, align=center,
cycle list/Paired,
every axis plot/.append style=fill,draw=black,no markers
[fill = Paired-G]
(,         1961.470022)
(,       230.9482337)
(,  237.1613752)
(,  109.1119637)
(,   99.76219681)
(,      71.86741923)

[fill = Paired-F]
(,      2742.235474)
(,       149.154503)
(,  149.1949995)
(,  108.184498)
(,   119.689003)
(,      41.785)

TVM, Elevate+Rise

Performance of TVM vs. generated code that has been optimized by strategies.

Performance Comparison
In the second experiment, we are interested in the performance achieved when optimizing programs with compared to TVM.
Ideally, the code optimized with should be similar to the TVM-generated code and achieve competitive performance.
We generated LLVM code with TVM (version 0.6.dev) and C code for annotated with OpenMP pragmas for the version which include parallelization or vectorization.
The generated C code was compiled with clang (v.9.0.0) using -Ofast -ffast-math -fopenmp which echoes the settings used by TVM and Halide[<https://github.com/halide/Halide/issues/2905>].
The measurements were performed on an Intel core i5-4670K CPU (frequency locked to 3.4GHz) running Arch Linux (kernel 5.3.11-arch1-1).
We measured wall-time for -generated code and used TVM's built-in measurement API.
We measured 100 iterations per version reporting the median runtimes in milliseconds.

<Ref> shows the performance of and TVM generated code using a logarithmic scale.
The code generated by controlled by the optimization strategies performs competitive to TVM.

Similar to the results of the Halide case study, our experiment shows a matching trend when comparing to TVM's versions with equivalent optimizations.
The most optimized parallel generated version improves the performance over the baseline by a factor of about 110x.
This means that the strategies we developed using , that are defined in an extensible style by composing individual rewrite steps, scale to a level where they actually encode practically useable and relevant optimizations.

In this section, we introduce how to use the core concepts of to build optimizations typically applied by state-of-the-art optimizing compilers like Halide or TVM.
As a running example, we use as the target language for the optimizations we develop.
However, is not in any way restricted to optimize programs only.
In contrast, we also show how to use to optimize F-Smooth, a new programming language targeted towards automatic differentiation.
Finally we also briefly explain how meta-optimize strategies by using to optimize itself.

Strategic Rewriting and Scheduling Languages
In traditional strategic rewriting, the goal is usually to find the most efficient (i.e., shortest) sequence of rewrites required to reach a desired normal-form for a given term, graph or expression.
Targeting a single normal-form is sufficient in restricted settings such as transforming arithmetic expressions into sums-of-products or transforming boolean expressions into disjunctive normal-form.
When optimizing more interesting programs such as dense linear algebra on multi-dimensional tensors however, a single normal-form does not necessarily cover all desirable points in the exploration space of possible implementations, if it exists at all.

The growing popularity of scheduling languages exposed in optimizing compilers such as Halide, TVM or Tiramisu solve this problem by providing a small set of optimization primitives.
These primitives allow users to guide the optimization process when optimizing for different hardware architectures or metrics like runtime or energy-efficiency.
Unfortunately, these scheduling primitives are usually built into the compiler infrastructure, defined in an ad-hoc manner as black-box APIs and are usually not extensible.

With , we aim to provide a principled framework which allows to build optimization strategies similar to the scheduling primitives in prominent compilers.
Specifically, allows to break down and define complex optimizations as a sequence of simple program transformations.
In the following, we explain how we implement recurring optimizations such as tiling in a principled way by composing simple building blocks including several normal-forms, strategy combinators and domain-specific traversals.

Multi-dimensional Tiling as a Strategy
As a running example, we'll consider the prominent tiling optimization and apply it to matrix multiplication.
The code for the unoptimized matrix multiplication contains the typical three loops:
for (int i = 0; i < M; ++i)
for (int j = 0; j < N; ++j)
for (int k = 0; k < K; ++k)
C[i][j] += A[i][k] * B[k][j];

Halide, TVM and Tiramisu provide a  scheduling primitive to generate the following optimized code in which the two outermost loops are tiled.
K loop is between tiled and inner loops! Move further inside, this is what halide and tvm also do most likely
for (int m = 0; m < M; m += Mtile)
for (int n = 0; n < N; n += Ntile)
for (int k = 0; k < K; ++k)
for (int i = 0; i < Mtile; ++i)
for (int j = 0; j < Ntile; ++j)
int row = m + i; int col = n + j;
C[row][col] += A[row][k] * B[k][col];

Essentially tiling is a combination of loop-blocking (i.e., strip-mining) and loop-interchanges.
In fact,  in Halide is an alias for applying  (strip-mining) twice, blocking the outermost two loops, plus an additional  (loop-interchange) call which makes sure all loops are in the correct order.
In some sense, one could already argue Halide's  is some kind of strategy composed of simpler building blocks.
Nevertheless, by decomposing tiling even further using , we gain a much more flexible strategy composed of generic building blocks with well defined semantics.

In the following, we consider the following matrix multiplication expression which generates the exact same three-loop code as shown before.
dot = @$\lambda$@a. @$\lambda$@b. ((reduce + 0) @$\circ$@ (map *)) (zip a b)
// a : M.K.float, b : K.N.float
mm = @$\lambda$@a. @$\lambda$@b.
map( @$\lambda$@ak.    // iterating over M
map( @$\lambda$@bk.    // iterating over N
dot ak bk    // iterating over K
) (transpose b)
) a

We show how to use to systematically construct a strategy out of simple building blocks which has the same effect as the existing  scheduling primitives.
Specifically, we construct a strategy $\textit{tileND}: \text{List[int]} \rightarrow \text{Strategy}_\Lift$ which expects a list of tile sizes, one per dimension.
$(\textit{tileND} \, [16,16] \, \text{mm})$ then returns the following tiled matrix multiplication expression which compiles to the optimized C code:
@$\lambda$@a. @$\lambda$@b. join o (map (map join)) o (map transpose) o
(map    // iterating over M
(map     // iterating over N
(map     // iterating over Mtile
(map     // iterating over Ntile
(reduce  // iterating over K
(@$\lambda$@y. @$\lambda$@acc. acc + y@$_1$@ * y@$_2$@) 0)
// loop-interchange
))) o transpose o ((map @$\lambda$@z. ((map (map (zip z)))
// strip-mine M and N dimension
((split 16) (transpose b)))))) ((split 16) a)

Note that we use two-dimensional tiling of matrix multiplication because it is a well known optimization in the systems community.
However, our tiling strategy is neither specialized for tiling two nested loops (such as the scheduling primitives in Halide, TVM and Tiramisu) nor specific to matrix multiplication.

§.§ Strip-Mining and Loop Interchange

In order to build a multi-dimensional tiling strategy we need to implement strip-mining and loop-interchange.
Once these strategies are available, the overall plan is simple:
1. strip-mine every loop to be tiled,
2. reorder the loops appropriately.
Since 's map directly corresponds to a -loop, implementing strip-mining as a strategy is straight forward.
It simply corresponds to the split-join rewrite rule:

\begin{equation*}
\text{map} ~ f \rightarrow \text{join} \circ (\text{map}(\text{map} ~ f )) \circ (\text{split} ~ n)
\end{equation*}

where $n$ determines the tile size.

Loop-Interchange Intuition
Loop-interchange is implemented by carefully adding a combination of map and transpose primitives to the expression.
Consider the following simple expression which applies a function $f$ to a three-dimensional tensor:

\begin{equation*}
\lambda a:M.N.O.\text{float} \, . ~ (\text{map}(\text{map}(\text{map} ~ f ))) ~ a
\end{equation*}

The nested map primitives correspond to nested for loops and thus, this expression compiles to the following C code:
for(int i = 0; i < M; i++)
for(int i = 0; i < N; i++)
for(int j = 0; j < O; j++)  /* f */

Interchanging these loops in is achieved by applying transpose before and after the applying $f$.
For example, in order to change the outermost two loops we write:

\begin{align*}
&\lambda a:M.N.O.\text{float} \, . \\
&(\text{transpose} \circ ~ (\text{map}(\text{map}(\text{map} ~ f ))) \circ \text{transpose})~ a
\end{align*}

Applying transpose to $a$ interchanges the two outermost dimensions of the tensor ($M$ and $N$ in this case) and thus, the order of the for-loops during compilation change as well.
In order to change the innermost two loops we have to apply transpose within the first map which swaps the order of the $N$ and $O$ dimension:

\begin{align*}
&\lambda a:M.N.O.\text{float} \, . \\
&(\text{map}~(\text{transpose} \circ \text{map}(\text{map} ~ f ) \circ \text{transpose}))~ a
\end{align*}

Interchanging multiple loops requires to simply apply the correct combination of map and transpose primitives.

Loop-Interchange Strategy
Since we need to implement loop-interchange as a semantics-preserving strategy, we need to find a sequence of rewrites which adds the desired combination of primitives to our target expression.
Specifically, we need three separate rewrite rules to implement a simple loop-interchange strategy which swaps the two outermost for-loops:

\begin{align}
f &\rightarrow \text{id} \circ f \tag{R1}\\
\text{id} &\rightarrow \text{transpose} \circ \text{transpose} \tag{R2}\\
(\text{map}~(\text{map} \, f)) \circ \text{transpose} &\rightarrow \text{transpose} \circ (\text{map}~(\text{map} \, f)) \tag{R3}
\end{align}

The strategy implementing loop-interchange is defined as:

\begin{align*}
\text{loopInterchange} = \text{(R1) ; (R2) ; (argument (R3)) }
\end{align*}

Visualization of loop-interchange implemented as an strategy

Note that R2 is a short form for a context sensitive rule which asserts the type of the argument of id is at least a two dimensional tensor such that transpose is actually applicable.
Figure <ref> visualizes the transformation sequence for applying the loop-interchange strategy to our initial expression.
We highlight the locations in the AST where the rules of each step are applied.
We need to wrap the third rule (R3) in an argument traversal primitive in order to traverse to the second transpose primitive which needs to be swapped with the map-nest.

Extended Loop-Interchange
The current loop-interchange strategy is only able to swap the two outermost loops.
In order to swap any adjacent pair of loops we need to extend this strategy slightly.
Note that swapping non-adjacent loop pairs is always expressible as a combination of swapping adjacent loops.
The following strategy implements loop-interchange at an arbitrary depth, where a depth of 0 corresponds to interchanging the two outermost loops:
// interchange adjacent loops at depth d
loopInterchangeAtDepth : Int @$\rightarrow$@ Strategy
loopInterchangeAtDepth = @$\lambda$@d.
applyNTimes d (@$\lambda$@s. fmap s) loopInterchange

// applies f n-times to s
applyNTimes : Int @$\rightarrow$@ (Strategy @$\rightarrow$@ Strategy) @$\rightarrow$@ Strategy @$\rightarrow$@ Strategy
applyNTimes = @$\lambda$@i. @$\lambda$@f. @$\lambda$@s.
if(i <= 0) s else (applyNTimes i-1 f (f s))

// applies s to the function-argument of a map primitive
fmap : Strategy @$\rightarrow$@ Strategy
fmap = @$\lambda$@s. (function (argumentOf map (body s)))

Here, argumentOf is a more restricted argument traversal which only applies its strategy to the argument of an apply node, if the applied function of this node is of a specific type:

\begin{align*}
&\text{argumentOf} : \Lift \rightarrow \text{Strategy}_\Lift \rightarrow \text{Strategy}_\Lift \\
&\text{argumentOf} = \lambda x. \lambda s. \lambda p. \\
\textit{Success}\,(x \, (s \, e)),& \text{if } p = (x \, e)\\
\textit{Failure}\,(\text{argumentOf}\, x \,s),              & \text{otherwise}
\end{cases}
\end{align*}

For example, (loopInterchangeAtDepth 1) evaluates to (fmap loopInterchange).
The intuition here is simple:
Instead of applying the loopInterchange strategy to the outermost map as before, we apply it to the next nested one using the fmap traversal strategy.

(fmap s): Traverse to the function-argument of a map primitive and apply strategy $s$ there

Figure <ref> visualizes the fmap traversal strategy which is a good example for a useful domain-specific traversal because it allows us to prescribe a specific AST structure we require in order for the strategy to succeed.
In this case, we want to apply loopInterchange to a nested map or we want the whole strategy to fail in case there is no nested map, i.e., there are no more inner loops to interchange.
Note that the fmap traversal expects the function argument of a map primitive to be a $\lambda$.
Unfortunately, this means that fmap fails if we apply it to the ASTs shown in Figure <ref> where this is not the case since all expressions are in beta-eta-normal-form.

§.§ Normal-forms

Strategies like fmap expect expressions to be in a particular form in order to be applicable.
In lambda calculus, and therefore in , there are multiple possibilities to create semantically equivalent but syntactically different expressions.
For example, $\lambda x.f\,x$ is equivalent to $f$ iff, $x$ does not appear free in $f$.
Transforming $\lambda x.f\,x$ to $f$ is called eta-reduction and the reverse way is called eta-abstraction.

In the following we introduce several normal-forms which we use during the optimization of programs.
These normal-forms ensure that the AST is in a specific shape as expected by the strategies.

Beta-Eta-Normal-Form (BENF)
The simplest normal-form we use is the beta-eta-normal-form:

\begin{equation*}
\text{BENF} = \text{normalize}~(\text{betaReduction <+ etaReduction})
\end{equation*}

We mainly use BENF to reduce the size of our ASTs.
All expressions in Figure <ref> are in beta-eta-normal-form.

Data-Flow-Normal-Form (DFNF)
Not every $\lambda$ abstraction is eta-reducible.
Therefore, function arguments to 's higher-order primitives such as map or reduce might have different structure, i.e., $\lambda x.f\,x$ or plain $f$ depending on whether $x$ is bound or free in $f$.
In order to reduce the size of required rewrite rules which match against the structure of the AST, we use the DFNF to unify the structure of function arguments to higher-order primitives.
DFNF = BENF ;
// every function-argument of a map is a lambda
normalize(argumentOf map ((not (is @$\lambda$@)) ; etaAbstraction)) ;
// ... similar normalization for reduce primitive

Note how the following definitions of not and is allow us to perform boolean-like arithmetic with strategies:

\begin{align*}
&\text{not} : \text{Strategy}_P \rightarrow \text{Strategy}_P \\
&\text{not} = \lambda s. \lambda p.
\begin{cases}
\textit{Success}\,(p),& \text{if } (s \, p) = \text{Failure(s)}\\
\textit{Failure}\,(\text{not} \, s), & \text{if } (s \, p) = \text{Success(e)}
\end{cases}
\end{align*}

\begin{align*}
&\text{is} : P \rightarrow \text{Strategy}_P \\
&\text{is} = \lambda x. \lambda p.
\begin{cases}
\textit{Success}\,(p),& \text{if } x = p\\
\textit{Failure}\,(\text{is} \, x),              & \text{otherwise}
\end{cases}
\end{align*}

First, the AST is beta-eta-normalized.
Then, we unify the structure of the function arguments to 's higher order primitives.
Specifically, every argument of a map primitive which is not yet a $\lambda$ abstraction will be eta-abstracted.
Note how we only apply etaAbstraction if the argument of a map is not a $\lambda$ abstraction already.
If it is a $\lambda$ abstraction, the (not (is $\lambda$)) part fails and we do not continue applying the strategy to the right of the sequence (;) combinator.
Additionally, this conditional check ensures termination of the normal-form as (normalize (argumentOf map etaAbstraction)) alone would not terminate since one can endlessly eta-abstract any expression in lambda calculus.

The binary operator of reduce is similarly normalized but this is omitted because of brevity here.
We call this normal-form DFNF because introducing $\lambda$ abstractions makes the dataflow within the AST explicit.
For example, applying DFNF to (map(map(map f)) a) results in

\begin{equation*}
((map \lambda\eta1. ((map \lambda\eta2. ((map \lambda\eta3. (f ~ \eta3)) ~ \eta2)) ~ \eta1)) ~ a)
\end{equation*}

Rewrite-Normal-Form (RNF)
Both, BENF and DFNF are lambda-calculus-specific but agnostic to any -specific primitives.
not entirely true, DFNF makes use of map and reduce
Finally, we introduce one more normal-form which ensure a certain -specific structure:

\begin{equation*}
\text{RNF} = \text{normalize}~\text{map-fission}
\end{equation*}

where map-fission is the inverse of the map-fusion rule and is defined as:

\begin{equation*}
\text{map-fission} = \text{map}~(f \circ g) \rightarrow (\text{map}~f)\circ(\text{map}~g)
\end{equation*}

The rewrite-normal-form fissions as many maps as possible.
This especially simplifies the use of parenthesis in expressions as every primitive is then either nested in maps or standing on its own.
not entirely true, e.g., reduce operators or arguments of zip
As ASTs grow more complex rather quickly when applying multiple optimizations, this normal-form significantly simplifies the development of more complex optimizations.
The following shows the effect of normalizing a expression using RNF:

\begin{align*}
&\text{RNF} ~ (\text{map}~(\text{f} \circ (\text{map}~((\text{map} ~ g ) \circ \text{h})))) \\
=& ~(\text{map}~\text{f})\circ(\text{map}~(\text{map}~(\text{map}~g)))~\circ\\
& ~(\text{map}~(\text{map}~\text{h}))
\end{align*}

The input expression is much more concise but the normalized expression is significantly easier to read and to reason about.
Especially, it allows us to define another useful domain-specific traversal move:

\begin{align*}
&\text{move} : \text{Int} \rightarrow \text{Strategy}_\Lift \rightarrow \text{Strategy}_\Lift \\
&\text{move} = \lambda i. \lambda s. ~(\text{applyNTimes} ~ i ~ (\lambda e.~(\text{argument}~e)) ~ s)
\end{align*}

Intuitively, this traversal allows to move along function compositions, i.e., (move $0$ $s$) evaluates to $s$ and is applied at the root (i.e, the first map nest) whereas (move $2$ $s$) evaluates to (argument (argument $s$)) and applies $s$ to the third map nest: (map (map h)).

§.§ Tiling: Putting everything together

Now we have all building blocks available to create a multi-dimensional tiling strategy.
list is parameterized using brackets, Strategy is parameterized using subscript. use one notation for the same thing!
tileND : List[Int] @$\rightarrow$@ Strategy@$_\Lift$@ =
tileND = @$\lambda$@l. (size l) match
// nothing to tile
case x if x <= 0 => id
// simply apply split-join rule
case 1 => (function (split-join (head l)))
// tile inner loops first...
case i => (fmap (tileND (tail l))) ;
// ...tile current loop + reorder loops
(tileND [(head l)]) ; (shiftDim i)

shiftDim : Int @$\rightarrow$@ Strategy@$_\Lift$@
shiftDim = @$\lambda$@d.
let joins = d
let transposes = (1 to d-2).sum
RNF `;` shiftDimRec(joins + transposes)(d-1)

// (p)osition: how far to move until we reach maps
// (d)epth:    how deep transpose pairs are nested in maps
shiftDimRec : Int @$\rightarrow$@ Int @$\rightarrow$@ Strategy@$_\Lift$@
shiftDimRec = @$\lambda$@p. @$\lambda$@d. DFNF ; (d match
case 1 => (move p (loopInterchangeAtDepth 1))
case d => (shiftDimRec p d-1) ; RNF ;
(move p+d-1 (loopInterchangeAtDepth d))

tileND is defined recursively which allows us to tile arbitrary many loops in arbitrary deep loop-nests.
Remember that a loop nest of depth $n$ corresponds to $n$ nested maps in .
The base case is simple:
If we want to tile a single loop, we only need to apply the split-join rule and no loops have to be reordered.
If we want to tile more than one loop, the intuition is as follows:

The recursive calls are structured such that we tile the loops from innermost to outermost.
Figure <ref> shows the first three steps of tiling a loop nest of depth $n$.
First, we traverse to and tile the innermost loop to be tiled using fmap and simply apply the split-join rule (step 1).
No dimensions need to be reordered in this step.
Then, we progressively move outwards to tile the remaining loops while assuming all inner loops are already ordered appropriately.
Specifically, when we tile loop $n-1$ as shown in step 2 of Figure <ref>, the newly created loop needs to be moved one level inside the loop nest (step 3).
If we would continue to tile loop $n-2$ we would have to move the two loop two levels further inside and so on.

Moving the newly created loops is implemented in shiftDim.

§.§ Implementing a Scheduling Language

Show more examples like reorder or vectorize without too much information and detail.

§.§ F~  and Meta-Optimization?

Do we want to say something about that here and if so, what?

Somehow show that is essential to drive the rewriting process of an IR like .
Count how many single steps a typical scheduling program in Halide/TVM would take.

§ RELATED WORK

Term Rewriting and Strategy Languages
is inspired by existing strategy languages, especially ELAN <cit.> and Stratego <cit.>, which introduce combinators to support user-defined strategies in the context of term rewriting systems.
Similar rewriting systems include <cit.>.
Program transformations using rewrite rules and strategy languages have since been used in many different domains including reverse engineering <cit.>, refactoring <cit.>, and obfuscation <cit.>.
Visser <cit.> and Kirchner <cit.> provide surveys covering term rewriting, strategy languages and their application domains.

To the best of our knowledge, is the first strategy language that has been used to specify state-of-the-art compiler optimizations such as tiling focusing on high performance code generation.

Rewriting in Compilers
Rewrite rules and rewriting strategies have also been used when building compilers.
The Glasgow Haskell Compiler <cit.> uses rewrite rules as a practical way to optimize Haskell programs and Visser et. al. <cit.> describe how to build program optimizers using rewriting strategies.
Other areas include building interpreters <cit.>, instruction selection <cit.> or constant propagation <cit.>.
More recently, Lift <cit.> showed how to use rewrite rules to generate high-performance code targeting accelerators.

Controlling the application of rewrite rules in compilers still largely is built-in in a fixed way based on heurisitcs.
In this work, we showed how to use instead, allowing a more flexible and practical approach towards using rewrite rules for describing optimizations in compilers.

Schedule-based Compilers
Halide <cit.> introduced the concept of schedules describing program optimizations separate from the algorithm describing the computation.
This concept has been adopted by many other frameworks in domains including machine learning (TVM <cit.>), graph applications (GraphIt <cit.>) or polyhedral compilation (Tiramisu <cit.>, CHiLL <cit.>, AlphaZ <cit.>, URUK <cit.>).

These existing scheduling APIs are not designed as principled programming languages.
Instead, a fixed set of ad-hoc built-in primitives is exposed allowing users to specify which optimizations to apply.
In this work, we showed how to use to implement scheduling languages from first principles as composition of rewrite rules.

§ CONCLUSION

In this paper, we presented : a language for describing optimization strategies.
follows a tradition of prior systems used in different contexts that express optimization strategies as composition of rewrites.
We showed that, in contrast to existing systems with scheduling APIs such as Halide and TVM, programmers are not restricted to a set of built-in optimizations but define their own optimization strategies.
Using three case studies, we demonstrated 's flexiblity to rewrite different languages (and ), its extensibility to add custom abstractions inlcuding domain-specific optimizations, and its practicality to scale to complex optimization strategies requiring 150k rewrite steps used in deep learning.
We showed that successfully optimizes programs in the language achieving competitive performance compared to Halide and TVM.

§.§ Movement Rules

(or some other names) simple and easy-to-proof rewrite rules. Basic building block for every optimization. Easy to proof correct. Rewrite rules which cannot be divided into smaller parts, somewhat minimal whatever that means for a rewrite rule.

§.§ Family of Rewrites

Combining several similar (what does this mean) rewrite rules to a family of rewrite rules. Actually the way we defined them is quite interesting. Each family consists of infinitely many rewrite rules. For example the family:

Transpose o Map(Map(f)) = Map(Map(f)) o Transpose

This family contains the members:

T $\circ$ **f = **f $\circ$ T

*T $\circ$ ***f = ***f $\circ$ *T

**T $\circ$ ****f = ****f $\circ$ **T

***T $\circ$ *****f = *****f $\circ$ ***T

and so on

maybe for the sake of this paper we should treat split not as a separate pattern but as the special case slide(n,n)
We can most likely get rid of this concept and use Family(? sounds stupid) = Repeat(mapFusion) >> Apply(baseRule) >> RewriteNormalForm instead.
Allows to keep rewrite rules much simpler and shows again how nice these strategy primitives are.

§.§ Strategy building blocks

Not entirely new. What is new for in our approach? Allows to define generic optimization strategies.
Allow to provide Halide-like scheduling primitives but with correctness guarantees.
New: Blocks which go from program to set of programs or from set of programs to set of programs.
Useful to define a search space.
Follow up questions: What do we do with the search space?
Whats the structure of that space? Plain list, tree, ...?

Rewrites required for applying tiling:

* 1D: 12

* 2D: 42 (tedious for humas)

* 3D: 100 (already infeasible to do by hand - and this is only tiling (without local memory))

* 4D: ? - Still interesting use case and actually required for 4D Tensor applcations eg. Batched GEMM or Conv-Layers

What about regions and locations?

§.§ Normal forms

We define normal forms for rewriting and codegen. However, we're not using them in the traditional rewriting sense where you define a normal form and try to reach this with a automatic rewrite engine. Traditionally: Define normal form: try to reach this via automated rewriting. We: Define normal form, transform expression to normal form, and only then we begin doing some serious rewriting. The normal forms are more enabling states rather than desired states if that makes sense.

§.§ Usecase

Take point-wise neural network which zips some bias and weight to the input and show that the tiling strategy is applicable to this

§.§ Christophes Questions

A strategy is kind of a rewrite rule itself (just like a "macrorule"). Can we, should we be able to define rewrite rules in the stategy language itself?
For now, the strategy stuff sits on top of the existing rewrite stuff.
Would it be worth it defining rewrite rules themselves in the strategy language and what would we gain?

§.§ Questions

Whats the problem we're solving here?
How to we control applying the rewrite rules?
Why do we want control?
- Manually dictate how to do it (for particular hardware)
- Tradeoff: control manual vs automatic

Why do we want a formally defined language vs Halide-like?
What are benefits of formal definition? -> How do we measure them?
How do we argue for them? Expressiveness? Performance? Competition?

Motivates Elevate: A language to express strategies

(Optimization-)Strategy: f: Progr -> Progr?
A program transformation that improves some performance metric we care about?

... oh there's a problem :)

Design Section (if we would have a language like this, this would solve all the problems):
Design Goals for this language, what should the language look like?
Evaluate these:?
compositional! allows to build our own abstractions
only small set of rules required
separation between rules themselves and strategies, allows extensibility of the set of rules
Goal? Expressing generic strategies vs domain-specific strategies
(3-4 pages? until here)

Core language:
Core concepts: Rule Strategy Location
Normal forms?
Basic Strategies: Apply, Try, ...
How to compose?
Traversals? BFS, DFS?

How do we build abstractions?

Tiling  on GPUs ...
What is tiling?

Some form of performance evaluation?

§.§ Thoughts/Notes

* Our new reorder strategy is similar to Halide's built-in  schedule primitive and furtharks built in primitive

* I think our rewrite systems/normal forms are always confluent because they are always deterministic whereas in traditional rewriting systems the rule application is non-deterministic

* is the confluence concept even applicable to our strategies since everything is deterministic?

* phrase: break down complex transformations into a sequence of simple transformations

* use polyhedral loop transformation names: like tiling = stripmining + interchange?

* assuming our rules are semantics preserving, all our strategies are strategy preserving as well (can we show this somehow? transitivity of some kind?)

* related work: rewriting recursive programs: Composable, sound transformations of nested recursion and loops

* we could also show example strategy building blocks using standard polyhedral transformations as an example: showing the output of stratgy(map(map(id))) for example

* specific rewrite rules (e.g., liftReduce) require type information which might be interesting to talk about

* elevate not only nice to have (for lift) but essential if you look at the number of rewrites required to optimize something simple like matmul

* related work: compare with different autmatic programming optimization techniques like auto-tuning etc. Hadis Deep Learning compilation paper. Albert Cohens partial specifications. ETH? Tree things, need to find that paper again

* elevate meta optimization might actually become important because rewriting now takes a couple of minute:wq

* compare matmul against cuda samples. simple example which nevertheless already applies tiling and shared memory usage - does halide have any matmul examples for CPU?

“we implemented a simple, brute- force auto-tuning system that searched the low-dimensional space of auto-scheduler parameters, rather than the space of Halide schedules.” from "Automatically scheduling halide image processing pipelines"

§.§ OLD

§.§ Normal forms

In , we make heavy use of two normal forms to orchestrate the optimization of Lift programs via rewrite rules.
During the optimization of a single expression, we normalize expressions multiple times to...
In contrast to existing strategic rewriting, our normal forms are simple and have desirable properties such as confluence and termination which allows us to

The fissioned-maps normal form normalize($*(f\circ g) \rightarrow *f \circ *g$) is used during rewriting and ensures that ...?
The fused-maps normal form normalize($*f \circ *g \rightarrow *(f\circ g) $) is used for code generation and ensures that we fuse as many maps as possible.
This is especially important for mapping the lift expressions to the targeted parallel architecture as we will explain in Section (parallesims mapping).

It's obvious that both, the fissioned-maps and the fused-maps normalforms are confluent as well as terminating.
map-fusion and fission is associative and in a finite expression there are only a finite number of possible locations which can fused or fissioned respectively.

§.§ Movement Rules / Family of Rules

When trying to optimize real world programs expressed in Lift, we need to be able to rewrite expressions composed of hundreds of single primitives.
You can do so in two ways:
One possible option is that the rewrite systems in use has a large collection of powerful rules which allow to rewrite large parts of the expression.
This approach was used in previous versions of lift, the rules were called macrorules.
The downside of this approach is that for every new requirement, architecture, optimization etc, you have to have an expert who writes a new macro rule.

Another option is to have a small set of simple but composable rules which are easy to reason about and use strategic primitives to compose the simple rules in meaningful ways to achieve the same effect as the macrorules once had.
The rewrite normal form allows us to think only about the relationship of two adjacent primitives.
Additionally, one or both primitives can be mapped in arbitrary many maps.
We can neglect the case where both primitives are wrapped in maps as we can fuse them until only one or no primitive is wrapped in maps and after applying a movement rule, fuse them back together.

The following movement rules describe the relationship of pairwise lift primitive combinations:

In order to handle the case where both primitives are wrapped in maps we introduce a new concept call family of rewrites.
For every movement rule we can define a family of similar rules as a strategy.
Informally, every family consists of a parent movement rule which defines the relationship of two adjacent primitives, e.g., $\text{parent:} f\circ g \rightarrow g \circ f$.
The family belonging to this parent conceptually contains the following rules: $*f\circ *g \rightarrow *g \circ *f$, $**f\circ **g \rightarrow **g \circ **f$ and so on.
Since every family contains infinite rules we do not list them explicitly but define them as a strategy where we apply three steps:

* fuse all maps until either only one or none of the two target primitives is wrapped in maps

* apply the parent rule

* fission all maps again, restoring the rewrite normal form

Below is the scala defintion for movement families.

private def increasePosition(p: Position, i: Int): Position =
if (i == 0) p else increasePosition(p++, i-1)

private case class MovementFamily(rule: Rule, location: Location) extends Strategy
def apply(lambda: Lambda): Lambda =
// get absolute dfs position
val position = Position(
Location.locationToAbsolutePosition(FindFirst(Strategy.containsUserFun), lambda, bfs = false),
bfs = false

// fuse as many maps as possible at THAT position (CodeGenNormalForm fuses way too much here)
CountingRepeat(i => Apply(FusionRules.mapFusion, increasePosition(position, i))) >>
// find first is not precise enough, works for now though
Apply(rule, FindFirst(Strategy.applicable(rule))) >>
$$ lambda
\end{lstlisting}

The rewrite normal form allows us to reason about the relationship of any two adjacent primitives composed using function compositon ($f \circ g$).
If an expression is in rewrite-normalform, $f$ (and $g$) can only either have one of two forms:
Either $f$ \emph{one} of the primitives described in ... (lift primtives), or $f$ is one of these primitives but additionally wrapped in an arbitrary number of maps.
Crucially, $f$ can never have the form $f = *(f_1 \circ f_2)$.
By exploiting the rewrite-normalform, we make sure that we can use a small (minimal?) number of rewrite rules to do so.
These, we call movement rules.
Describe valid rewrites between two adjacent Lift-primitives

\subsection{Domain-specific Optimization Strategies}
\begin{enumerate}
\item Algorithmic: computational (map-reduce-fusion, tree-based-reduction)
\item Algorithmic: data-layout (tiling, overlapped-tiling)
\item Hardware-specific: memory (exploit locality using shared memory)
\item Hardware-specific: parallelism (mapping of computation to the parallel thread hierarchy)
\end{enumerate}

\subsubsection{Data Layout Strategies}
Why tiling? Actually our most important reason to apply tiling is to divide the input into pieces which we can assign to the parallel compute hierarchy.
In addition, some applications benefit from tiling when locality can be exploited in some form.
For a point-wise operation for example, we won't see any locality benefits as every input element is only used once, however we still need to apply tiling to assign work to workgroups warps and threads.
For stencil computations, we are able to exploit locality, however the effectivness depends on the shape of the stencil.

Our generic tiling strategy is composed out of three (maybe two?) parts:
\begin{enumerate}
\item split-join rule in every dimension, "tile" every dimension one after each other, corresponds to traditional loop blocking for every for-loop.
\item (Restore rewrite normal form) - we might not want to count this as a "step" because we might need to do that anyhow when we reformulate movement rules as strategies too.
\item rearrange dimensions such that the created tile dimensions are innermost. visualize and show for loops
\end{enumerate}

%\begin{lstlisting}[style=Elevate, language=Lift, caption=code for tiling examples, float]
%def stencil9pt = \( [[Float]@$_M$@]@$_N$@], input =>
%    map(map(f) o                                            // apply stencil function
%      transpose o slide(3,1) o map(slide(3,1) @\$@ input)   // create 9-pt neighborhoods
%// use this short notation?
%// before tiling
%def stencil9pt =
%\( [[Float]@$_M$@]@$_N$@], xs => **f o T o S o *S @\$@ xs)
%// after step 1 and 2
%\( [[Float]@$_M$@]@$_N$@], xs => J o **J o ****f **Split o Split o T o S o *S @\$@ xs)
%// after step 3
%\( [[Float]@$_M$@]@$_N$@], xs => J o **J o *T o ****f o T o **Split o Split o T o S o *S @\$@ xs)
%// now overlapped tiling...

\subsubsection{Parallelism Mapping Strategies}
Can we somehow refer to Futharks PPoPP'19 paper? Essentially these strategies do what they describe in their whole paper.

In order to generate high-performance programs, we need to efficiently map computation to the compute hierarchy of the targeted architecture.
GPUs for example, have a deeply nested compute hierarchy consisting of 3 levels: Blocks, Warps and Threads.
Each of these levels are arranged in up to 3 dimension providing unique ID's in the OpenCL programming model, e.g., \texttt{threadIdx.x} (this is cuda).
The warp-level is special as it is not explicitly exposed at OpenCL's programming model, however, high-performance implementations of GPU algorithms need to optimize for this particular level as well to achieve the best possible performance.

In Lift, we use low-level map primitives to decide which computation is mapped to which level and dimension of the compute hierarchy.
Figure~\ref{fig:lowLevelMaps} shows the valid nestings of Lift low-level map primitives.

Somehow visualize compute-hierarchy and how we map dimensions of our application to this hierarchy. Maybe use figure we had in PSI paper

\begin{figure}
\includegraphics[width=\linewidth]{img/lowLevelMap}
\caption{Valid nestings of low-level map primitives: modify this to show three OpenCL dimensions as well. Maybe highlight paths to visualize parallelism strategies: i.e. global0 = * $\rightarrow$ mapGlobal0 $\rightarrow$ mapSeq}
\label{fig:lowLevelMaps}
\end{figure}
\begin{lstlisting}[style=Elevate, caption=we probably want to use equations rather than listings?, float]
// forward-style
def global01 =
normalize(mapFusion) >>
apply(mapGlb(0), FindFirst(applicable(mapGlb))) >>
apply(mapGlb(1), FindFirst(applicable(mapGlb))) >>

// function-compositon
def global(inner: Int, outer: Int) =
normalize(mapSeq) o
apply(mapGlb(inner), FindFirst(applicable(mapGlb))) o
apply(@\color{solarized-magenta}{\textbf mapGlb}@(outer), FindFirst(applicable(mapGlb))) o

def mapParallelism = (group10 +> global10 +> global0)
\end{lstlisting}

% \begin{definition}
%   A rewrite rule is a partial function mapping a \Lift \texttt{Expr} to a \texttt{Expr}.
%   Rewrite rules have the following type signature: $\Expr \pfun \Expr$
% \end{definition}

% \begin{figure}[t]

% \newcommand{\phrasetype}{\mathsf{phrase}}
% \newcommand{\passivetype}{\mathsf{passive}}
% \newcommand{\datatype}{\mathsf{data}}
% \newcommand{\natkind}{\mathsf{nat}}
% \newcommand{\vwkind}{\mathsf{width}}
% % \newcommand{\num}{\mathsf{num}}
% \newcommand{\sem}[1]{\llbracket #1 \rrbracket}
% \newcommand{\interfere}{\mathrel\triangledown}
% \newcommand{\indep}{\mathrel\triangle}
% \newcommand{\objspace}{\mathord{\dagger}}

% \newcommand{\kw}[1]{\mathrm{#1}}

% \newcommand{\tycomm}{\mathsf{comm}}
% \newcommand{\tyexp}{\mathsf{exp}}
% \newcommand{\tyacc}{\mathsf{acc}}
% \newcommand{\tyvar}{\mathsf{var}}

% \newcommand{\pureto}{\to_{\textrm{p}}}

% \newcommand{\ty}{\mathsf{Type}}
% \newcommand{\LiftExpr}{\mathsf{LiftExpr}}

%   % \begin{figure}[t]

%   %   % \begin{minipage}{.8\linewidth}
%   %   %   \fbox{$\vdash T$}
%   %   %   \begin{mathpar}
%   %   %     \inferrule*
%   %   %     { }
%   %   %     {\vdash \LiftExpr}

%   %   %     \inferrule*
%   %   %     {\vdash T \and \vdash U}
%   %   %     {\vdash T \rightarrow U}
%   %   %   \end{mathpar}

%   %   %   \label{types}
%   %   %   \caption{Well formed types}
%   %   % \end{minipage}

%   %   \medskip

%   %   % \begin{minipage}{.8\linewidth}
%   %   %   \fbox{$\Gamma \vdash t : T$}
%   %   %   \begin{mathpar}
%   %   %     \inferrule*
%   %   %     {x : T \in \Gamma}
%   %   %     {\Gamma \vdash x : T}

%   %   %     \inferrule*
%   %   %     {\Gamma, x : T \vdash t : U}
%   %   %     {\Gamma \vdash \lambda x : T . t : T \rightarrow U}

%   %   %     \inferrule*
%   %   %     {\Gamma \vdash f : T \rightarrow U \and \Gamma \vdash t : T}
%   %   %     {\Gamma \vdash f\ t : U}

%   %   %     % \inferrule*
%   %   %     % {}
%   %   %     % {\Gamma \vdash \mathsf{error} : T}
%   %   %   \end{mathpar}
%   %   %   \label{terms}
%   %   %   \caption{Well typed terms}
%   %   % \end{minipage}

%   % \end{figure}

%   \begin{figure}

%     \begin{minipage}{.8\textwidth}
%       \begin{eqnarray*}
%       Rule &=& \LiftExpr \rightarrow \LiftExpr \qquad \text{(partial function vs. exceptions?)} \\
%       Strategy &=& \LiftExpr \rightarrow \LiftExpr\\
%       Location &=& Position(Int) | AtExpr(\LiftExpr) | FindFirst(\LiftExpr \rightarrow \mathsf{bool})\\
%       \\
%       isDefined &:& Rule \rightarrow \LiftExpr \rightarrow \mathsf{bool}\\
%       isDefined &=& \lambda r . \lambda e~.~\mathsf{try}~((r~e); \mathsf{true})~\mathsf{catch}~\mathsf{false} \\
%       id &:& Strategy\\
%       id &=& \lambda e~.~e\\
%       applyAt &:& Rule \rightarrow Location \rightarrow Strategy\\
%       applyAt &=& \ldots\\
%       lChoice &:& Strategy \rightarrow Strategy \rightarrow Strategy\\
%       lChoice &=& \lambda f . \lambda s . \lambda e~.~\mathsf{try}~(f~e)~\mathsf{catch}~(s~e)\\
%       try &:& Strategy \rightarrow Strategy\\
%       try &=& \lambda s . lChoice~s~id\\
%       seq &:& Strategy \rightarrow Strategy \rightarrow Strategy\\
%       seq &=& \lambda f . \lambda s . \lambda e~.~s~(f~e)\\
%       repeat &:& Strategy \rightarrow Strategy\\
%       repeat &=& \lambda s~.~try~(s~;~(repeat~s))\\
%       normalize &:& Rule \rightarrow Strategy\\
%       normalize &=& \lambda r~.~repeat~(applyAt~r~(FindFirst~(isDefined~rule)))\\
%       rewriteNormalForm &:& Strategy\\
%       rewriteNormalForm &=& normalize~mapFissionRule \qquad \text{// } map(f~o~g) \mapsto map(f)~o~map(g)\\
%       codeGenNormalForm &:& Strategy\\
%       codeGenNormalForm &=& normalize~mapFusionRule \qquad \text{// } map(f)~o~map(g) \mapsto map(f~o~g)\\
%       listPotentialRewrites &:& Rule \rightarrow \LiftExpr \rightarrow List[(Rule, Location)]\\
%       listPotentialRewrites &=& \ldots\\
%       foldLeft &:& List[(Rule, Location)] \rightarrow (\LiftExpr, (Rule, Location)) \rightarrow \LiftExpr) \rightarrow Strategy\\
%       foldLeft &=& \lambda list~.~\lambda~f~.~\lambda~e~list~match~\{\\
%         & & \quad case~Nil~=>~e\\
%         & & \quad case~(r, l)~::~rest~=>~foldLeft~rest~f~( f(e, (r, l)) )\\
%         &&\}\\
%       tiling &:& \mathsf{int} \rightarrow Strategy\\
%       tiling &=& \lambda size~.~\lambda~e.~\\
%         &&\quad foldLeft~(listPotentialRewrites~(splitJoin~size)~e)~(\lambda~(e, (r, l)).\\
%         &&\qquad try~(applyAt~r~l)~e) ; \\
%         &&\quad rewriteNormalForm ; \\
%         &&\quad interleaveDimensions~(numberOfTiledDimensions~e)
%       \end{eqnarray*}
%     \end{minipage}

%   \end{figure}

% \end{figure}

%% Acknowledgments
\begin{acks}                            %% acks environment is optional
%% contents suppressed with 'anonymous'
%% Commands \grantsponsor{<sponsorID>}{<name>}{<url>} and
%% \grantnum[<url>]{<sponsorID>}{<number>} should be used to
%% acknowledge financial support and will be used by metadata
%% extraction tools.
% This material is based upon work supported by the
% \grantsponsor{GS100000001}{National Science
%   Foundation}{http://dx.doi.org/10.13039/100000001} under Grant
% No.~\grantnum{GS100000001}{nnnnnnn} and Grant
% No.~\grantnum{GS100000001}{mmmmmmm}.  Any opinions, findings, and
% conclusions or recommendations expressed in this material are those
% of the author and do not necessarily reflect the views of the
% National Science Foundation.

We would like to thank the entire \Rise (rise-lang.org) and \Elevate (elevate-lang.org) teams for their development efforts.
The first author was financially supported by an Nvidia Research Fellowship.
\end{acks}

\balance
%% Bibliography
%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\begin{thebibliography}{43}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[\protect\citeauthoryear{Abadi, Agarwal, Barham, Brevdo, Chen, Citro,
Corrado, Davis, Dean, Devin, Ghemawat, Goodfellow, Harp, Irving, Isard, Jia,
Jozefowicz, Kaiser, Kudlur, Levenberg, Man\'{e}, Monga, Moore, Murray, Olah,
Schuster, Shlens, Steiner, Sutskever, Talwar, Tucker, Vanhoucke, Vasudevan,
Vi\'{e}gas, Vinyals, Warden, Wattenberg, Wicke, Yu, and Zheng}{Abadi
\bibfield{author}{\bibinfo{person}{Mart\'{\i}n Abadi}, \bibinfo{person}{Ashish
Agarwal}, \bibinfo{person}{Paul Barham}, \bibinfo{person}{Eugene Brevdo},
\bibinfo{person}{Zhifeng Chen}, \bibinfo{person}{Craig Citro},
\bibinfo{person}{Greg~S. Corrado}, \bibinfo{person}{Andy Davis},
\bibinfo{person}{Jeffrey Dean}, \bibinfo{person}{Matthieu Devin},
\bibinfo{person}{Sanjay Ghemawat}, \bibinfo{person}{Ian Goodfellow},
\bibinfo{person}{Andrew Harp}, \bibinfo{person}{Geoffrey Irving},
\bibinfo{person}{Michael Isard}, \bibinfo{person}{Yangqing Jia},
\bibinfo{person}{Rafal Jozefowicz}, \bibinfo{person}{Lukasz Kaiser},
\bibinfo{person}{Manjunath Kudlur}, \bibinfo{person}{Josh Levenberg},
\bibinfo{person}{Dandelion Man\'{e}}, \bibinfo{person}{Rajat Monga},
\bibinfo{person}{Sherry Moore}, \bibinfo{person}{Derek Murray},
\bibinfo{person}{Chris Olah}, \bibinfo{person}{Mike Schuster},
\bibinfo{person}{Jonathon Shlens}, \bibinfo{person}{Benoit Steiner},
\bibinfo{person}{Ilya Sutskever}, \bibinfo{person}{Kunal Talwar},
\bibinfo{person}{Paul Tucker}, \bibinfo{person}{Vincent Vanhoucke},
\bibinfo{person}{Vijay Vasudevan}, \bibinfo{person}{Fernanda Vi\'{e}gas},
\bibinfo{person}{Oriol Vinyals}, \bibinfo{person}{Pete Warden},
\bibinfo{person}{Martin Wattenberg}, \bibinfo{person}{Martin Wicke},
\bibinfo{person}{Yuan Yu}, {and} \bibinfo{person}{Xiaoqiang Zheng}.}
\bibinfo{year}{2015}\natexlab{}.
\newblock \bibinfo{title}{{TensorFlow}: Large-Scale Machine Learning on
Heterogeneous Systems}.
\newblock
\newblock
\urldef\tempurl%
\url{https://www.tensorflow.org/}
\showURL{%
\tempurl}
\newblock
\shownote{Software available from tensorflow.org.}

\bibitem[\protect\citeauthoryear{Andrei, Fern{\'{a}}ndez, Kirchner,
Melan{\c{c}}on, Namet, and Pinaud}{Andrei et~al\mbox{.}}{2011}]%
\bibfield{author}{\bibinfo{person}{Oana Andrei}, \bibinfo{person}{Maribel
Fern{\'{a}}ndez}, \bibinfo{person}{H{\'{e}}l{\`{e}}ne Kirchner},
\bibinfo{person}{Guy Melan{\c{c}}on}, \bibinfo{person}{Olivier Namet}, {and}
\bibinfo{person}{Bruno Pinaud}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{{PORGY:} Strategy-Driven Interactive Transformation
of Graphs}. In \bibinfo{booktitle}{\emph{Proceedings 6th International
Workshop on Computing with Terms and Graphs, {TERMGRAPH} 2011,
Saarbr{\"{u}}cken, Germany, 2nd April 2011.}} \bibinfo{pages}{54--68}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.4204/EPTCS.48.7}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Atkey, Steuwer, Lindley, and Dubach}{Atkey
\bibfield{author}{\bibinfo{person}{Robert Atkey}, \bibinfo{person}{Michel
Steuwer}, \bibinfo{person}{Sam Lindley}, {and} \bibinfo{person}{Christophe
Dubach}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Strategy Preserving Compilation for Parallel
Functional Code}.
\newblock \bibinfo{journal}{\emph{CoRR}}  \bibinfo{volume}{abs/1710.08332}
\newblock

\bibitem[\protect\citeauthoryear{Baghdadi, Ray, Romdhane, Sozzo, Akkas, Zhang,
Suriana, Kamil, and Amarasinghe}{Baghdadi et~al\mbox{.}}{2019}]%
\bibfield{author}{\bibinfo{person}{Riyadh Baghdadi}, \bibinfo{person}{Jessica
Ray}, \bibinfo{person}{Malek~Ben Romdhane}, \bibinfo{person}{Emanuele~Del
Sozzo}, \bibinfo{person}{Abdurrahman Akkas}, \bibinfo{person}{Yunming Zhang},
\bibinfo{person}{Patricia Suriana}, \bibinfo{person}{Shoaib Kamil}, {and}
\bibinfo{person}{Saman~P. Amarasinghe}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Tiramisu: {A} Polyhedral Compiler for Expressing
Fast and Portable Code}. In \bibinfo{booktitle}{\emph{{IEEE/ACM}
International Symposium on Code Generation and Optimization, {CGO} 2019,
Washington, DC, USA, February 16-20, 2019}}. \bibinfo{pages}{193--205}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1109/CGO.2019.8661197}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Barham and Isard}{Barham and Isard}{2019}]%
\bibfield{author}{\bibinfo{person}{Paul Barham} {and} \bibinfo{person}{Michael
Isard}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Machine Learning Systems are Stuck in a Rut}. In
\bibinfo{booktitle}{\emph{HotOS}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{177--183}.
\newblock

\bibitem[\protect\citeauthoryear{Bird and de~Moor}{Bird and de~Moor}{1997}]%
\bibfield{author}{\bibinfo{person}{Richard Bird} {and} \bibinfo{person}{Oege de
Moor}.} \bibinfo{year}{1997}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Algebra of Programming}}.
\newblock \bibinfo{publisher}{Prentice-Hall, Inc.}, \bibinfo{address}{Upper
Saddle River, NJ, USA}.
\newblock
\showISBNx{0-13-507245-X}

\bibitem[\protect\citeauthoryear{Borovansk{\'{y}}, Kirchner, Kirchner, Moreau,
and Ringeissen}{Borovansk{\'{y}} et~al\mbox{.}}{1998}]%
\bibfield{author}{\bibinfo{person}{Peter Borovansk{\'{y}}},
\bibinfo{person}{Claude Kirchner}, \bibinfo{person}{H{\'{e}}l{\`{e}}ne
Kirchner}, \bibinfo{person}{Pierre{-}Etienne Moreau}, {and}
\bibinfo{person}{Christophe Ringeissen}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{An overview of {ELAN}}.
\newblock \bibinfo{journal}{\emph{Electr. Notes Theor. Comput. Sci.}}
\bibinfo{volume}{15} (\bibinfo{year}{1998}), \bibinfo{pages}{55--70}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/S1571-0661(05)82552-6}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Borovansk{\'{y}}, Kirchner, Kirchner, Moreau,
and Vittek}{Borovansk{\'{y}} et~al\mbox{.}}{1996}]%
\bibfield{author}{\bibinfo{person}{Peter Borovansk{\'{y}}},
\bibinfo{person}{Claude Kirchner}, \bibinfo{person}{H{\'{e}}l{\`{e}}ne
Kirchner}, \bibinfo{person}{Pierre{-}Etienne Moreau}, {and}
\bibinfo{person}{Marian Vittek}.} \bibinfo{year}{1996}\natexlab{}.
\newblock \showarticletitle{{ELAN:} {A} logical framework based on
computational systems}.
\newblock \bibinfo{journal}{\emph{Electr. Notes Theor. Comput. Sci.}}
\bibinfo{volume}{4} (\bibinfo{year}{1996}), \bibinfo{pages}{35--50}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/S1571-0661(04)00032-5}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Boyle, Harmer, and Winter}{Boyle
\bibfield{author}{\bibinfo{person}{James~M Boyle}, \bibinfo{person}{Terence~J
Harmer}, {and} \bibinfo{person}{Victor~L Winter}.}
\bibinfo{year}{1997}\natexlab{}.
\newblock \showarticletitle{The TAMPR program transformation system:
Simplifying the development of numerical software}.
\newblock In \bibinfo{booktitle}{\emph{Modern software tools for scientific
computing}}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{353--372}.
\newblock

\bibitem[\protect\citeauthoryear{Bravenboer and Visser}{Bravenboer and
\bibfield{author}{\bibinfo{person}{Martin Bravenboer} {and}
\bibinfo{person}{Eelco Visser}.} \bibinfo{year}{2002}\natexlab{}.
\newblock \showarticletitle{Rewriting Strategies for Instruction Selection}. In
\bibinfo{booktitle}{\emph{Rewriting Techniques and Applications, 13th
International Conference, {RTA} 2002, Copenhagen, Denmark, July 22-24, 2002,
Proceedings}}. \bibinfo{pages}{237--251}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/3-540-45610-4\_17}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Chen, Chame, and Hall}{Chen
\bibfield{author}{\bibinfo{person}{Chun Chen}, \bibinfo{person}{Jacqueline
Chame}, {and} \bibinfo{person}{Mary Hall}.} \bibinfo{year}{2008}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{CHiLL: A framework for composing high-level
loop transformations}}.
\newblock \bibinfo{type}{{T}echnical {R}eport}.
\bibinfo{institution}{Citeseer}.
\newblock

\bibitem[\protect\citeauthoryear{Chen, Moreau, Jiang, Zheng, Yan, Shen, Cowan,
Wang, Hu, Ceze, Guestrin, and Krishnamurthy}{Chen et~al\mbox{.}}{2018}]%
\bibfield{author}{\bibinfo{person}{Tianqi Chen}, \bibinfo{person}{Thierry
Moreau}, \bibinfo{person}{Ziheng Jiang}, \bibinfo{person}{Lianmin Zheng},
\bibinfo{person}{Eddie~Q. Yan}, \bibinfo{person}{Haichen Shen},
\bibinfo{person}{Meghan Cowan}, \bibinfo{person}{Leyuan Wang},
\bibinfo{person}{Yuwei Hu}, \bibinfo{person}{Luis Ceze},
\bibinfo{person}{Carlos Guestrin}, {and} \bibinfo{person}{Arvind
Krishnamurthy}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{{TVM:} An Automated End-to-End Optimizing Compiler
for Deep Learning}. In \bibinfo{booktitle}{\emph{13th {USENIX} Symposium on
Operating Systems Design and Implementation, {OSDI} 2018, Carlsbad, CA, USA,
October 8-10, 2018}}. \bibinfo{pages}{578--594}.
\newblock
\urldef\tempurl%
\url{https://www.usenix.org/conference/osdi18/presentation/chen}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Chikofsky and II}{Chikofsky and II}{1990}]%
\bibfield{author}{\bibinfo{person}{Elliot~J. Chikofsky} {and}
\bibinfo{person}{James H.~Cross II}.} \bibinfo{year}{1990}\natexlab{}.
\newblock \showarticletitle{Reverse Engineering and Design Recovery: {A}
\newblock \bibinfo{journal}{\emph{{IEEE} Software}} \bibinfo{volume}{7},
\bibinfo{number}{1} (\bibinfo{year}{1990}), \bibinfo{pages}{13--17}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1109/52.43044}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Clavel, Dur{\'{a}}n, Eker, Lincoln,
Mart{\'{\i}}{-}Oliet, Meseguer, and Quesada}{Clavel et~al\mbox{.}}{2002}]%
\bibfield{author}{\bibinfo{person}{Manuel Clavel}, \bibinfo{person}{Francisco
Dur{\'{a}}n}, \bibinfo{person}{Steven Eker}, \bibinfo{person}{Patrick
Lincoln}, \bibinfo{person}{Narciso Mart{\'{\i}}{-}Oliet},
\bibinfo{person}{Jos{\'{e}} Meseguer}, {and} \bibinfo{person}{Jose~F.
Quesada}.} \bibinfo{year}{2002}\natexlab{}.
\newblock \showarticletitle{Maude: specification and programming in rewriting
\newblock \bibinfo{journal}{\emph{Theor. Comput. Sci.}} \bibinfo{volume}{285},
\bibinfo{number}{2} (\bibinfo{year}{2002}), \bibinfo{pages}{187--243}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/S0304-3975(01)00359-0}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Collberg, Thomborson, and Low}{Collberg
\bibfield{author}{\bibinfo{person}{Christian~S. Collberg},
\bibinfo{person}{Clark~D. Thomborson}, {and} \bibinfo{person}{Douglas Low}.}
\bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Manufacturing Cheap, Resilient, and Stealthy Opaque
Constructs}. In \bibinfo{booktitle}{\emph{{POPL} '98, Proceedings of the 25th
{ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, San
Diego, CA, USA, January 19-21, 1998}}. \bibinfo{pages}{184--196}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/268946.268962}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Dolstra and Visser}{Dolstra and
\bibfield{author}{\bibinfo{person}{Eelco Dolstra} {and} \bibinfo{person}{Eelco
Visser}.} \bibinfo{year}{2002}\natexlab{}.
\newblock \showarticletitle{Building Interpreters with Rewriting Strategies}.
\newblock \bibinfo{journal}{\emph{Electr. Notes Theor. Comput. Sci.}}
\bibinfo{volume}{65}, \bibinfo{number}{3} (\bibinfo{year}{2002}),
\bibinfo{pages}{57--76}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/S1571-0661(04)80427-4}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Fern{\'{a}}ndez, Kirchner, and
Namet}{Fern{\'{a}}ndez et~al\mbox{.}}{2011}]%
\bibfield{author}{\bibinfo{person}{Maribel Fern{\'{a}}ndez},
\bibinfo{person}{H{\'{e}}l{\`{e}}ne Kirchner}, {and} \bibinfo{person}{Olivier
Namet}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{A Strategy Language for Graph Rewriting}. In
\bibinfo{booktitle}{\emph{Logic-Based Program Synthesis and Transformation -
21st International Symposium, {LOPSTR} 2011, Odense, Denmark, July 18-20,
2011. Revised Selected Papers}}. \bibinfo{pages}{173--188}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-32211-2\_12}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Fowler}{Fowler}{1999}]%
\bibfield{author}{\bibinfo{person}{Martin Fowler}.}
\bibinfo{year}{1999}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Refactoring - Improving the Design of
Existing Code}}.
\newblock \bibinfo{publisher}{Addison-Wesley}.
\newblock
\showISBNx{978-0-201-48567-7}
\urldef\tempurl%
\url{http://martinfowler.com/books/refactoring.html}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Girbal, Vasilache, Bastoul, Cohen, Parello,
Sigler, and Temam}{Girbal et~al\mbox{.}}{2006}]%
\bibfield{author}{\bibinfo{person}{Sylvain Girbal}, \bibinfo{person}{Nicolas
Vasilache}, \bibinfo{person}{C{\'{e}}dric Bastoul}, \bibinfo{person}{Albert
Cohen}, \bibinfo{person}{David Parello}, \bibinfo{person}{Marc Sigler}, {and}
\bibinfo{person}{Olivier Temam}.} \bibinfo{year}{2006}\natexlab{}.
\newblock \showarticletitle{Semi-Automatic Composition of Loop Transformations
for Deep Parallelism and Memory Hierarchies}.
\newblock \bibinfo{journal}{\emph{International Journal of Parallel
Programming}} \bibinfo{volume}{34}, \bibinfo{number}{3}
(\bibinfo{year}{2006}), \bibinfo{pages}{261--317}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/s10766-006-0012-3}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Goguen, Kirchner, Kirchner, M{\'{e}}grelis,
Meseguer, and Winkler}{Goguen et~al\mbox{.}}{1987}]%
\bibfield{author}{\bibinfo{person}{Joseph~A. Goguen}, \bibinfo{person}{Claude
Kirchner}, \bibinfo{person}{H{\'{e}}l{\`{e}}ne Kirchner},
\bibinfo{person}{Aristide M{\'{e}}grelis}, \bibinfo{person}{Jos{\'{e}}
Meseguer}, {and} \bibinfo{person}{Timothy~C. Winkler}.}
\bibinfo{year}{1987}\natexlab{}.
\newblock \showarticletitle{An Introduction to {OBJ} 3}. In
\bibinfo{booktitle}{\emph{Conditional Term Rewriting Systems, 1st
International Workshop, Orsay, France, July 8-10, 1987, Proceedings}}.
\bibinfo{pages}{258--263}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/3-540-19242-5\_22}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hagedorn, Stoltzfus, Steuwer, Gorlatch, and
Dubach}{Hagedorn et~al\mbox{.}}{2018}]%
\bibfield{author}{\bibinfo{person}{Bastian Hagedorn}, \bibinfo{person}{Larisa
Stoltzfus}, \bibinfo{person}{Michel Steuwer}, \bibinfo{person}{Sergei
Gorlatch}, {and} \bibinfo{person}{Christophe Dubach}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{High performance stencil code generation with
lift}. In \bibinfo{booktitle}{\emph{Proceedings of the 2018 International
Symposium on Code Generation and Optimization, {CGO} 2018, V{\"{o}}sendorf /
Vienna, Austria, February 24-28, 2018}}. \bibinfo{pages}{100--112}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3168824}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Hall, Chame, Chen, Shin, Rudy, and Khan}{Hall
\bibfield{author}{\bibinfo{person}{Mary Hall}, \bibinfo{person}{Jacqueline
Chame}, \bibinfo{person}{Chun Chen}, \bibinfo{person}{Jaewook Shin},
\bibinfo{person}{Gabe Rudy}, {and} \bibinfo{person}{Malik~Murtaza Khan}.}
\bibinfo{year}{2009}\natexlab{}.
\newblock \showarticletitle{Loop transformation recipes for code generation and
auto-tuning}. In \bibinfo{booktitle}{\emph{International Workshop on
Languages and Compilers for Parallel Computing}}. Springer,
\bibinfo{pages}{50--64}.
\newblock

\bibitem[\protect\citeauthoryear{Hennessy and Patterson}{Hennessy and
\bibfield{author}{\bibinfo{person}{John~L. Hennessy} {and}
\bibinfo{person}{David~A. Patterson}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{A new golden age for computer architecture}.
\newblock \bibinfo{journal}{\emph{Commun. {ACM}}} \bibinfo{volume}{62},
\bibinfo{number}{2} (\bibinfo{year}{2019}), \bibinfo{pages}{48--60}.
\newblock

\bibitem[\protect\citeauthoryear{Kirchner}{Kirchner}{2015}]%
\bibfield{author}{\bibinfo{person}{H{\'{e}}l{\`{e}}ne Kirchner}.}
\bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Rewriting Strategies and Strategic Rewrite
Programs}. In \bibinfo{booktitle}{\emph{Logic, Rewriting, and Concurrency -
Essays dedicated to Jos{\'{e}} Meseguer on the Occasion of His 65th
Birthday}}. \bibinfo{pages}{380--403}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-23165-5\_18}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Luttik, Visser, et~al\mbox{.}}{Luttik
\bibfield{author}{\bibinfo{person}{Sebastiaan~Pascal Luttik},
\bibinfo{person}{Eelco Visser}, {et~al\mbox{.}}}
\bibinfo{year}{1997}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Specification of rewriting strategies}}.
\newblock \bibinfo{publisher}{Universiteit van Amsterdam. Programming Research
\newblock

\bibitem[\protect\citeauthoryear{Olmos and Visser}{Olmos and Visser}{2002}]%
\bibfield{author}{\bibinfo{person}{Karina Olmos} {and} \bibinfo{person}{Eelco
Visser}.} \bibinfo{year}{2002}\natexlab{}.
\newblock \showarticletitle{Strategies for Source-to-Source Constant
\newblock \bibinfo{journal}{\emph{Electr. Notes Theor. Comput. Sci.}}
\bibinfo{volume}{70}, \bibinfo{number}{6} (\bibinfo{year}{2002}),
\bibinfo{pages}{156--175}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/S1571-0661(04)80605-4}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Paszke, Gross, Chintala, Chanan, Yang, DeVito,
Lin, Desmaison, Antiga, and Lerer}{Paszke et~al\mbox{.}}{2017}]%
\bibfield{author}{\bibinfo{person}{Adam Paszke}, \bibinfo{person}{Sam Gross},
\bibinfo{person}{Soumith Chintala}, \bibinfo{person}{Gregory Chanan},
\bibinfo{person}{Edward Yang}, \bibinfo{person}{Zachary DeVito},
\bibinfo{person}{Zeming Lin}, \bibinfo{person}{Alban Desmaison},
\bibinfo{person}{Luca Antiga}, {and} \bibinfo{person}{Adam Lerer}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Automatic differentiation in PyTorch}.
\newblock  (\bibinfo{year}{2017}).
\newblock

\bibitem[\protect\citeauthoryear{Peyton~Jones, Tolmach, and Hoare}{Peyton~Jones
\bibfield{author}{\bibinfo{person}{Simon Peyton~Jones}, \bibinfo{person}{Andrew
Tolmach}, {and} \bibinfo{person}{Tony Hoare}.}
\bibinfo{year}{2001}\natexlab{}.
\newblock \showarticletitle{Playing by the rules: rewriting as a practical
optimisation technique in GHC}. In \bibinfo{booktitle}{\emph{2001 Haskell
Workshop} (\bibinfo{edition}{2001 haskell workshop} ed.)}. ACM SIGPLAN.
\newblock

\bibitem[\protect\citeauthoryear{Pinaud, Andrei, Fern{\'{a}}ndez, Kirchner,
Melan{\c{c}}on, and Vallet}{Pinaud et~al\mbox{.}}{2017}]%
\bibfield{author}{\bibinfo{person}{Bruno Pinaud}, \bibinfo{person}{Oana
Andrei}, \bibinfo{person}{Maribel Fern{\'{a}}ndez},
\bibinfo{person}{H{\'{e}}l{\`{e}}ne Kirchner}, \bibinfo{person}{Guy
Melan{\c{c}}on}, {and} \bibinfo{person}{Jason Vallet}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{{PORGY} : a Visual Analytics Platform for System
Modelling and Analysis Based on Graph Rewriting}. In
\bibinfo{booktitle}{\emph{17{\`{e}}me Journ{\'{e}}es Francophones Extraction
et Gestion des Connaissances, {EGC} 2017, 24-27 Janvier 2017, Grenoble,
France}}. \bibinfo{pages}{473--476}.
\newblock
\urldef\tempurl%
\url{http://editions-rnti.fr/?inprocid=1002327}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Ragan{-}Kelley, Adams, Sharlet, Barnes, Paris,
Levoy, Amarasinghe, and Durand}{Ragan{-}Kelley et~al\mbox{.}}{2018}]%
\bibfield{author}{\bibinfo{person}{Jonathan Ragan{-}Kelley},
\bibinfo{person}{Andrew Adams}, \bibinfo{person}{Dillon Sharlet},
\bibinfo{person}{Connelly Barnes}, \bibinfo{person}{Sylvain Paris},
\bibinfo{person}{Marc Levoy}, \bibinfo{person}{Saman~P. Amarasinghe}, {and}
\bibinfo{person}{Fr{\'{e}}do Durand}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Halide: decoupling algorithms from schedules for
high-performance image processing}.
\newblock \bibinfo{journal}{\emph{Commun. {ACM}}} \bibinfo{volume}{61},
\bibinfo{number}{1} (\bibinfo{year}{2018}), \bibinfo{pages}{106--115}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3150211}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Ragan{-}Kelley, Barnes, Adams, Paris, Durand,
and Amarasinghe}{Ragan{-}Kelley et~al\mbox{.}}{2013}]%
\bibfield{author}{\bibinfo{person}{Jonathan Ragan{-}Kelley},
\bibinfo{person}{Connelly Barnes}, \bibinfo{person}{Andrew Adams},
\bibinfo{person}{Sylvain Paris}, \bibinfo{person}{Fr{\'{e}}do Durand}, {and}
\bibinfo{person}{Saman~P. Amarasinghe}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Halide: a language and compiler for optimizing
parallelism, locality, and recomputation in image processing pipelines}. In
\bibinfo{booktitle}{\emph{{PLDI}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{519--530}.
\newblock

\bibitem[\protect\citeauthoryear{Shaikhha, Fitzgibbon, Vytiniotis, and {Peyton
Jones}}{Shaikhha et~al\mbox{.}}{2019}]%
\bibfield{author}{\bibinfo{person}{Amir Shaikhha}, \bibinfo{person}{Andrew
Fitzgibbon}, \bibinfo{person}{Dimitrios Vytiniotis}, {and}
\bibinfo{person}{Simon {Peyton Jones}}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Efficient differentiable programming in a
functional array-processing language}.
\newblock \bibinfo{journal}{\emph{{PACMPL}}} \bibinfo{volume}{3},
\bibinfo{number}{{ICFP}} (\bibinfo{year}{2019}),
\bibinfo{pages}{97:1--97:30}.
\newblock

\bibitem[\protect\citeauthoryear{Steuwer, Fensch, Lindley, and Dubach}{Steuwer
\bibfield{author}{\bibinfo{person}{Michel Steuwer}, \bibinfo{person}{Christian
Fensch}, \bibinfo{person}{Sam Lindley}, {and} \bibinfo{person}{Christophe
Dubach}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Generating performance portable code using rewrite
rules: from high-level functional expressions to high-performance OpenCL
code}. In \bibinfo{booktitle}{\emph{{ICFP}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{205--217}.
\newblock

\bibitem[\protect\citeauthoryear{Steuwer, Remmelg, and Dubach}{Steuwer
\bibfield{author}{\bibinfo{person}{Michel Steuwer}, \bibinfo{person}{Toomas
Remmelg}, {and} \bibinfo{person}{Christophe Dubach}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Matrix multiplication beyond auto-tuning:
rewrite-based {GPU} code generation}. In \bibinfo{booktitle}{\emph{{CASES}}}.
\bibinfo{publisher}{{ACM}}, \bibinfo{pages}{15:1--15:10}.
\newblock

\bibitem[\protect\citeauthoryear{Steuwer, Remmelg, and Dubach}{Steuwer
\bibfield{author}{\bibinfo{person}{Michel Steuwer}, \bibinfo{person}{Toomas
Remmelg}, {and} \bibinfo{person}{Christophe Dubach}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Lift: a functional data-parallel {IR} for
high-performance {GPU} code generation}. In
\bibinfo{booktitle}{\emph{Proceedings of the 2017 International Symposium on
Code Generation and Optimization, {CGO} 2017, Austin, TX, USA, February 4-8,
2017}}. \bibinfo{pages}{74--85}.
\newblock
\urldef\tempurl%
\url{http://dl.acm.org/citation.cfm?id=3049841}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{van~den Brand, van Deursen, Heering, de~Jong,
de~Jonge, Kuipers, Klint, Moonen, Olivier, Scheerder, Vinju, Visser, and
Visser}{van~den Brand et~al\mbox{.}}{2001}]%
\bibfield{author}{\bibinfo{person}{Mark van~den Brand}, \bibinfo{person}{Arie
van Deursen}, \bibinfo{person}{Jan Heering}, \bibinfo{person}{H.~A. de Jong},
\bibinfo{person}{Merijn de Jonge}, \bibinfo{person}{Tobias Kuipers},
\bibinfo{person}{Paul Klint}, \bibinfo{person}{Leon Moonen},
\bibinfo{person}{Pieter~A. Olivier}, \bibinfo{person}{Jeroen Scheerder},
\bibinfo{person}{Jurgen~J. Vinju}, \bibinfo{person}{Eelco Visser}, {and}
\bibinfo{person}{Joost Visser}.} \bibinfo{year}{2001}\natexlab{}.
\newblock \showarticletitle{The {ASF+SDF} Meta-environment: {A} Component-Based