《Communications of the ACM》：Technical Perspective: Making Equality Saturation Usable for Developing Vectorized Compilers
编辑推荐：
```section id="bodymatter" data-extent="bodymatter" property="articleBody" typeof="Text">
利用加速器实现领域特定的专业化是提升现代计算系统性能和能效的主要技术。毫不奇怪，如今的计算系统正变
```section id="bodymatter" data-extent="bodymatter" property="articleBody" typeof="Text">
利用加速器实现领域特定的专业化是提升现代计算系统性能和能效的主要技术。毫不奇怪，如今的计算系统正变得越来越异构化。这些系统也越来越具有并行性（即多个任务可以在不同的核心或处理器上同时执行），并且在许多情况下还具备向量化特性，这是一种特殊的并行形式，其中相同的操作被应用于多个数据项上。图形处理单元（GPU）就是这种特性的典型代表。如今，常见的笔记本电脑会配备多种加速器，如GPU、张量核心、专用视频处理单元和神经处理引擎。即使是小型物联网（IoT）设备也通常包含多种定制加速器。
然而，将加速器集成到计算系统中只是提高性能和能效的一个方面。如果我们想充分利用这些加速器及其底层硬件，关键任务是为每种硬件开发专门的编译器。为新的硬件目标开发高性能编译器具有挑战性，因为这需要制定一系列重写规则来进行后端优化以及指令选择。
专家们通常需要花费大量的人力（以“人月”为单位）来手动制定这些重写规则。除了制定规则外，专家们还需要设计启发式方法来确定这些规则的应用顺序，这通常被称为“阶段排序问题”。由于重写规则在优化过程中会“破坏”原有程序，因此探索不同的规则应用顺序意味着需要进行多次编译。一种能提升某个程序性能的规则顺序可能会降低另一个程序的性能。
一个有趣的想法是非破坏性地将所有重写规则应用于程序，通过创建等价类来探索所有可能生成的程序，然后根据特定目标的成本指标（如代码大小或运行时性能）选择最优方案。等价性饱和是一种实现这一想法的方法，它利用了一种称为e-graph的巧妙数据结构来避免阶段排序问题。等价性饱和是一种很有吸引力的程序优化方法，但在存在规范化程序的规则（例如结合律和交换律）的情况下，等价类的数量以及用于等价性饱和的e-graph数据结构的大小可能会显著增加。
本文的亮点在于它能够自动生成适用于特定类型加速器（如需要向量化执行的数字信号处理器）的重写规则，并利用等价性饱和技术。本文生成重写规则的方法非常巧妙：它利用目标指令集的规范以及一阶成本模型，通过现有的重写规则推理工具（如Ruler）来穷尽地枚举候选规则，并使这些工具具备向量化处理能力。简单的枚举方法可能会生成数百条规则，其中一些可能是错误的，或者无法改善目标指标（如代码大小或运行时性能）。本文通过成本模型筛选掉不合适的规则，并利用可满足性模理论求解器来消除错误规则。这种方法是将程序合成技术应用于生成向量化重写规则的经典范例。
采用穷举搜索技术（如等价性饱和和重写规则合成）的方法在处理大型程序时存在常见的问题。一种常见的策略是提高抽象层次，然后采用分而治之的方法。本文通过将重写规则分为三类（优化规则、规范化规则和向量化规则），并对每一类分别应用等价性饱和技术来解决这一问题。
Santosh Nagarakatte（santosh.nagarakatte@cs.rutgers.edu）是美国新泽西州罗格斯大学计算机科学专业的教授和本科生项目主任。
```
