kassertassertstylebasicstyleld kadtadtstylebasicstyleld

# Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection

Ross Daly 0000-0002-4938-5250  Stanford University
Stanford, CA, USA
<EMAIL_ADDRESS>Caleb Donovick 0000-0001-9336-1267  Stanford
University
Stanford, CA, USA
<EMAIL_ADDRESS>Caleb Terrill  Stanford University
Stanford, CA, USA
<EMAIL_ADDRESS>Jackson Melchert 0000-0002-8232-1603  Stanford
University
Stanford, CA, USA
<EMAIL_ADDRESS>Priyanka Raina 0000-0002-8834-8663  Stanford University
Stanford, CA, USA
<EMAIL_ADDRESS>Clark Barrett 0000-0002-9522-3084  Stanford University
Stanford, CA, USA
<EMAIL_ADDRESS>Pat Hanrahan 0000-0002-3474-9752  Stanford University
Stanford, CA, USA
<EMAIL_ADDRESS>
###### Abstract

Compiling programs to an instruction set architecture (ISA) requires a set of
rewrite rules that map patterns consisting of compiler instructions to
patterns consisting of ISA instructions. We synthesize such rules by
constructing SMT queries, whose solutions represent two functionally
equivalent programs. These two programs are interpreted as an instruction
selection rewrite rule. Existing work is limited to single-instruction ISA
patterns, whereas our solution does not have that restriction. Furthermore, we
address inefficiencies of existing work by developing two optimized
algorithms. The first only generates unique rules by preventing synthesis of
duplicate and composite rules. The second only generates lowest-cost rules by
preventing synthesis of higher-cost rules. We evaluate our algorithms on
multiple ISAs. Without our optimizations, the vast majority of synthesized
rewrite rules are either duplicates, composites, or higher cost. Our
optimizations result in synthesis speed-ups of up to 768$\times$ and
4004$\times$ for the two algorithms.

## I

### I-A

##  II Introduction

As we approach the end of Moore’s law and Dennard scaling, drastically
improving computing performance and energy efficiency requires designing
domain-specific hardware architectures (DSAs) or adding domain-specific
extensions to existing architectures [22]. As a result, many DSAs have been
developed in recent years [24, 30, 8, 4, 27], each with its own custom
instruction set architecture (ISA) or ISA extension. Targeting such ISAs from
a compiler’s intermediate representation (IR) requires a custom library of
instruction selection rewrite rules. A rewrite rule is a mapping of an IR
pattern to a functionally equivalent ISA pattern. Manual specification of
rewrite rules is error-prone, time-consuming, and often incomplete. It is
therefore desirable to automatically generate valid rewrite rules. When
specifying instruction selection rewrite rules, there are two common cases.
When ISAs have complex instructions, rewrite rules will often map multi-
instruction IR patterns to a single ISA instruction. When ISAs have simple
instructions, rewrite rules will often map a single IR instruction to a multi-
instruction ISA pattern. A rewrite rule generation tool should be able to
create rewrite rules for both cases. We call such rewrite rules many-to-many
rules. Generating instruction selectors is not a new idea. Most relevant to
this work is Gulwani et al. [21] who use a satisfiability modulo theories
(SMT) solver to synthesize a loop-free program that is functionally equivalent
to a given specification. Their approach is called component-based program
synthesis (CBPS), as each synthesized program must include functional
components from a given component library. Buchwald et al. [6] use and extend
CBPS to efficiently generate multi-instruction loop-free IR programs
equivalent to a single ISA instruction program; that is, they solve the many-
to-one rewrite rules synthesis problem. However, multi-instruction ISA
programs cannot be synthesized. Both of these algorithms produce many
duplicate rules, which are removed during a post-processing step. As we show,
this adds significant additional cost. Another issue is that CBPS as currently
formulated does not incorporate the notion of optimizing for cost. In
practice, we often want only the set of lowest-cost rules, making it
unnecessary (and expensive) to generate equivalent higher-cost rules. This
paper presents an algorithm for automatically generating a complete set of
many-to-many rewrite rules. We address the above issues by preventing the
synthesis of both duplicate and high-cost rules at rule generation time, using
exclusion techniques. As a further optimization, we generate rules in stages
and exclude _composite_ rules, i.e. rules that can be composed of smaller
rules found in previous stages. These ensure we produce a minimal but complete
set of rewrite rules. Compared to previous work, our approach eliminates
unnecessary rules and significantly reduces the time required to produce the
unique necessary ones. Our contributions are as follows:

  * •

We define generalized component-based program synthesis (GCBPS) as the task of
synthesizing two functionally equivalent programs using two component
libraries. We then present an SMT-based synthesis approach inspired by Gulwani
et al. to solve it.

  * •

We present an iterative algorithm $\mathit{genAll}$ to generate all unique
many-to-many rules up to a given size. We identify a set of equivalence
relations for patterns encoded as programs and for rules that map IR programs
to ISA programs. We use these relations to enumerate and exclude duplicate
rules. Furthermore, we directly exclude composite rewrite rules. These result
in up to a 768$\times$ synthesis speed-up.

  * •

We present an algorithm $\mathit{genAll}_{LC}$ which generates only the
lowest-cost rules by incorporating a cost metric in addition to excluding
duplicate and composite rewrite rules. This results in a synthesis speed-up up
to 4004$\times$.

The rest of the paper is organized as follows. Section III discusses
instruction selection, existing rule generation methods, SMT, and program
synthesis. Section IV describes a program synthesis query for generating many-
to-many rules. Section V presents an algorithm for generating only unique
rewrite rules and defines duplicates and composites. Section VI presents an
algorithm for synthesizing only the lowest-cost rules. Section VII evaluates
both algorithms, and Section VIII discusses limitations and further
optimizations.

##  III Background and Related Work

###  III-A Instruction Selection

Instruction selection is the task of translating code in the compiler’s
intermediate representation (IR) to functionally equivalent code for a target
ISA. Typically, a library of rewrite rules is used in instruction selection. A
rewrite rule is a mapping from an IR pattern consisting of IR instructions to
a functionally equivalent ISA pattern consisting of ISA instructions. Such
patterns can be expression trees or directed acyclic graphs (DAGs).
Significant work has been devoted to developing rewrite rule tiling algorithms
to perform instruction selection [19, 16, 17, 29, 12, 1, 15, 14, 5, 26]. For
each rule in the rule library, a tiling algorithm first finds all fragments
from the IR program in which the rule’s IR pattern exactly matches that
fragment. Then, the instruction selector finds a tiling of these matches that
completely covers the basic block and minimizes the total rule cost according
to some cost metric. Simple instruction selectors only handle tree-based IR
patterns, which is inefficient for reused computations. Modern instruction
selectors like LLVM, use DAG-based matching that allows for both a richer
rules and better tiling. Koes et al. [26] describe a similar near-optimal DAG-
based instruction selection algorithm [5]. We want to generate rules that can
be used with such modern instruction selectors.

###  III-B Generating Instruction Selectors

Generating instruction selectors from instruction semantics has been a topic
of research interest [7, 23, 10, 9, 6]. Dias and Ramsey [10] introduce an
algorithm for generating rewrite rules based on a declarative specification of
the ISA. While this solves part of the many-to-many rule task, their work
relies on an existing set of algebraic rewrite rules for synthesizing
semantically equivalent rules. Our work uses SMT for the instruction and
program semantics. However, incorporating certain kinds of algebraic rewrite
rules could be an avenue for future optimizations. Daly et al. [9] propose a
way to synthesize instruction selection rewrite rules from the register-
transfer level (RTL) specification of a processor. Their algorithm requires a
set of pre-specified IR patterns. In contrast, we can efficiently synthesize
rules that consider all possible multi-instruction IR patterns up to a given
size. Their approach for synthesizing complex instruction constants and
handling floating point types could be combined with the approaches in this
paper. The most relevant to this work is the work by Buchwald et al. [6], that
leverages component-based program synthesis to generate rules with multi-
instruction IR patterns and single-instruction ISA patterns. In contrast, our
work synthesizes rules with both multi-instruction IR patterns and multi-
instruction ISA patterns. We additionally prevent the synthesis of duplicate,
composite, and high-cost rewrite rules, unlike any of the above approaches.

###  III-C Program Synthesis and Equivalence

We use SMT-based program synthesis to enumerate a complete set of instruction
selection rewrite rules. In program synthesis enumeration, it is common to
remove equivalent solutions [3]. We use the equivalence relation defined in
Section V-A to determine equivalent rewrite rules. In prior work [2],
observational equivalence (i.e., programs with the same semantics) has been
used for de-duplication [2], however observational equivalence does not take
into account the structure of the program which is essential for rewrite rule
pattern matching.

###  III-D Logical Setting and Notation

We work in the context of many-sorted logic (e.g., [13]), where we assume an
infinite set of variables of each sort. Terms are denoted using non-boldface
symbols (e.g., $X$). Boldface symbols (e.g., $\mathbf{X}$) are used for sets,
tuples, and multisets, whose elements are either terms or other collections of
terms. $\mathbf{Y}:=(Y_{1},...,Y_{N})$ defines a tuple, where $|\mathbf{Y}|=N$
and $Y_{i}$ refers to the $i$-th element. $\mathbf{Z}:=\\{z^{n}\\}$ defines a
multiset, where the multiplicity of element $z$ is $n\in\mathbb{N}$. Both
$\psi$ and $\phi$ are used to denote formulas. $\psi(\mathbf{X})$ is a formula
whose free variables are a subset of $\mathbf{X}$. We use
$\mathcal{M}\vDash\psi(\mathbf{X})$ to denote the _satisfiability_ relation
between the interpretation $\mathcal{M}$ and the formula $\psi$. Assuming
$\mathbf{X}$ is a collection of variables, $\mathcal{M}_{\mathbf{X}}$ denotes
the _assignment_ to those variables induced by $\mathcal{M}$. For an
assignment $\alpha$, we write $\alpha\models\psi(\mathbf{X})$ if
$\mathcal{M}\models\psi(\mathbf{X})$ for every model $\mathcal{M}$ such that
$\mathcal{M}_{\mathbf{X}}=\alpha$.

###  III-E Component-based Program Synthesis

CBPS is a program synthesis task introduced by Gulwani et al. The inputs to
the task are:

  * •

A _specification_
$\mathbf{S}:=(\mathbf{I}^{S},O^{S},\phi_{\mathit{spec}}(\mathbf{I}^{S},O^{S}))$
containing a tuple of input variables $\mathbf{I}^{S}$, a single output
variable $O^{S}$, and a formula $\phi_{\mathit{spec}}(\mathbf{I}^{S},O^{S})$
relating the inputs and the output.

  * •

A _library of components_ (e.g., instructions) $\mathbf{K}$, where the $k$-th
component
$\mathbf{K}_{k}:=(\mathbf{I}_{k},O_{k},\phi_{k}(\mathbf{I}_{k},O_{k}))$
consists of a tuple of input variables $\mathbf{I}_{k}$, a single output
variable $O_{k}$, and a formula $\phi_{k}(\mathbf{I}_{k},O_{k})$ defining the
component’s semantics.

An example component for an addition instruction is shown below using the
theory of bit-vectors, QF_BV, where $\mathit{BV}_{[n]}$ is an n-bit sort.

$((I_{0}:\mathit{BV}_{[16]},I_{1}:\mathit{BV}_{[16]}),O:\mathit{BV}_{[16]},I_{0}+_{[16]}I_{1}=O)$

The task is to synthesize a valid program functionally equivalent to the
specification using each component from $\mathbf{K}$ exactly once. For
notational convenience, we group together the set of all inputs and outputs of
the components:
$\mathbf{W}:=\cup_{(\mathbf{I}_{k},O_{k},\\_)\in\mathbf{K}}\left(O_{k}\cup\left(\cup\mathbf{I}_{k}\right)\right)$.
Gulwani et al. encode the program structure using a _connection constraint_ :
$\phi_{\mathit{conn}}(\mathbf{L},\mathbf{I}^{S},O^{S},\mathbf{W})$. This is a
formula representing how the program inputs ($\mathbf{I}^{S}$) and program
output ($O^{S}$) are connected via the components. The connections are
specified using _location variables_ $\mathbf{L}$. We do not go into the
details of how location variables encode connections (they are in [21]). It is
sufficient for our purposes to know that these are integer variables, and an
assignment to them uniquely determines a way of connecting the components
together into a program. The _program semantics_ $\phi_{\mathit{prog}}$ are
defined as the components’ semantics conjoined with the connection constraint:

$\displaystyle\phi_{prog}(\mathbf{L},\mathbf{I}^{S},O^{S},\mathbf{W}):=$ (1)
$\displaystyle\ \
\left(\bigwedge_{k}\phi_{k}(\mathbf{I}_{k},O_{k})\right)\land\phi_{conn}(\mathbf{L},\mathbf{I}^{S},O^{S},\mathbf{W}).$

They define a verification constraint that holds if a particular program is
both well-formed (specified using a well-formedness constraint
$\psi_{\mathit{wfp}}$) and satisfies the specification $\phi_{\mathit{spec}}$:

$\displaystyle\phi_{\mathit{verif}}:=\psi_{\mathit{wfp}}(\mathbf{L})\wedge\forall\mathbf{I}^{S},O^{S},\mathbf{W}.$
(2) $\displaystyle\ \
\phi_{prog}(\mathbf{L},\mathbf{I}^{S},O^{S},\mathbf{W})\implies\phi_{spec}(\mathbf{I}^{S},O^{S}).$

A _synthesis formula_ $\phi_{\mathit{synth}}$ existentially quantifies
$\mathbf{L}$ in (2):

$\displaystyle\phi_{\mathit{synth}}:=\exists\mathbf{L}.\forall\mathbf{I}^{S},O^{S},\mathbf{W}.$
(3) $\displaystyle\ \
\psi_{\mathit{wfp}}(\mathbf{L})\land\left(\phi_{\mathit{prog}}(\mathbf{L},\mathbf{I}^{S},O^{S},\mathbf{W})\implies\phi_{spec}(\mathbf{I}^{S},O^{S})\right).$

This formula can be solved using a technique called counter-example guided
inductive synthesis (CEGIS). CEGIS solves such exist-forall formulas by
iteratively solving a series of quantifier-free queries and is often more
efficient than trying to solve the quantified query directly. More details are
in [21]. For our purposes, we assume the existence of a CEGIS implementation,
$\mathit{CEGIS}$, which takes an instance of $\phi_{\mathit{synth}}$ and
returns a model $\mathcal{M}$ with the property that
$\mathcal{M}_{\mathbf{L}}\models\phi_{\mathit{verif}}$, from which a program
that is a solution to CBPS can be constructed.

##  IV Component-based Program Synthesis for Many-to-Many Rules

Given the IR and ISA instruction sets ${\mathbf{K}}^{\mathit{IR}}$ and
${\mathbf{K}}^{\mathit{ISA}}$, Buchwald et al. [6] use CBPS to synthesize
rewrite rules. They use a single ISA instruction
${\mathbf{k}}^{\mathit{ISA}}\in{\mathbf{K}}^{\mathit{ISA}}$ for the CBPS
specification and a subset of the IR instructions for the CBPS components. A
solution to the resulting $\phi_{\mathit{synth}}$ formula gives a program
${\mathbf{P}}^{\mathit{IR}}$. If ${\mathbf{P}}^{\mathit{ISA}}$ is the single-
instruction program consisting of ${\mathbf{k}}^{\mathit{ISA}}$, they
interpret the pair $({\mathbf{P}}^{\mathit{IR}},{\mathbf{P}}^{\mathit{ISA}})$
as an instruction selection rewrite rule. However, Buchwald et al.’s solution
is insufficient for generating many-to-many rules, as they cannot synthesize
IR and ISA programs that both contain multiple instructions. Instead, two
functionally equivalent programs need to be synthesized. We first define an
extension to CBPS called generalized component-based program synthesis (GCBPS)
to address this problem. Then we show how to construct a synthesis query whose
solutions represent pairs of functionally equivalent programs.

###  IV-A Generalized Component-based Program Synthesis

We define the GCBPS task as that of synthesizing two programs,
$\mathbf{P}^{a}$ and $\mathbf{P}^{b}$, represented using location variables
${\mathbf{L}}^{a}$ and ${\mathbf{L}}^{b}$, given two sets of components
${\mathbf{K}}^{a}$ and ${\mathbf{K}}^{b}$, two sets of inputs
${\mathbf{I}}^{a},{\mathbf{I}}^{b}$ where
$|{\mathbf{I}}^{a}|=|{\mathbf{I}}^{b}|$, and two outputs $O^{a},O^{b}$ where
the following conditions hold true:

  1. 1.

${\mathbf{P}}^{a}$ uses each component in ${\mathbf{K}}^{a}$ exactly once.

  2. 2.

${\mathbf{P}}^{b}$ uses each component in ${\mathbf{K}}^{b}$ exactly once.

  3. 3.

${\mathbf{P}}^{a}$ is functionally equivalent to ${\mathbf{P}}^{b}$.

###  IV-B Solving GCBPS

We start with the CBPS verification constraint from (2) using components
${\mathbf{K}}^{a}$ (and a corresponding set of inputs and outputs
${\mathbf{W}}^{a}$), but modify it slightly by introducing variables
$({\mathbf{I}}^{a},O^{a})$ that are fresh copies of $(\mathbf{I}^{S},O^{S})$:

$\displaystyle\psi_{\mathit{wfp}}({\mathbf{L}}^{a})\wedge\forall{\mathbf{I}}^{a},O^{a},{\mathbf{W}}^{a},\mathbf{I}^{S},O^{S}.$
(4) $\displaystyle\ \
(\phi^{a}_{prog}({\mathbf{L}}^{a},{\mathbf{I}}^{a},O^{a},{\mathbf{W}}^{a})\land\phi_{spec}(\mathbf{I}^{S},O^{S}))\implies$
$\displaystyle\ \ \left(\left(\wedge_{i}\ I^{a}_{i}=I^{S}_{i}\right)\implies
O^{a}=O^{S}\right).$

Assuming the formulas for both the program and the specification, if their
inputs are the same, their outputs must also be the same. We next replace the
specification program with a different component-based program using
components ${\mathbf{K}}^{b}$ and quantify over that program’s inputs
${\mathbf{I}}^{b}$, output $O^{b}$, and component variables
${\mathbf{W}}^{b}$:

$\displaystyle\phi_{\mathit{verif}}:=\psi_{\mathit{wfp}}({\mathbf{L}}^{a})\wedge\psi_{\mathit{wfp}}({\mathbf{L}}^{b})\wedge\forall{\mathbf{I}}^{a},{\mathbf{I}}^{b},O^{a},O^{b},{\mathbf{W}}^{a},{\mathbf{W}}^{b}.$
(5) $\displaystyle\ \
\left(\phi^{a}_{prog}({\mathbf{L}}^{a},{\mathbf{I}}^{a},O^{a},{\mathbf{W}}^{a})\land\phi^{b}_{prog}({\mathbf{L}}^{b},{\mathbf{I}}^{b},O^{b},{\mathbf{W}}^{b})\right)\\!\\!\implies\\!\\!$
$\displaystyle\ \ \left(\left(\wedge_{i}\
\\!I^{a}_{i}=I^{b}_{i}\right)\\!\\!\implies\\!\\!O^{a}=O^{b}\right).$

This is our generalized verification constraint stating the correctness
criteria for when two component-based programs are semantically equivalent. To
synthesize such a pair of programs, a synthesis formula
$\phi_{\mathit{synth}}$ is defined by existentially quantifying
${\mathbf{L}}^{a}$ and ${\mathbf{L}}^{b}$ in the verification formula (5):

$\displaystyle\phi_{synth}:=\exists{\mathbf{L}}^{a},{\mathbf{L}}^{b}.\forall{\mathbf{I}}^{a},{\mathbf{I}}^{b},O^{a},O^{b},{\mathbf{W}}^{a},{\mathbf{W}}^{b}.$
(6) $\displaystyle\ \
\psi_{wfp}({\mathbf{L}}^{a})\land\psi_{wfp}({\mathbf{L}}^{b})\land$
$\displaystyle\ \
\biggl{(}\left(\phi^{a}_{prog}({\mathbf{L}}^{a},{\mathbf{I}}^{a},O^{a},{\mathbf{W}}^{a})\land\phi^{b}_{prog}({\mathbf{L}}^{b},{\mathbf{I}}^{b},O^{b},{\mathbf{W}}^{b})\right)\implies$
$\displaystyle\ \ \left(\left(\wedge_{i}\ I^{a}_{i}=I^{b}_{i}\right)\implies
O^{a}=O^{b}\right)\biggr{)}.$

As above, we assume that calling $\mathit{CEGIS}$ on $\phi_{\mathit{synth}}$
returns a model $\mathcal{M}$ such that
$\mathcal{M}_{{\mathbf{L}}^{a}\cup{\mathbf{L}}^{b}}\models\phi_{\mathit{verif}}$.
This can be converted into a pair of programs
$({\mathbf{P}}^{a},{\mathbf{P}}^{b})$ representing a rewrite rule that is a
solution for the GCBPS task. We write
$\mathit{rewriteRule}({\mathbf{K}}^{a},{\mathbf{K}}^{b},\mathcal{M}_{{\mathbf{L}}^{a}},\mathcal{M}_{{\mathbf{L}}^{b}})$
for the rewrite rule constructed from a specific model $\mathcal{M}$ using the
component sets ${\mathbf{K}}^{a}$ and ${\mathbf{K}}^{b}$.

##  V Generating All Many-to-Many Rewrite Rules

Buchwald et al. [6] describe an iterative algorithm,
$\mathit{IterativeCEGIS}$, to synthesize rewrite rules using CBPS. This
algorithm iterates over all multisets of IR instructions up to a given size
and only runs synthesis on each such multiset. Compared to running synthesis
using all the IR instructions at once, this iterative algorithm works better
in practice. However, $\mathit{IterativeCEGIS}$ cannot synthesize rewrite
rules with both multi-instruction IR programs and multi-instruction ISA
programs. Furthermore, it produces duplicate rewrite rules which are then
filtered out in a post-synthesis filtering step. Although the results are
correct, this approach is highly inefficient because each call to CEGIS is
expensive, and a CEGIS call is made, not just for some duplicate rules, but
for every possible duplicate rule. In our approach, we make the requirement
that a solution is not a duplicate part of the CEGIS query itself, ensuring
that each successful CEGIS query finds a new, non-redundant rewrite rule.

⬇

1$\mathit{genAll}({\mathbf{K}}^{\mathit{IR}},{\mathbf{K}}^{\mathit{ISA}},N^{\mathit{IR}},N^{\mathit{ISA}})$:

2 $\mathbb{S}_{R}\leftarrow\\{\\}$

3 for $n_{1},n_{2}\in[1,N^{\mathit{IR}}]\times[1,N^{\mathit{ISA}}]$:

4 for
${\mathbf{m}}^{\mathit{IR}}\in\mathit{multicomb}({\mathbf{K}}^{\mathit{IR}},n_{1})$:

5 for
${\mathbf{m}}^{\mathit{ISA}}\in\mathit{multicomb}({\mathbf{K}}^{\mathit{ISA}},n_{2})$:

6 for
${\mathbf{I}}^{\mathit{IR}},{\mathbf{I}}^{\mathit{ISA}}\in\mathit{allInputs}({\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}})$:

7 $\phi,{\mathbf{L}}^{\mathit{IR}},{\mathbf{L}}^{\mathit{ISA}}\leftarrow$

8
$\mathit{GCBPS}({\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}},{\mathbf{I}}^{\mathit{IR}},{\mathbf{I}}^{\mathit{ISA}})$

9 $\phi\leftarrow\phi\
\wedge\neg\mathit{AllComposites}(\mathbb{S}_{R},\ldots)$

10 $\mathbb{S}_{R}\ \leftarrow\mathbb{S}_{R}\ \cup$

11
$\mathit{CEGISAll}(\phi,{\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}},{\mathbf{L}}^{\mathit{IR}},{\mathbf{L}}^{\mathit{ISA}})$

12 return $\mathbb{S}_{R}$

Figure 1: Iterative algorithm to generate all unique rewrite rules up to a
given size.

⬇

1$\mathit{CEGISAll}(\phi,{\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}},{\mathbf{L}}^{\mathit{IR}},{\mathbf{L}}^{\mathit{ISA}})$:

2 $\mathbb{S}_{R}=\\{\\}$

3 while True:

4 $\mathcal{M}\leftarrow\mathit{CEGIS}(\phi)$

5 if $\mathcal{M}=\bot$: return $\mathbb{S}_{R}$

6
$\mathbf{R}\leftarrow\mathit{rewriteRule}({\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}},\mathcal{M}_{{\mathbf{L}}^{\mathit{IR}}},\mathcal{M}_{{\mathbf{L}}^{\mathit{ISA}}})$

7 $\mathbb{S}_{R}\leftarrow\mathbb{S}_{R}\cup\\{\mathbf{R}\\}$

8
$\phi\leftarrow\phi\land\neg\psi_{\mathit{dup}}(\mathbf{R},({\mathbf{L}}^{\mathit{IR}},{\mathbf{L}}^{\mathit{ISA}}))$

Figure 2: AllSAT algorithm to synthesize all unique rules. Line 8 excludes all
rules that are duplicates of the current synthesized rewrite rule.

Our iterative algorithm, $\mathit{genAll}$, is shown in Figure 2. It takes as
parameters the IR and ISA component sets, ${\mathbf{K}}^{\mathit{IR}}$ and
${\mathbf{K}}^{\mathit{ISA}}$ respectively, as well as a maximum number of
components of each kind to use in rewrite rules, $N^{\mathit{IR}}$ and
$N^{\mathit{ISA}}$, and iteratively builds up a set $\mathbb{S}_{R}$ of
rewrite rules, which it returns at the end. Line 3 shows that $n_{1}$ and
$n_{2}$ iterate up to these maximum sizes. Line 4 iterates over all multisets
of elements from ${\mathbf{K}}^{\mathit{IR}}$ of size $n_{1}$ using a standard
multicombination algorithm $\mathit{multicomb}$ [25] (not shown). Line 5 is
similar but for multisets from ${\mathbf{K}}^{\mathit{ISA}}$ of size $n_{2}$.
Next, for a given choice of multisets, line 6 enumerates all possible ways of
selecting input vectors from those multisets that could create well-formed
programs. Line 7 constructs fresh sets of location variables
${\mathbf{L}}^{\mathit{IR}}$ and ${\mathbf{L}}^{\mathit{ISA}}$ and returns
them along with the instantiated GCBPS synthesis formula (using Equation
(6)).111We augment the well-formed program constraint in (6) to prevent
synthesizing programs containing dead code and unused inputs. This can be
accomplished by enforcing that each input and intermediate value is used in at
least one location. Line 8 excludes all composite rules from the synthesis
search space. Composite rules are rules that can be constructed using the
current set of rules $\mathbb{S}_{R}$ and are thus unnecessary for instruction
selection. We discuss this in more detail in Section V-B. Finally, on line 9,
the current set of rules $\mathbb{S}_{R}$ is updated with the result of
calling $\mathit{CEGISAll}$, which we describe next. Figure 2 shows the
$\mathit{CEGISAll}$ algorithm that performs the AllSAT [20, 31] task. Its
parameters are the synthesis formula $\phi$, the multisets
${\mathbf{m}}^{\mathit{IR}}$ and ${\mathbf{m}}^{\mathit{ISA}}$, and the
location variables ${\mathbf{L}}^{\mathit{IR}}$ and
${\mathbf{L}}^{\mathit{ISA}}$. It returns a set $\mathbb{S}_{R}$ of rewrite
rules. Initially this set is empty. The algorithm iteratively calls a standard
$\mathit{CEGIS}$ algorithm to solve the synthesis query, constructing a new
rewrite rule $\mathbf{R}$, which is added to the set $\mathbb{S}_{R}$ of
rewrite rules, when the call to $\mathit{CEGIS}$ is successful. The iteration
repeats until the $\mathit{CEGIS}$ query returns $\bot$, indicating that there
are no more rewrite rules to be found. Note that after each iteration, the
$\phi_{\mathit{synth}}$ formula is refined by adding the negation of a formula
capturing the notion of duplicates for this rule. We describe how this is done
next.

###  V-A Excluding Duplicate Rules

Consider the two distinct rules below. As a syntactical convention, infix
operators are used for IR patterns and function calls for ISA patterns.

$\displaystyle I_{1}+(I_{2}\cdot I_{3})\to add(I_{1},mul(I_{2},I_{3}))$
$\displaystyle(I_{1}\cdot I_{3})+I_{2}\to add(I_{2},mul(I_{1},I_{3}))$

The two IR patterns represent the same operation despite the fact that the
variable names and the order of the commutative arguments to addition are both
different. Both rules would match the same program fragments in an instruction
selector and would result in the same rewrite rule application. Thus, we
consider such rules to be equivalent and would like to ensure that only one is
generated by our algorithm. We first define a rewrite rule equivalence
relation, $\sim_{rule}$. Informally, two rules are equivalent if replacing
either one by the other has no discernible effect on the execution of an
instruction selection algorithm. We make this more formal by considering
various attributes of standard instruction selection algorithms. Commutative
Instructions Modern pattern matching algorithms used for instruction selection
try all argument orderings for commutative instructions [5]. We define the
commutative equivalence relation $\sim_{C^{\mathit{IR}}}$ as
${\mathbf{P}}^{\mathit{IR}}_{1}\sim_{C^{\mathit{IR}}}{\mathbf{P}}^{\mathit{IR}}_{2}$
iff ${\mathbf{P}}^{\mathit{IR}}_{2}$ is a remapping of
${\mathbf{P}}^{\mathit{IR}}_{1}$’s commutative instruction’s arguments. Same-
kind Instructions Programs $\mathbf{P}$ generated by GCPBS have a unique
identifier, the program line number, for each instruction. This means that if
two instructions of the same kind appear in a program, interchanging their
line numbers results in a different program, even though it makes no
difference to the instruction selection algorithm. We define the same-kind
equivalence relation $\sim_{K^{\mathit{IR}}}$ as
${\mathbf{P}}^{\mathit{IR}}_{1}\sim_{K^{\mathit{IR}}}{\mathbf{P}}^{\mathit{IR}}_{2}$
iff ${\mathbf{P}}^{\mathit{IR}}_{2}$ is the result of remapping the line
numbers for same-kind instructions in ${\mathbf{P}}^{\mathit{IR}}_{1}$. Data
Dependency Modern instruction selection algorithms perform pattern matching,
not based on a total order of instructions, but on a partial order determined
by data dependencies. Many different sequences may thus lead to the same
partial order. We define $\sim_{D^{\mathit{IR}}}$ as
${\mathbf{P}}^{\mathit{IR}}_{1}\sim_{D^{\mathit{IR}}}{\mathbf{P}}^{\mathit{IR}}_{2}$
iff ${\mathbf{P}}^{\mathit{IR}}_{1}$ and ${\mathbf{P}}^{\mathit{IR}}_{2}$ have
the same data dependency graph. Rule Input Renaming For a given rewrite rule,
the input variables used for the IR program must match the input variables
used for the ISA program, but the specific variable identifiers used do not
matter. We define the equivalence relation $\sim_{I^{\mathit{rule}}}$ on rules
(i.e., pairs of programs) as
$\mathbf{R}_{1}\sim_{I^{\mathit{rule}}}\mathbf{R}_{2}$ iff $\mathbf{R}_{2}$ is
the result of remapping variable identifiers in $\mathbf{R}_{1}$. Rule
Equivalence The first three equivalence relations defined above are for IR
programs, but the analogous relations ($\sim_{C^{\mathit{ISA}}}$,
$\sim_{K^{\mathit{ISA}}}$, $\sim_{D^{\mathit{ISA}}}$) for ISA instructions are
also useful. Putting everything together, we define rule equivalence
$\sim_{rule}$ as follows.

$\displaystyle\sim_{\mathit{IR}}\ $
$\displaystyle:=\uplus\\{\sim_{C^{\mathit{IR}}},\sim_{K^{\mathit{IR}}},\sim_{D^{\mathit{IR}}}\\}$
(7) $\displaystyle\sim_{\mathit{ISA}}\ $
$\displaystyle:=\uplus\\{\sim_{C^{\mathit{ISA}}},\sim_{K^{\mathit{ISA}}},\sim_{D^{\mathit{ISA}}}\\}$
(8) $\displaystyle\sim_{rule}\ $
$\displaystyle:=\uplus\\{(\sim_{\mathit{IR}}\otimes\sim_{\mathit{ISA}}),\sim_{I^{\mathit{rule}}}\\}$
(9)

Overall IR equivalence is defined as the transitive closure of the union
(notated with $\uplus$) of the three individual IR relations. ISA equivalence
is defined similarly. Overall rewrite rule equivalence is then defined using
the $\otimes$ operator, where $\sim_{\otimes}=\sim_{a}\otimes\sim_{b}$ is
defined as: $(a_{1},b_{2})\sim_{\otimes}(a_{2},b_{2})$ iff
$a_{1}\sim_{a}a_{2}$ and $b_{1}\sim_{b}b_{2}$. Specifically, rule equivalence
is obtained by combining IR equivalence in this way with ISA equivalence, and
then combining the result with $\sim_{I^{\mathit{rule}}}$ using $\uplus$. The
set of all duplicates of rule $\mathbf{R}$ is the rule equivalence class
$[\mathbf{R}]_{rule}$, where
$\mathbf{R^{\prime}}\in[\mathbf{R}]_{rule}\iff\mathbf{R}\sim_{rule}\mathbf{R^{\prime}}$.
$\psi_{\mathit{dup}}$ can be constructed by enumerating all elements of the
equivalence class $[\mathbf{R}]_{rule}$.

###  V-B Excluding Composite Rules

We also exclude any rule whose effect can already be achieved using the
current set of generated rules (line 8 of Figure 2). We elucidate this using a
simple example. Assume the algorithm just constructed a new query for the
multisets ${\mathbf{m}}^{\mathit{IR}}$, ${\mathbf{m}}^{\mathit{ISA}}$, and the
input ${\mathbf{I}}^{\mathit{IR}}$ (line 7 of Figure 2) and assume that the
rule library $\mathbb{S}_{R}$ currently contains rules for addition
($I_{1}+I_{2}\to add(I_{1},I_{2})$), and multiplication ($I_{1}\cdot I_{2}\to
mul(I_{1},I_{2})$). Consider the following cases.

  1. 1.

If ${\mathbf{I}}^{\mathit{IR}}=(I_{1})$, ${\mathbf{m}}^{\mathit{IR}}=\\{+\\}$,
and ${\mathbf{m}}^{\mathit{ISA}}=\\{add\\}$, then the rule $I_{1}+I_{1}\to
add(I_{1},I_{1})$ will be synthesized by $\mathit{CEGISAll}$. But this rule is
a specialization of the existing rule for addition. Any use of this
specialized rule could instead be replaced by the more general rule and this
rule can thus be excluded. Note that we order the inputs on line 6 of Figure 2
to guarantee that the most general version of a rule is found first.

  2. 2.

If ${\mathbf{I}}^{\mathit{IR}}=(I_{1},I_{2},I_{3})$,
${\mathbf{m}}^{\mathit{IR}}=\\{+,\cdot\\}$, and
${\mathbf{m}}^{\mathit{ISA}}=\\{add,mul\\}$, then the composite rule
$(I_{1}+(I_{2}\cdot I_{3}))\to add(I_{1},mul(I_{2},I_{3}))$ will be
synthesized by $\mathit{CEGISAll}$. Using similar logic, any use of this
composite rule could instead use the simpler and more general rules for
addition and multiplication, and this rule can thus be excluded. The multiset
ordering used in lines 4 and 5 of Figure 2 ensures that subsets are visited
before supersets, guaranteeing that smaller rules are found first.

Only a subset of composite rules built from existing rules need to be excluded
for each synthesis query. In general, for a specific query based on
${\mathbf{m}}^{\mathit{IR}}$, ${\mathbf{m}}^{\mathit{ISA}}$, and
${\mathbf{I}}^{\mathit{IR}}$, we exclude composite rules
$\mathbf{R}:=({\mathbf{P}}^{\mathit{IR}},{\mathbf{P}}^{\mathit{ISA}})$ that
meet the following criteria:

  * •

$\mathbf{R}$ has exactly $|{\mathbf{I}}^{\mathit{IR}}|$ inputs.

  * •

${\mathbf{P}}^{\mathit{IR}}$ has the same components as
${\mathbf{m}}^{\mathit{IR}}$.

  * •

${\mathbf{P}}^{\mathit{ISA}}$ has the same components as
${\mathbf{m}}^{\mathit{ISA}}$.

  * •

${\mathbf{P}}^{\mathit{IR}}$ is built from the IR programs of already-found
rules in $\mathbb{S}_{R}$.

  * •

${\mathbf{P}}^{\mathit{ISA}}$ is the result of applying the rewrite rules used
to build ${\mathbf{P}}^{\mathit{IR}}$.

These checks are encapsulated by the call to $\mathit{AllComposites}$ on line
8 of Figure 2.

##  VI Generating All Lowest-Cost Rules

⬇

1$\mathit{genAll}_{LC}({\mathbf{K}}^{\mathit{IR}},{\mathbf{K}}^{\mathit{ISA}},N^{\mathit{IR}},N^{\mathit{ISA}},\mathit{cost})$:

2
$\mathbf{K}_{\mathit{sorted}}\leftarrow\mathit{sortByCost}({\mathbf{K}}^{\mathit{ISA}},N^{ISA},\mathit{cost})$

3 $\mathbb{S}_{R}\leftarrow\\{\\}$

4 for n $\in[1,N^{\mathit{IR}}]$:

5 for
${\mathbf{m}}^{\mathit{IR}}\in\mathit{multicomb}({\mathbf{K}}^{\mathit{IR}},n)$:

6 for ${\mathbf{m}}^{\mathit{ISA}}\in\mathbf{K}_{\mathit{sorted}}$:

7 $c_{cur}\leftarrow\mathit{cost}({\mathbf{m}}^{\mathit{ISA}})$

8 for
${\mathbf{I}}^{\mathit{IR}},{\mathbf{I}}^{\mathit{ISA}}\in\mathit{allInputs}({\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}})$:

9 $\phi,{\mathbf{L}}^{\mathit{IR}},{\mathbf{L}}^{\mathit{ISA}}\leftarrow$

10
$\mathit{GCBPS}({\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}},{\mathbf{I}}^{\mathit{IR}},{\mathbf{I}}^{\mathit{ISA}})$

11
$\phi\leftarrow\phi\wedge\neg\mathit{AllComposites}_{\mathit{LC}}(\mathbb{S}_{R},c_{cur},\ldots)$

12 $\mathbb{S}_{R}\ \leftarrow\mathbb{S}_{R}\ \cup$

13
$\mathit{CEGISAll}_{\mathit{LC}}(\phi,{\mathbf{m}}^{\mathit{IR}},{\mathbf{m}}^{\mathit{ISA}},{\mathbf{L}}^{\mathit{IR}},{\mathbf{L}}^{\mathit{ISA}})$

14 return $\mathbb{S}_{R}$

Figure 3: Iterative algorithm to generate all lowest-cost rules. ISA multisets
are ordered by cost. $\mathit{CEGISAll}$ is modified to exclude rules with
duplicate IR programs.

Because all duplicates are excluded, the $genAll$ algorithm generates only
unique rewrite rules. However, two unique rules can share the same IR pattern.
For a particular IR pattern, only the lowest-cost rule is needed for some cost
metrics. Knowing the instruction selection cost metric at rule-generation time
presents another time-saving opportunity because we can also prevent the
synthesis of high-cost rules. We make a few assumptions about such a cost
metric.

  * •

The cost for an instruction selection tiling is equal to the sum of the costs
of each tiling rule’s ISA program.

  * •

The cost of an ISA program ${\mathbf{P}}^{\mathit{ISA}}$ only depends on the
instruction contents, not the program structure. This cost is the sum of the
cost of each instruction in the program.

While these assumptions are a restriction on the space of possible cost
metrics, they are sufficient to represent common ones like code size and
energy. If the compiler’s cost metric violates these assumptions, the
$\mathit{genAll}$ algorithm can be used instead. This restricted space of cost
metrics has the important property that the cost of any rule that would be
synthesized using the components ${\mathbf{m}}^{\mathit{ISA}}$ can be
determined up front as the sum of the cost of each component. Figure 3 shows
our synthesis algorithm updated to only synthesize the lowest-cost rules for
each unique IR pattern. The first change is to sort all possible mulitsets of
ISA instructions up to size $N^{\mathit{ISA}}$ by cost (lower cost first)
(line 2). This ordering ensures that the first rule synthesized for a
particular IR program will be the lowest-cost version of that rule. Therefore,
after synthesizing a new rule, all rules with a duplicate IR program can be
excluded. The second change excludes rules with duplicate IR programs. A
duplicate IR program is defined using the IR equivalence relation:

$\displaystyle\sim_{\mathit{IR}_{\mathit{LC}}}$
$\displaystyle:=\uplus\\{\sim_{C^{\mathit{IR}}},\sim_{K^{\mathit{IR}}},\sim_{D^{\mathit{IR}}},\sim_{I^{\mathit{IR}}}\\}$
(10)

This is the same definition as (7), but with an additional relation
$\sim_{I^{\mathit{IR}}}$ defined as
${\mathbf{P}}^{\mathit{IR}}_{1}\sim_{I^{\mathit{IR}}}{\mathbf{P}}^{\mathit{IR}}_{2}$
iff ${\mathbf{P}}^{\mathit{IR}}_{2}$ is the result of remapping variable
identifiers in ${\mathbf{P}}^{\mathit{IR}}_{1}$. The
$\mathit{CEGISAll}_{\mathit{LC}}$ function called on line 11 is the same as
$\mathit{CEGISAll}$, except that it uses $\sim_{\mathit{IR}_{\mathit{LC}}}$
instead of $\sim_{\mathit{IR}}$ when constructing $\psi_{\mathit{dup}}$. The
third change modifies $\mathit{AllComposites}$ to use the known up-front cost
$\mathit{cost}({\mathbf{m}}^{\mathit{ISA}})$. To see how this works, we
consider again the example from Section V-B. As before, we assume
$\mathbb{S}_{R}$ currently contains two rules: one for addition
($I_{1}+I_{2}\to add(I_{1},I_{2})$) and one for multiplication ($I_{1}\cdot
I_{2}\to mul(I_{1},I_{2})$). We assume the target (ISA) expressions for these
rules have cost 5 and 10, respectively. Consider the following situation:

  * •

Suppose ${\mathbf{I}}^{\mathit{IR}}=(I_{1},I_{2},I_{3})$, and
${\mathbf{m}}^{\mathit{IR}}=\\{+,\cdot\\}$. It might be possible to synthesize
a rule that has IR pattern $(I_{1}+(I_{2}\cdot I_{3}))$. We know that the
composite rule $(I_{1}+(I_{2}\cdot I_{3}))\to add(I_{1},mul(I_{2},I_{3}))$
would have a cost of 15 since rule costs are additive. Therefore, we can
exclude any rule that matches this IR pattern and has
$\mathit{cost}({\mathbf{m}}^{\mathit{ISA}})\geq 15$.

To implement this, only one adjustment needs to be made to the conditions in
Section V-B. Instead of requiring ${\mathbf{P}}^{\mathit{ISA}}$ to have the
same components as ${\mathbf{m}}^{\mathit{ISA}}$, we simply require
$\mathit{cost}({\mathbf{P}}^{\mathit{ISA}})\geq\mathit{cost}({\mathbf{m}}^{\mathit{ISA}})$,
i.e., for rules matching the other conditions, if the ISA program has a cost
equal to or greater than cost of the ISA program in the current rule, it is
excluded. These conditions are encapsulated by the call to
$\mathit{AllComposites}_{\mathit{LC}}$ (line 10).

##  VII Evaluation

Our evaluation strategy is threefold. We first show that our algorithm is
capable of producing a variety of many-to-many rules. A good set of rewrite
rules involves both many-to-one and one-to-many rules. We also show that by
removing duplicate, composite, and high-cost rules, we produce a much smaller
set of rewrite rules. Second, we analyze the effect on performance of the
optimizations described above. We show that they all significantly reduce the
time spent in synthesis. Finally, we show that by using different cost
metrics, we can generate different sets of lowest-cost rewrite rules.

###  VII-A Implementation

All instructions are formally specified using the hwtypes Python library [11],
which leverages pySMT [18] to construct (quantifier-free) SMT queries in the
theory of bit-vectors. We also use annotations indicating which instructions
are commutative. We use Boolector [28] as the SMT solver and set a timeout of
12 seconds for each CEGIS invocation. Every synthesized rewrite rule is
independently verified to be valid.

###  VII-B Instruction Specifications

To evaluate our algorithms, we selected small but non-trivial sets of IR and
ISA instructions operating on 4-bit bit-vectors. IR We define the IR
instruction set to be constants (0, 1), bitwise operations ($not$, $and$,
$or$, $xor$), arithmetic operations ($neg$, $add$, $sub$), multiplication
($mul$), unsigned comparison operations ($ult$, $ule$, $ugt$, $uge$), equality
($eq$), and dis-equality ($neq$). ISA 1 This is a minimal RISC-like ISA
containing only 6 instructions: $nand$, $sub$, three comparison instructions
($cmpZ$, $cmpN$, $cmpC$) which compute the zero (Z), sign (N), and carry (C)
flags respectively for a subtraction, and a flag inverting instruction
($inv$). ISA 2 This is an ISA specialized for linear algebra. It supports the
5 instructions: $neg$, $add$, $add3$ (addition of 3 values), $mul$, and $mac$
(multiply-accumulate).

| ISA Program Size
---|---
| All Rules | Only Unique | Only Lowest-Cost
| 1 | 2 | 3 | 1 | 2 | 3 | 1 | 2 | 3 | 4 | 5
IR Prog Size | 1 | 5 | 32 | 1096 | 3 | 10 | 96 | 3 | 4 | 2 | 1 | 0
2 | 76 | 1719 | 56894 | 40 | 189 | 1940 | 40 | 67 | 34 | 12 | 6

TABLE I: Number of synthesized rewrite rules for ISA 1a.

| ISA Program Size
---|---
| All Rules | Only Unique | Only Lowest-Cost
| 1 | 2 | 3 | 1 | 2 | 3 | 1 | 2 | 3 | 4
IR Program Size | 1 | 17 | 71 | 3662 | 9 | 51 | 873 | 7 | 3 | 0 | 0
2 | 89 | 3942 (-5) | 199572 | 78 | 717 | 21511 | 52 | 64 | 9 | 0

TABLE II: Number of synthesized rewrite rules for ISA 1b.

| IR Program Size
---|---
| All Rules | Only Unique | Only Lowest-Cost
| 1 | 2 | 3 | 1 | 2 | 3 | 1 | 2 | 3
ISA Program Size | 1 | 11 | 287 | 3998 | 3 | 14 | 315 | 3 | 14 | 315
2 | 10 | 3115 | $341758^{*}$ | 3 | 69 | 1337 | 1 | 32 | 760

TABLE III: Number of synthesized rewrite rules for ISA 2. ISA | Rule Size up | % Duplicate | % High-cost
---|---|---|---
| to (IR, ISA) | or Composite |
1a | (2, 3) | 96.2% | 99.7%
1b | (2, 3) | 88.8% | 99.9%
2 | (3, 2) | 99.5% | 99.7%
TABLE IV: Percent of rewrite rules up to (IR, ISA) size that are a duplicate
or a composite, and percent that are high-cost.

###  VII-C Rewrite Rule Synthesis

For each ISA we run three experiments. The first experiment (All Rules) is the
baseline that generates all many-to-many rules including duplicate, composite,
and high cost rules. This is an implementation of Buchwald et al.’s
$\mathit{IterativeCEGIS}$ algorithm extended to use GCBPS for many-to-many
rules (notated as $\mathit{IterativeCEGIS_{GCBPS}}$). The second (Only Unique)
generates only unique rules by excluding all duplicates and composites using
the $\mathit{genAll}$ algorithm. The third (Only Lowest-Cost) generates only
the lowest-cost rules using the $\mathit{genAll}_{LC}$ algorithm in Figure 3.
A code-size cost metric is used, i.e., $\mathit{cost}(\mathbf{K})$ is just the
number of components in $\mathbf{K}$. For ISA 1, we split the rule generation
into two parts. The first part (ISA 1a) synthesizes rules composed of bitwise
and arithmetic IR instructions using the ISA’s $nand$ and $sub$ instructions.
The second part (ISA 1b) synthesizes rules composed of constants and
comparison instructions using the four instructions $cmpZ$, $cmpN$, $cmpC$,
and $inv$. For 1a and 1b, we synthesize rewrite rules up to an IR program size
of 2 and an ISA program size of 3 (written 2-to-3). For (Only Lowest-Cost), we
increase the ISA program size to 5 and 4 respectively. For ISA 2, we
synthesize all rewrite rules composed of constant, and arithmetic (including
$mul$) IR instructions up to size 3-to-2. The number of rewrite rules produced
for ISA 1a, 1b, and 2 are shown in Tables III, III, and III, respectively.
Each table entry is the number of rewrite rules synthesized for a particular
IR and ISA program size. For all ISAs, the extra synthesized rules in (All
Rules) were compared against the duplicate and composite rules excluded by
(Only Unique). Entries in (All Rules) marked with a ‘(-n)’ represent ‘n’ rules
that (Only Unique) synthesized, but (All Rules) missed due to CEGIS timeouts.
The (All Rules) experiment for the entry marked with an asterisk could not
complete in 70 hours, so the number calculated from (Only Unique) is shown.
For both ISAs we were able to synthesize 1-to-many and many-to-1 rules for
both IR and ISA instructions. $\mathit{genAll}$ produced a more complete set
of rules than $\mathit{IterativeCEGIS_{GCBPS}}$. Table IV shows the percentage
of rules that are duplicates or composites in the first column, and the
percentage of rules that are high cost in the second column. Most rules in
(All Rules) are duplicates, composites, or high cost. Out of the 349179 rules
up to size 3-to-2 for ISA 2 (i.e. the sum of the (All Rules)), 99.5% are
duplicates or composites. Similarly, most rules are high cost. In ISA 1a,
59672 out of 59822 rules (99.7%) up to size 2-to-3 are high cost.

###  VII-D Synthesis Time Improvement with $\mathit{genAll}$

In this section we showcase the synthesis time improvements of
$\mathit{genAll}$. The first experiment is the baseline
$\mathit{IterativeCEGIS_{GCBPS}}$. The second excludes duplicate rules (i.e.,
with line 8 of Figure 2). The third, $\mathit{genAll}$, excludes both
duplicates and composites (i.e. with line 8 of both Figure 2 and Figure 2).
For each $\mathit{GCBPS}$ query, we note the time required
($t_{\mathit{sat}}$) to run $\mathit{CEGISAll}$. Next, we measure the number
of unique rules ($N_{\mathit{unique}}$) found by $\mathit{CEGISAll}$. We then
add the pair ($N_{\mathit{unique}},t_{\mathit{sat}}$) to our dataset. We plot
the cumulative synthesis time versus the number of unique rules found by doing
the following. Each data point is sorted by its slope
($t_{\mathit{sat}}/N_{\mathit{unique}}$). Then, the increase in both
$t_{\mathit{sat}}$ and $N_{\mathit{unique}}$ is plotted for each sorted point.
Some data points have $N_{\mathit{unique}}=0$ indicating that every
synthesized rule was redundant and is shown using a vertical slope. The
synthesis time plot for unique rewrite rules for ISA 1b up to size 2-to-3 is
shown in Figure 4(a). Excluding all duplicates shows a 5.3$\times$ speedup.
Excluding both duplicates and composites shows a 6.2$\times$ speedup. Both
optimizations find an additional 5 unique rules.

(a) $\mathit{genAll}$

(b) $\mathit{genAll}_{LC}$

Figure 4: Cumulative synthesis time comparison for ISA 1b up to size 2-to-3.

###  VII-E Synthesis Time Improvement with $\mathit{genAll}_{LC}$

We also showcase the synthesis time improvements of $\mathit{genAll}_{LC}$
using a similar setup. The first experiment is the baseline
$\mathit{IterativeCEGIS_{GCBPS}}$. The second excludes IR duplicate rules. The
third, $\mathit{genAll}_{LC}$, excludes both IR duplicates and IR composites.
We use the same experimental setup as before except when computing
$N_{\mathit{unique}}$, all higher-cost rules are filtered instead. The
synthesis time plot for lowest-cost rewrite rules for ISA 1b up to size 2-to-3
is shown in Figure 4(b). Excluding rules with duplicate IR programs provides a
41$\times$ speed-up. Also excluding high-cost composites provides a
1254$\times$ speed-up over the baseline (All Rules) configuration.

###  VII-F Total Speed-up

We summarize the speed-ups of $\mathit{genAll}$ and $\mathit{genAll}_{LC}$
compared to the $\mathit{IterativeCEGIS_{GCBPS}}$ baseline for all
configurations in Table V. We compare the synthesis time in the “Synth”
column. We compare the total algorithm runtime in the “Total” column
(including time for iterating, solving, rule filtering, etc.). The last row’s
baseline did not complete in 70 hours, so we provide lower bounds for speed-
up. The speed-ups depend on many parameters including the maximum size of the
rewrite rules, the number of possible instructions, the commutativity of the
instructions, and the semantics of the instructions. The optimizations
discussed produce several orders of magnitude speed-ups. Further optimizing
the non-solver portions (e.g. re-coding in C) would drastically increase the
“Total” speed-ups to be closer to the “Synth” ones. Clearly, the combination
of all optimizations discussed in this paper can produce speed-ups of several
orders of magnitude.

ISA | Rule Size up |  $\mathit{genAll}$ Speed-up |  $\mathit{genAll}_{LC}$ Speed-up
---|---|---|---
| to (IR, ISA) | Synth | Total | Synth | Total
1a | (2, 2) | 3.5$\times$ | 1.3$\times$ | 11$\times$ | 2.8$\times$
1b | (2, 2) | 3.1$\times$ | 1.7$\times$ | 26$\times$ | 2.8$\times$
2 | (2, 2) | 11$\times$ | 2$\times$ | 53$\times$ | 2.5$\times$
1a | (2, 3) | 12$\times$ | 6.8$\times$ | 601$\times$ | 57$\times$
1b | (2, 3) | 6.2$\times$ | 2.7$\times$ | 1254$\times$ | 63$\times$
2 | (3, 2) | > 768$\times$ | > 81$\times$ | > 4004$\times$ | > 171$\times$
TABLE V: Speed-ups compared to $\mathit{IterativeCEGIS_{GCBPS}}$.

###  VII-G Cost Metric Comparisons

Our final experiment explores how the choice of cost metric influences the
rules. We have implemented two cost metrics: a code size metric (CS) and an
estimated energy metric (E). The energy metric was created to correspond to
real hardware energy data. For example the cost ratio for $mul$ and $add$ is
$1:1$ for code size, but is $2.5:1$ for energy. The number of common and
unique lowest-cost rewrite rules for each ISA is shown in Table VI.

ISA | Rule Size up | Unique | Unique | Common
---|---|---|---|---
| to (IR, ISA) | (CS) | (E) |
1a | (2, 5) | 121 | 161 | 48
1b | (2, 4) | 99 | 198 | 36
2 | (3, 2) | 134 | 137 | 991
TABLE VI: Number of unique and common rewrite rules synthesized for code size
(CS) and energy (E) cost metrics.

While there is some overlap in common rules, each cost metric produces a
differing set of unique lowest-cost rules.

##  VIII Conclusion and Future Work

We showed that many-to-many instruction selection rewrite rules can be
synthesized for various ISAs using program synthesis. This supports two major
trends in computer architecture. The first is the trend towards simple or
reduced instruction architectures where multiple instructions are needed for
simple operations. It also supports the trend to introduce more complex
domain-specific instructions for energy efficiency. In this case, a single
instruction can implement complex operations. We showed that our algorithms
are efficient. Removing duplicates, composites, and higher-cost rules results
in multiple orders of magnitude speed-ups. Synthesizing many-to-many rewrite
rules for modern IRs and ISAs may require further optimizations. Many of our
synthesized rules contain program fragments that a compiler would optimize
before instruction selection (e.g., $sub(X,X)$). Excluding these could result
in further speed-ups. Buchwald et al. [6] presented generalizations for multi-
sorted instructions, multiple outputs, preconditions, and internal attributes,
enabling the modeling of memory and control flow instructions. Our synthesis
query and algorithms are orthogonal and could incorporate these features,
allowing for a broader range of possible instruction sets. As is the case in
prior work, we limit synthesis to loop free patterns. Relaxing this constraint
and using other instruction selection algorithms would be an interesting
research avenue. We believe this research area is fertile ground and hope our
work inspires and enables future research endeavors towards the goal of
automatically generating compilers for emerging domain-specific architectures.

## IX

### IX-A

## References

  * [1] Alfred V. Aho, Mahadevan Ganapathi, and Steven W. K. Tjiang.  Code generation using tree matching and dynamic programming.  ACM Transactions on Programming Languages and Systems (TOPLAS), 11(4):491–516, 1989.
  * [2] Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid.  Recursive program synthesis.  In Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25, pages 934–950. Springer, 2013.
  * [3] Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa.  Scaling enumerative program synthesis via divide and conquer.  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 319–336. Springer, 2017.
  * [4] Rick Bahr, Clark Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick, David Durst, Kayvon Fatahalian, Kathleen Feng, Pat Hanrahan, et al.  Creating an agile hardware design flow.  In 2020 57th ACM/IEEE Design Automation Conference (DAC), pages 1–6. IEEE, 2020.
  * [5] Eli Bendersky.  A deeper look into the LLVM code generator, Part 1, Feb 2013.
  * [6] Sebastian Buchwald, Andreas Fried, and Sebastian Hack.  Synthesizing an instruction selection rule library from semantic specifications.  In Proceedings of the 2018 International Symposium on Code Generation and Optimization, pages 300–313, 2018.
  * [7] R. G. Cattell.  Automatic derivation of code generators from machine descriptions.  ACM Transactions on Programming Languages and Systems (TOPLAS), 2(2):173–190, 1980.
  * [8] Yu-Hsin Chen, Joel Emer, and Vivienne Sze.  Eyeriss: A spatial architecture for energy-efficient dataflow for convolutional neural networks.  ACM SIGARCH Computer Architecture News, 44(3):367–379, 2016.
  * [9] Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze Bullock, Priyanka Raina, Clark Barrett, and Pat Hanrahan.  Synthesizing instruction selection rewrite rules from RTL using SMT.  In Conference on Formal Methods in Computer-Aided Design (FMCAD), page 139, 2022.
  * [10] Joao Dias and Norman Ramsey.  Automatically generating instruction selectors using declarative machine descriptions.  ACM Sigplan Notices, 45(1):403–416, 2010.
  * [11] Caleb Donovick, Ross Daly, Jackson Melchert, Lenny Truong, Priyanka Raina, Pat Hanrahan, and Clark Barrett.  Peak: A single source of truth for hardware design and verification.  arXiv preprint arXiv:2308.13106, 2023.
  * [12] Helmut Emmelmann, F.-W. Schröer, and Rudolf Landwehr.  BEG: A generator for efficient back ends.  ACM Sigplan Notices, 24(7):227–237, 1989.
  * [13] Herbert Enderton and Herbert B. Enderton.  A mathematical introduction to logic.  Elsevier, 2001.
  * [14] Christopher W. Fraser and David R. Hanson.  A retargetable C compiler: Design and implementation.  Addison-Wesley Longman Publishing Co., Inc., 1995.
  * [15] Christopher W. Fraser, David R. Hanson, and Todd A. Proebsting.  Engineering a simple, efficient code-generator generator.  ACM Letters on Programming Languages and Systems (LOPLAS), 1(3):213–226, 1992.
  * [16] Mahadevan Ganapathi.  Retargetable code generation and optimization using attribute grammars.  PhD thesis, 1980.  AAI8107834.
  * [17] Mahadevan Ganapathi and Charles N. Fischer.  Description-driven code generation using attribute grammars.  In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’82, page 108–119, New York, NY, USA, 1982. Association for Computing Machinery.
  * [18] Marco Gario and Andrea Micheli.  PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms.  In SMT Workshop 2015, 2015.
  * [19] R. Steven Glanville and Susan L. Graham.  A new method for compiler code generation.  In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’78, page 231–254, New York, NY, USA, 1978. Association for Computing Machinery.
  * [20] Orna Grumberg, Assaf Schuster, and Avi Yadgar.  Memory efficient all-solutions SAT solver and its application for reachability analysis.  In Formal Methods in Computer-Aided Design: 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004. Proceedings 5, pages 275–289. Springer, 2004.
  * [21] Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan.  Synthesis of loop-free programs.  In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011.
  * [22] John L. Hennessy and David A. Patterson.  A new golden age for computer architecture.  Commun. ACM, 62(2):48–60, January 2019.
  * [23] Roger Hoover and Kenneth Zadeck.  Generating machine specific optimizing compilers.  In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 219–229, 1996.
  * [24] Norman P. Jouppi, Cliff Young, Nishant Patil, and David Patterson.  A domain-specific architecture for deep neural networks.  Communications of the ACM, 61(9):50–59, 2018.
  * [25] Donald E. Knuth.  The Art of Computer Programming, Volume 4, Fascicle 3: Generating All Combinations and Partitions.  Addison-Wesley Professional, 2005.
  * [26] David Ryan Koes and Seth Copen Goldstein.  Near-optimal instruction selection on DAGs.  In Proceedings of the 6th Annual IEEE/ACM International Symposium on Code Generation and Optimization, pages 45–54, 2008.
  * [27] Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark Barrett, Mark A Horowitz, Pat Hanrahan, and Priyanka Raina.  APEX: A framework for automated processing element design space exploration using frequent subgraph analysis.  In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, pages 33–45, 2023.
  * [28] Aina Niemetz, Mathias Preiner, and Armin Biere.  Boolector 2.0.  J. Satisf. Boolean Model. Comput., 9(1):53–58, 2014.
  * [29] Eduardo Pelegri-Llopart and Susan L. Graham.  Optimal code generation for expression trees: An application BURS theory.  In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 294–308, 1988.
  * [30] Raghu Prabhakar, Yaqi Zhang, David Koeplinger, Matt Feldman, Tian Zhao, Stefan Hadjis, Ardavan Pedram, Christos Kozyrakis, and Kunle Olukotun.  Plasticine: A reconfigurable architecture for parallel patterns.  ACM SIGARCH Computer Architecture News, 45(2):389–402, 2017.
  * [31] Takahisa Toda and Takehide Soh.  Implementing efficient all solutions sat solvers.  Journal of Experimental Algorithmics (JEA), 21:1–44, 2016.


# Post-training deep neural network pruning via layer-wise calibration

Ivan Lazarevich
Intel Corporation
<EMAIL_ADDRESS>Alexander Kozlov
Intel Corporation
<EMAIL_ADDRESS>Nikita Malinin
Intel Corporation
<EMAIL_ADDRESS>
###### Abstract

We present a post-training weight pruning method for deep neural networks that
achieves accuracy levels tolerable for the production setting and that is
sufficiently fast to be run on commodity hardware such as desktop CPUs or edge
devices. We propose a data-free extension of the approach for computer vision
models based on automatically-generated synthetic fractal images. We obtain
state-of-the-art results for data-free neural network pruning, with $\sim$1.5%
top@1 accuracy drop for a ResNet50 on ImageNet at 50% sparsity rate. When
using real data, we are able to get a ResNet50 model on ImageNet with 65%
sparsity rate in 8-bit precision in a post-training setting with a $\sim$1%
top@1 accuracy drop. We release the code as a part of the OpenVINOTM Post-
Training Optimization
tool111https://docs.openvinotoolkit.org/latest/pot_README.html.

##  1 Introduction

Deep neural network (DNN) models have achieved unprecedented accuracy in
several crucial domains such as computer vision and natural language
processing. Despite the success of DNN models, an unreasonably large amount of
computations and memory required for their inference limits their deployment
on edge devices, such as smart cameras equipped with low-power CPUs, GPUs or
ASIC accelerators. Significant efforts in recent years have been devoted to
both hardware design and algorithmic approaches to DNN model compression to
enable inference speedups for various model architectures and use cases. Some
of the DNN compression methods, such as 8-bit quantization, were adapted to
the post-training setting where the original DNN model to be compressed could
come from any software framework and no access to the original training
pipeline and the training dataset is given. One of the promising approaches to
reduce the memory footprint and inference latency of DNNs is weight pruning
[2, 4], which results in models with sparse weight matrices. Recently, a lot
of research and development has been aimed at leveraging weight sparsity to
achieve inference speedups on a range of hardware platforms [3, 6]. However,
relatively little effort was devoted to providing accurate sparse DNN models
in the post-training scenario.

In this work, we propose a recipe for fast post-training pruning of DNNs that
produces models with significant sparsity rates (e.g. 50%) but negligible
accuracy drops. Furthermore, if combined with weight quantization techniques,
the proposed method could reduce the model memory footprint by a factor of
6-8x [16]. We propose a fast data-free extension of our weight pruning
pipeline which allows getting state-of-the-art accuracy levels for a range of
computer vision models. To streamline the deployment process of sparse
quantized DNNs on hardware, we have implemented the proposed method as a part
of the OpenVINOTM Post-Training Optimization tool.

We summarize our contributions as follows:

  * •

A recipe for post-training weight pruning with demonstrated results on a wide
range of models and datasets.

  * •

State-of-the-art results for data-free weight pruning of computer vision
models using synthetic fractal images for model compression.

  * •

An ablation study of the proposed post-training weight pruning pipeline
demonstrating the effects of particular components such as per-layer sparsity
rate selection criteria, bias correction and layer-wise fine-tuning settings.

Table 1: Accuracy values of the sparse 8-bit quantized DNN models obtained with the proposed post-training method. Metric values were measured on a CPU with OpenVINOTM 2021.3 as an inference engine. The same is for other accuracy values reported in the paper unless specified otherwise. Model | Dataset (acc. metric) | Sparsity rate, % | Compressed model acc. | Absolute acc. drop
---|---|---|---|---
ResNet50 | ImageNet (top@1 acc.) | 65 | 75.09 | 1.04
ResNet18 | ImageNet (top@1 acc.) | 50 | 68.93 | 0.81
GoogleNetV4 | ImageNet (top@1 acc.) | 50 | 78.96 | 0.94
MobileNetV2 | ImageNet (top@1 acc.) | 40 | 70.29 | 1.51
MobileNetV1-SSD | VOC07 (mAP) | 50 | 71.53 | 0.98
TinyYOLOv2 | COCO (AP) | 50 | 28.29 | 0.83
NCF | MovieLens 20M (hit ratio) | 70 | 64.67 | 0.93
BERT-base | MRPC (acc.) | 50 | 82.50 | 0.63
Table 2: Accuracy of sparse computer vision models obtained with layer-wise fine-tuning on different input data. Note that accuracy levels are very similar when fine-tuning on original validation or training datasets, suggesting the absence of overfitting during layer-wise fine-tuning. ”FractalDB-1k(c)” denotes the colored FractalDB-1k dataset. Model (sparsity rate, dataset/acc. metric) |  Orig. model acc. |  Val. data |  Training data |  FractalDB 1k(c) |  White noise
---|---|---|---|---|---
ResNet18 (50%; ImageNet top@1) |  69.75 |  68.94 |  68.92 |  68.27 |  66.90
ResNet50 (50%; ImageNet top@1) |  76.13 |  75.51 |  75.57 |  74.50 |  73.89
MobileNetV2 (40%; ImageNet top@1) |  71.81 |  70.04 |  70.12 |  68.94 |  66.84
MobileNetV1-SSD (50%; VOC07 mAP) |  72.51 |  71.37 |  71.53 |  71.13 |  69.52
TinyYOLOv2 (50%; COCO AP) |  29.12 |  28.06 |  28.29 |  28.18 |  27.10
RetinaFace-ResNet50 (50%; WIDER FACE mAP) |  87.29 |  87.40 |  87.41 |  87.45 |  86.87

##  2 Related work

Neural network weight pruning is a technique used to produce lightweight
models by removing (zeroing out) a certain percentage of unimportant weights.
In this work, we focus on unstructured pruning (weight sparsification) whereby
no structural constraints on the sparsity pattern are imposed and a subset of
weights determined to have the lowest importance score values is removed
regardless of position in weight tensors. Various definitions of weight
importance functions have been proposed in the literature [4, 23], the
simplest baseline being magnitude-based weight pruning, as well as various
heuristics to determine per-layer sparsity rates [13, 7]. Magnitude-based
sparsification via a global importance threshold was found to be a strong
baseline in the compression-aware training regime for a range of models [4,
20]. These weight pruning approaches typically imply compression-aware model
re-training, which means existing access to the training code, the training
dataset and appropriate compute resources. Other DNN compression techniques,
such as 8-bit quantization, however, have been successfully applied in a less
restrictive setting – in the post-training or data-free regimes [18]. The
post-training compression regime is favorable from a practical perspective,
since model compression could be ultimately implemented via a single API call
rather than via the modification of the original model training code. There,
however, have been few attempts to implement post-training or data-free weight
pruning of DNNs, primarily due to the large accuracy drop incurred during
sparsification [8, 21]. Recently, there have also been developed layer-wise
gradient optimization-based methods for post-training compression [9, 15, 17,
8] with applications to low-bitwidth quantization and weight pruning. These
methods are promising because they allow restoring compressed model accuracy
in the post-training setting in many cases. Nevertheless accuracy degradation
was still found to be significant for sparsity rates above 40%. In this work,
we propose a post-training sparsification recipe that allows insignificant
accuracy drops on a range of DNN models at sparsity rates of 50% and higher.
We also suggest a straightforward and fast extension of the method for the
data-free compression of computer vision models, using synthetic fractal image
data, that allows getting state-of-the-art accuracy on a range of natural
image datasets.

##  3 Post-training sparsity pipeline

Figure 1: Flowchart of the proposed post-training sparsity pipeline. The
process begins with a small initial global sparsity value, the model is fine-
tuned in a layer-wise manner, the sparsity level is increased and the fine-
tuning is repeated. This iterative process is carried out until the target
sparsity level or the maximal allowed accuracy drop is reached (either of
these parameters is set in advance).

The proposed post-training sparsity pipeline consists of three basic steps:
(i) layer-wise sparsity rate selection given a global sparsity constraint,
(ii) bias & variance correction steps, and (iii) layer-wise fine-tuning using
auxiliary knowledge distillation losses. We introduce a progressively
increasing sparsity schedule for each layer whereby these three steps are
performed iteratively and the global sparsity rate in the model is increased
on each iteration (see the flowchart in Fig. 1). The global sparsity rate for
the model on the $t^{th}$ iteration of the pipeline is determined via the
following polynomial (cubic) sparsity schedule [23]:

$s_{t}=s_{f}+(s_{i}-s_{f})\left(1-\frac{t}{T}\right)^{3}$

where $s_{i}$ and $s_{f}$ are the initial and final global sparsity rates of
the model, respectively, and $T$ is the total number of iterations of the
pipeline. After the original floating-point precision model with the target
global sparsity rate is obtained, the standard procedure of post-training
quantization is performed to prepare the model to be executed in 8-bit
precision. We found that performing post-training quantization on the pruned
model does not incur significant accuracy degradation compared to the
original-precision sparse model (see Fig. 2 for results on ResNet18/50 on
ImageNet), probably due to reduced quantization noise of sparse weight
matrices. We are using the following quantization configuration throughout the
paper: symmetric per-tensor quantization of activations (except for specific
per-channel cases like e.g. depthwise convolutions) and symmetric per-channel
quantization of weights. We further provide details on all the steps performed
on every iteration of the pruning pipeline in the corresponding sections
below.

### Layer-wise sparsity rate selection procedure

Table 3: Impact of per-layer sparsity selection criteria on a pre-trained ResNet50 model on ImageNet with 50% of weights pruned. Sparsity selection criterion |  BN-fusing |  Top@1 accuracy, %
---|---|---
ResNet50 50% sparsity |  |
Original model |  |  76.13
Magnitude |  Yes |  0.3814
L2-normalized magnitude |  Yes |  72.544
LAMP |  Yes |  72.328
Magnitude |  No |  72.831
L2-normalized magnitude |  No |  72.244
ResNet18 50% sparsity |  |
Original model |  |  69.75
Magnitude |  Yes |  0.418
L2-normalized magnitude |  Yes |  64.856
LAMP |  Yes |  64.866
MobileNetV2 30% sparsity |  |
(with bias correction) |  |
Original model |  |  71.81
Magnitude |  Yes |  18.386
L2-normalized magnitude |  Yes |  69.528
LAMP |  Yes |  69.524
Figure 2: Accuracy drop/sparsity rate curves for a ResNet18 (top) and a
ResNet50 (bottom) model obtained with our post-training pruning and
quantization pipeline. The horizontal dashed red line indicates the level of
1% absolute accuracy drop. Note that post-training quantization of the pruned
model does not lead to a huge accuracy drop increase for both models at
different sparsity rate levels. Figure 3: Absolute top@1 accuracy drops for a
range of models from the torchvision package pruned with a 50% global sparsity
rate depending on the per-layer compression level selection criterion.
BatchNorm fusing was not performed in the networks. Pruning is done in the
post-training regime (without any fine-tuning), BatchNorm adaptation is
performed after weight pruning. Global magnitude criterion is optimal in most
cases in this setting except for lightweight models such as MobileNets,
SqueezeNets and ShuffleNets. BatchNorm adaptation is a procedure analogous to
bias correction whereby the BN statistics are recollected after the model has
been compressed [14]. Accuracy drops are measured relative to the original
pre-trained weights using PyTorch on a GPU.

The problem of selecting an optimal (in terms of model accuracy) layer-wise
sparsity rate configuration given a certain global sparsity constraint is a
widely discussed problem in the literature [13]. The proposed approaches range
from simple heuristics (e.g. pruning uniformly except for the first and the
last layers in the network [4]) to making per-layer sparsity rates learnable
[12] or searching for the best configuration via global non-gradient
optimization or reinforcement learning [7]. The heuristic approaches also
include finding a global threshold for weight importance scores and pruning
all the weights with importances below this threshold. This naturally leads to
a non-uniform pattern of per-layer sparsity rates. The importance score
function in this case might be the absolute weight magnitude or a normalized
version thereof (like e.g. the LAMP score [13]). We compared several
variations of importance score functions in the global threshold approach,
namely (i) the absolute weight magnitude, (ii) the absolute weight magnitude
normalized by the L2 norm of the corresponding layer, (iii) the LAMP score
(Table 3). We initally observed that the global magnitude criterion led to
much worse accuracy comprared to the normalized criteria (Table 3). This
effect was found to be caused by the fusing of the BatchNorm layers into
preceding convolutions, which was performed in the model prior to compression.
BatchNorm fusing resulted in different layer-wise weight scales compared to
the original model, an effect easily counteracted by per-layer normalization
of weight magnitudes. In the case where the normalization layers were not
fused into convolutions, however, we found that the vanilla global magnitude
criterion performed the best compared to LAMP and L2-normalized magnitude
(Table 3 and Figure 3). We further assumed that the fusing could generally
occur prior to model compression and the original normalization layer
parameters might be unknown, hence we picked the per-layer L2-normalized
magnitude criterion as our sparsity rate selection heuristic. It performed
better than LAMP in our post-training scenario on most of the models with
BatchNorm fusing. The weight importance criterion for the $i^{th}$ weight in
the $l^{th}$ layer $w_{i}^{l}$ we use in our pipeline thus reads

$I(w^{l}_{i})=\frac{|w_{i}^{l}|}{\sqrt{\sum_{j\in l}|w_{j}^{l}|^{2}}}$

We pool the importance scores from all the layers and find the threshold value
corresponding to the set sparsity rate. The weights with importance values
below the threshold are pruned.

### Weight and activation bias correction

Once the layer-wise pruning rates have been determined, the weights are zeroed
out based on the intra-layer absolute magnitudes. This pruning operation
distorts the weight distribution, introducing bias and scale shifts. It is
beneficial to carry out a bias correction procedure on the weights in order to
restore the original mean and variance values in all of the convolutional
layer filters and fully-connected layer weight matrices [1]. We perform the
following affine transformation on all of the pruned weight tensors in a per-
channel/per-feature fashion:

$W^{s}_{corr}=\lambda W^{s}+E(W_{dense})-E(\lambda W^{s})$
$\lambda=\frac{\sigma(W_{dense})}{\sigma(W^{s})+\epsilon}$

where $W^{s}_{corr}$ is the weight tensor after the correction procedure, and
$W_{s}$ and $W_{dense}$ are the weight tensors of sparse and original dense
models, respectively, and $E$ and $\sigma$ are the mean and standard deviation
operators, $\epsilon=10^{-9}$ is a small constant added for numerical
stability. The resulting sparse weight tensor has the same mean and variance
values as original dense model weights for each output kernel/feature, since
this correction is applied to every output feature independently. Output
activations at each pruned layer are also suffering from a bias introduced by
the zeroed weights, which can be compensated by altering the bias parameters
of the convolutional and fully-connected layers. Nagel et al. [18] proposed to
perform this operation to mitigate biases introduced by quantization in an
iterative fashion, correcting the first layer and then calculating the bias
shift factors for the second layer using this corrected model. We found that a
one-shot version of the bias correction procedure was sufficient for post-
training sparsity, whereby we perform a forward pass of the original model and
calculate the input activation tensors $X_{dense}$ for each layer. The
corrected bias parameters are then determined as

$b_{corr}=b_{dense}+E(f(W_{dense},X_{dense}))-\\\
E(f(W^{s}_{corr},X_{dense}))$

where $f(W,X)$ is the convolutional or matrix-multiply operation of the layer
acting on inputs $X$ with weights $W$, $b_{dense}$ are the original bias
values in the layer, $X_{dense}$ is the set of input activation tensors for
the corresponding layer in the original dense model. In other words, we are
using the input tensors from the original model to calculate bias shifts, not
from the iteratively corrected compressed model. We found no significant
difference in the resulting accuracy between the two approaches, with the one-
shot one being faster since it requires a single forward pass of the model.
Results of the weight & activation bias correction procedures are shown in
Table 4 for a ResNet18 model at 50% sparsity rate. Both procedures
cumulatively improve the pruned model accuracy and top@1 accuracy drops are
not exceeding several percent for many ImageNet models at the sparsity rate of
50% just after layer-wise sparsity selection and bias correction. Accuracy can
be further improved by local layer-wise fine-tuning using auxiliary knowledge-
distillation losses, which is described in more detail below.

### Local layer-wise fine-tuning with auxiliary losses

Figure 4: Schematic description of the layerwise fine-tuning approach for
post-training sparse model calibration. Input and dense model output tensors
are pre-computed and stored in memory for each tuned layer. The red arrows
depict the local flow of gradients during weight and bias optimization. Red
pixels indicate sparsity masks in the compressed layers (sparsity levels are
individually selected for each layer).

Gradient-based fine-tuning with auxiliary loss functions was previously
successfully applied for post-training quantization [17, 15, 9] and, to a
smaller extent, to post-training weight pruning [8] and even filter pruning in
convolutional networks [5]. In this work, we follow a similar approach whereby
we define a local knowledge distillation loss for every pruned layer (see
Figure 4). These losses serve as a measure of how close the output activation
feature maps of the original (unpruned) and pruned layers are. Suppose the
pruned layer weights and biases are $W^{s}$ and $b^{s}$, then the knowledge
distillation mean-squared error loss for that layer is defined as

$L=\sum_{i\in batch}(Y^{i}_{dense}-f(W^{s}M^{s},X^{i}_{dense})-b^{s})^{2}\\\
Y^{i}_{dense}=f(W_{dense},X^{i}_{dense})$

where $f(X,W)$ is the convolutional/matrix-multiply operation represented by
the layer with weights $W$ acting on inputs $X$. The input tensors $X_{dense}$
used to calculate the output activations above are constructed by running a
forward pass of the original, unpruned model. $M^{s}$ is the binary mask layer
which is equal to one if the corresponding weight is not pruned and zero
otherwise. We fix the sparse binary mask and run a gradient descent of the
loss functions defined above for each layer independently to find the optimal
weights and biases $W^{s}$, $b^{s}$.

### Ablation study

Layer-wise fine-tuning settings. We run several ablation experiments to
establish the best optimization settings for the layer-wise fine-tuning
procedure, since it is inherently different from full model training via
backpropagation. We used a batch size of 50 samples in our experiments, and
found the optimal learning rate values across different models to be $10^{-5}$
for weights and $10^{-4}$ for bias parameters. We found that using the Adam
optimizer outperforms alternatives, such as SGD with momentum or Adadelta, and
techniques for better generalization in the vicinity of local minima, like
Lookahead [22] and Stochastic Weight Averaging [10] were also not found to be
beneficial in the layer-wise fine-tuning case. The MSE loss function also was
found to be a better choice than e.g. L1 loss, Huber loss or cosine similarity
between feature maps. We did not observe significant over-fitting present in
layer-wise optimization (we discuss this phenomenon in more details below) and
in particular we found that even low values of weight decay/L2 weight
regularization strength such as $10^{-6}$ could hurt the resulting model
accuracy (see Table 5). Thus, we set the weight decay strength to 0 in all our
experiments. Increasing model sparsity rate using a cubic schedule throughout
the pruning pipeline also turned out to improve accuracy for most models
compared to the constant sparsity baseline (Table 6). Overall, we were able to
prune and quantize a wide range of models with resulting sparsity rates
ranging from 40% to 70% and an absolute accuracy drop not exceeding or close
to 1% with our layer-wise fine-tuning recipe using images from the respective
models’ training datasets (Table 1 and Figure 2).

Table 4: Impact of bias & variance correction for weights and activations on a ResNet18 model on ImageNet with 50% of the weights pruned. ResNet18 50% sparse |  Top@1 accuracy |  Top@5 accuracy
---|---|---
L2-normalized magnitude |  64.856 |  86.126
L2-normalized magnitude |  |
(+ act. bias correction) |  66.852 |  87.438
L2-normalized magnitude |  |
(+ act. & weight bias correction) |  67.46 |  87.794
Table 5: Impact of L2 weight regularization on the fine-tuned model accuracy for a ResNet18 model at 50% sparsity on ImageNet. Even small weight decay values result in significant accuracy loss compared to the baseline with no regularization in place. L2-reg. strength | Top@1 / Top@5 accuracy, %
---|---
$\lambda=$ 0.0 | 68.97 / 88.77
$\lambda=$ 1e-6 | 67.78 / 87.96
$\lambda=$ 1e-5 | 38.14 / 64.49

Source of input data used for fine-tuning. Throughout experiments, we noticed
that the set of input samples to be used for fine-tuning does not have to be
necessarily large (we used a pool of randomly selected several hundred samples
in our experiments) and can come either from the training or the validation
dataset, with no significant accuracy difference between the two (see Table
2). These results suggest that this fine-tuning regime is not as prone to
over-fitting compared to full model training, a fact that was also previously
reported for layer-wise tuning of a quantized model [9]. We observed no
difference between fine-tuning on a batch of training or validation samples
not only for the ImageNet dataset but also for object detection models trained
on the Pascal VOC, COCO and WIDER FACE datasets. This lack of over-fitting is
not surprising since no annotation is used during fine-tuning and all the
layers are optimized independently, which reduces the amount of tuned
parameters per single optimization problem. The amount of supervision signal
is also high because the difference between whole activation tensors produced
by a set of input samples is used as a loss function. We further verified
whether we could utilize arbitrary input data for bias correction and layer-
wise fine-tuning, not related to the original dataset that the model has been
trained and tested on. The intuition behind this is that once the output
activation feature maps produced by these arbitrary data are similar to the
ones produced by running model inference on its original dataset, the layer-
wise fine-tuning procedure could produce a model that is sufficiently accurate
on the validation data. In particular, we tested several computer vision
models trained on different datasets (ImageNet, Pascal VOC, COCO, WIDER FACE;
see Table 2); the models were pruned using our post-training pipeline, but the
input images used to calculate activation statistics and feature maps for
fine-tuning consisted of synthetically generated white noise (each pixel value
in every color channel is independently sampled from a uniform distribution
from 0 to 255). We observed certain accuracy degradation when fine-tuning on
white noise images compared to tuning on original data, but typically not
exceeding several percent. We further tested whether these results could be
improved by using synthetic images producing activation distributions closer
to those generated by natural images in corresponding datasets. We took images
from the FractalDB-1k dataset [11], which is comprised of automatically-
generated grayscale images of fractals. These images and their generated
annotation were used to pre-train strong backbones for computer vision,
including Vision Transformers [11, 19]. We found that using these fractal
images as input samples to computer vision models during post-training weight
pruning significantly improves the resulting model accuracy compared to the
white noise baseline (Table 2). We took the original 512x512 images from
FractalDB-1k, randomly colored them by performing random shift-scale
operations on the color channels and used the same pre-processing strategy as
for the original datasets that the models were trained on. Overall, we were
able to achieve an accuracy degradation of absolute 1-3% at 50% sparsity rates
in the data-free pruning regime by using synthetically-generated fractal
images as model inputs. The results generalized beyond ImageNet to other
natural image datasets like Pascal VOC, COCO and WIDER FACE. Random
colorization of FractalDB images consistently yielded better accuracy compared
to using the (original) grayscale images (Table 7). The proposed data-free
pruning approach leads to better accuracy values compared to the existing
state-of-the-art [8] and is also fast and less restrictive since it does not
include a resource-consuming data distillation process that relies on
backpropagation through the model graph.

Table 6: Impact of the sparsity schedule vs. constant sparsity throughout fine-tuning. All metrics are reported at 50% sparsity rates. The cubic schedule was initialized at 10% sparsity rate which was increased in 10 iterations. The same number of optimizer steps was used for both fine-tuning modes. Model |  Top@1 accuracy w/o schedule |  Top@1 accuracy with schedule
---|---|---
ResNet18 |  68.76 |  68.91
ResNet50 |  75.43 |  75.60
GoogleNetV4 |  79.37 |  78.10
Table 7: Accuracy of models pruned in the post-training regime using different types of synthetic data: randomly-colored FractalDB1k images, (original) grayscale FractalDB-1k, and generated white noise images. Note that colorization of FractalDB images leads to increased resulting accuracy in most models. Model (sparsity rate, dataset/acc. metric) |  FractalDB-1k(c) |  FractalDB-1k |  White noise
---|---|---|---
ResNet18 (50%; ImageNet top@1) |  68.27 |  67.94 |  66.90
ResNet50 (50%; ImageNet top@1) |  74.50 |  74.46 |  73.89
MobileNetV2 (40%; ImageNet top@1) |  68.94 |  68.47 |  66.84
MobileNetV1-SSD (50%; VOC07 mAP) |  71.13 |  70.79 |  69.52
TinyYOLOv2 (50%; COCO AP) |  28.18 |  28.28 |  27.10

##  4 Conclusion

In this work, we have presented a novel post-training pruning recipe for deep
neural networks that allows zeroing out a significant proportion of model
weights without significant accuracy drops. We demonstrated efficiency of the
proposed pipeline on ImageNet models, object detection models on Pascal VOC
and COCO datasets as well as deep NLP and recommendation models. We proposed a
data-free formulation of the method by using synthetic fractal images to
compress computer vision models, which led to state-of-the-art results in
data-free weight pruning. We demonstrated that the proposed pruning method can
also be safely combined with post-training quantizaton, further increasing its
applicability in production settings.

## References

  * [1] R. Banner, Y. Nahshan, E. Hoffer, and D. Soudry.  Post-training 4-bit quantization of convolution networks for rapid-deployment.  arXiv preprint arXiv:1810.05723, 2018.
  * [2] D. Blalock, J. J. G. Ortiz, J. Frankle, and J. Guttag.  What is the state of neural network pruning?  arXiv preprint arXiv:2003.03033, 2020.
  * [3] E. Elsen, M. Dukhan, T. Gale, and K. Simonyan.  Fast sparse convnets.  In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 14629–14638, 2020.
  * [4] T. Gale, E. Elsen, and S. Hooker.  The state of sparsity in deep neural networks.  arXiv preprint arXiv:1902.09574, 2019.
  * [5] H. Guan, X. Shen, and S.-H. Lim.  Wootz: A compiler-based framework for fast cnn pruning via composability.  In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 717–730, 2019.
  * [6] C. Guo, B. Y. Hsueh, J. Leng, Y. Qiu, Y. Guan, Z. Wang, X. Jia, X. Li, M. Guo, and Y. Zhu.  Accelerating sparse dnn models without hardware-support via tile-wise sparsity.  arXiv preprint arXiv:2008.13006, 2020.
  * [7] Y. He, J. Lin, Z. Liu, H. Wang, L.-J. Li, and S. Han.  Amc: Automl for model compression and acceleration on mobile devices.  In Proceedings of the European Conference on Computer Vision (ECCV), pages 784–800, 2018.
  * [8] M. Horton, Y. Jin, A. Farhadi, and M. Rastegari.  Layer-wise data-free cnn compression.  arXiv preprint arXiv:2011.09058, 2020.
  * [9] I. Hubara, Y. Nahshan, Y. Hanani, R. Banner, and D. Soudry.  Improving post training neural quantization: Layer-wise calibration and integer programming.  arXiv preprint arXiv:2006.10518, 2020.
  * [10] P. Izmailov, D. Podoprikhin, T. Garipov, D. Vetrov, and A. G. Wilson.  Averaging weights leads to wider optima and better generalization.  arXiv preprint arXiv:1803.05407, 2018.
  * [11] H. Kataoka, K. Okayasu, A. Matsumoto, E. Yamagata, R. Yamada, N. Inoue, A. Nakamura, and Y. Satoh.  Pre-training without natural images.  In Proceedings of the Asian Conference on Computer Vision, 2020\.
  * [12] A. Kusupati, V. Ramanujan, R. Somani, M. Wortsman, P. Jain, S. Kakade, and A. Farhadi.  Soft threshold weight reparameterization for learnable sparsity.  In International Conference on Machine Learning, pages 5544–5555. PMLR, 2020.
  * [13] J. Lee, S. Park, S. Mo, S. Ahn, and J. Shin.  A deeper look at the layerwise sparsity of magnitude-based pruning.  arXiv preprint arXiv:2010.07611, 2020.
  * [14] B. Li, B. Wu, J. Su, and G. Wang.  Eagleeye: Fast sub-net evaluation for efficient neural network pruning.  In European Conference on Computer Vision, pages 639–654. Springer, 2020.
  * [15] Y. Li, R. Gong, X. Tan, Y. Yang, P. Hu, Q. Zhang, F. Yu, W. Wang, and S. Gu.  Brecq: Pushing the limit of post-training quantization by block reconstruction.  arXiv preprint arXiv:2102.05426, 2021.
  * [16] X. Liu, W. Li, J. Huo, L. Yao, and Y. Gao.  Layerwise sparse coding for pruned deep neural networks with extreme compression ratio.  In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 4900–4907, 2020.
  * [17] M. Nagel, R. A. Amjad, M. Van Baalen, C. Louizos, and T. Blankevoort.  Up or down? adaptive rounding for post-training quantization.  In International Conference on Machine Learning, pages 7197–7206. PMLR, 2020.
  * [18] M. Nagel, M. v. Baalen, T. Blankevoort, and M. Welling.  Data-free quantization through weight equalization and bias correction.  In Proceedings of the IEEE/CVF International Conference on Computer Vision, pages 1325–1334, 2019.
  * [19] K. Nakashima, H. Kataoka, A. Matsumoto, K. Iwata, and N. Inoue.  Can vision transformers learn without natural images?  arXiv preprint arXiv:2103.13023, 2021.
  * [20] S. P. Singh and D. Alistarh.  Woodfisher: Efficient second-order approximation for neural network compression.  Advances in Neural Information Processing Systems, 33, 2020.
  * [21] S. Srinivas and R. V. Babu.  Data-free parameter pruning for deep neural networks.  arXiv preprint arXiv:1507.06149, 2015.
  * [22] M. R. Zhang, J. Lucas, G. Hinton, and J. Ba.  Lookahead optimizer: k steps forward, 1 step back.  arXiv preprint arXiv:1907.08610, 2019.
  * [23] M. Zhu and S. Gupta.  To prune, or not to prune: exploring the efficacy of pruning for model compression.  arXiv preprint arXiv:1710.01878, 2017.