Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection

TL;DR

The paper addresses automatic generation of many-to-many instruction selection rewrite rules by formulating the problem as generalized component-based program synthesis ($\mathit{GCBPS}$) and solving it via SMT/CEGIS. It introduces two optimizations, $\mathit{genAll}$ and $\mathit{genAll}_{LC}$, to produce all unique rules and all lowest-cost rules, respectively, while excluding duplicates and composites through formal equivalence relations and cost-aware pruning. Empirical results across multiple ISAs show dramatic speedups (up to $\sim$ $768\times$ and $\sim$ $4004\times$) and demonstrate that most naive outputs are duplicates, composites, or high-cost rules. The approach yields compact, complete rule sets tailored to chosen cost metrics, enabling scalable automatic generation of instruction selectors for DSAs and ISA extensions. This work lays groundwork for broad automatic rule synthesis with potential integration of richer ISA features and relaxed loop-free constraints.

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 768x and 4004x for the two algorithms.

Figures (4)

• Figure 1: Iterative algorithm to generate all unique rewrite rules up to a given size.
• Figure 2: AllSAT algorithm to synthesize all unique rules. Line 8 excludes all rules that are duplicates of the current synthesized rewrite rule.
• Figure 3: Iterative algorithm to generate all lowest-cost rules. ISA multisets are ordered by cost. $\mathit{CEGISAll}\xspace$ is modified to exclude rules with duplicate IR programs.
• Figure 4: Cumulative synthesis time comparison for ISA 1b up to size 2-to-3.