Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware Architectures

文章标题：Hydride：一种面向现代硬件架构的可重定向、可扩展的基于综合的编译器
作者/机构：
Akash Kothari∗ (UIUC, USA)
Abdul Rafae Noor∗ (UIUC, USA)
Muchen Xu (UIUC, USA)
Hassam Uddin (UIUC, USA)
Dhruv Baronia (UIUC, USA)
Stefanos Baziotis (UIUC, USA)
Vikram Adve (UIUC, USA)
Charith Mendis (UIUC, USA)
Sudipta Sengupta (Amazon Web Services, USA)

A1 主要贡献

核心问题：随着现代硬件架构（如专用加速器和复杂向量扩展）的不断发展，以满足图像处理、深度学习等领域工作负载的性能需求，编译器面临着巨大挑战。特别是，像LLVM这样的可重定向编译器基础设施，其内部抽象和代码生成支持难以跟上新兴指令集（ISA）的演进速度。

研究挑战：
1. 设计目标无关的IR操作困难：为编译器IR设计一个新的目标无关操作，需要手动查阅数千页的多个硬件ISA文档，寻找通用指令类型（如多硬件目标上的点积指令），然后手动设计一个可降低到这些目标指令的目标无关指令。这个过程繁琐且耗时。
2. 代码生成实现困难：为每个硬件目标生成代码，需要费力地实现模式匹配代码，将目标无关指令序列转换为硬件指令。这需要大量的工程时间和精力来确保正确性，并且随着ISA规模和复杂度的增加而变得更加困难。
3. IR和代码生成支持的演进：编译器IR及其代码生成支持必须能够随硬件ISA自动演进，而目前的做法需要手动工程投入。

现有方法局限性：
* LLVM/GCC：通常通过实现映射到目标指令的目标特定内在函数（intrinsics）来绕过设计目标无关操作的难题，但这严重损害了可重定向性。它们不支持为复杂指令自动生成内在函数，并且其IR和代码生成支持无法随ISA自动演进。
* DSL编译器（如Halide）：由于LLVM IR的代码生成和优化支持无法自动为不同架构生成高效复杂的非SIMD和混洗（swizzle）指令，这些编译器为不同架构（x86, Hexagon, ARM等）使用独立的、目标特定的后端，生成目标特定的LLVM内在函数。这种方法为每个DSL编译器和每个目标重复了工程工作，效率低下、易错且难以维护。
* Vegen、Rake、Diospyros等：这些工具尝试解决部分问题，但存在局限性。例如，Vegen的模式匹配规则很脆弱且不支持关键的swizzle指令；Rake等基于程序综合的工具仅支持少量目标指令，扩展性差，且需要用户修改源代码。

本文方法（Hydride）：
本文提出了一种新方法，利用一个或多个硬件ISA的供应商规范，自动生成形式化定义的、语言无关和目标无关的LLVM IR操作（称为AutoLLVM IR），以及将AutoLLVM IR降低到每个目标特定指令集的指令选择过程。Hydride还包含一个代码合成器，可以自动为像Halide这样的调度型语言生成代码，以最优方式生成AutoLLVM IR。这种方法避免了脆弱的模式匹配，并使共享的编译器基础设施能够快速演进，同时实现近乎完整的硬件指令覆盖。

核心贡献：
* 自动设计编译器IR的新方法：提出了一种基于对多架构目标指令进行“相似性检查”的新技术，以自动设计一种语言无关和目标无关的编译器IR。
* 自动生成的编译器基础设施（Hydride）：构建了一个新的编译器基础设施Hydride，其中从DSL IR到目标特定指令的所有编译器阶段（前端IR到AutoLLVM IR的翻译、AutoLLVM IR操作、到目标特定LLVM内在函数的翻译）都是自动生成的。
* 可扩展的程序综合方法：提出了一种新颖且可扩展的综合方法，该方法利用目标指令的等价类，为输入子表达式分别创建综合语法，并结合针对复杂跨通道混洗（cross-lane swizzle）操作的综合策略，使得在Hydride中使用程序综合的时间成本变得合理。
* 全面评估：在x86、Hexagon和ARM架构上，使用来自图像处理和深度学习领域的各种核心（kernel）对该编译器进行了评估，且无需修改原始Halide源代码。结果表明，尽管编译器工程投入减少了几个数量级，但其性能与为Halide精心设计的生产级编译器相当。

A3 Hydride 概述

核心思想：Hydride的核心思想是利用硬件供应商定义的（多个）硬件ISA规范，自动生成其形式化语义，并通过推理不同ISA之间的相似性，自动设计或扩展一个使用参数化操作的形式化定义的、语言无关且目标无关的编译器IR。这一思想带来了几个关键能力：首先，硬件ISA的形式化语义使Hydride能够自动设计一个可随硬件ISA自动演进的可重定向编译器IR。其次，Hydride能够以比现有系统低几个数量级的工程投入，自动最大化对大型ISA的覆盖范围。第三，Hydride编译器IR的形式化语义使得语言前端可以使用程序综合技术自动地将其作为目标，并且为目标无关IR操作选择参数使得合成器能够生成高性能的目标特定指令序列；这些共同消除了在这些编译器中手动设计目标特定后端的需要。

工作流程：图1展示了Hydride的工作流程。Hydride分为两个阶段：离线阶段和在线阶段。在离线阶段，Hydride自动IR生成器（第3节）使用硬件供应商提供的ISA伪代码规范，自动为LLVM编译器IR生成语言无关的指令及其语义，我们称之为AutoLLVM IR。我们将这些新操作定义为LLVM内在函数，以避免修改现有的LLVM遍（passes）。在在线阶段（即编译时），Hydride的代码合成器（第4节）使用语法指导的综合技术，将输入的Halide程序代码从Halide前端的IR翻译成AutoLLVM IR。

A2 方法细节

Hydride的自动IR生成器

基于ISA语义的指令相似性分析：Hydride自动IR生成器使用硬件ISA语义来寻找相似的指令。其核心思想是，来自一个或多个机器指令集（ISA）的相似指令可以被分组到一个（参数化的）等价类中，并表示为一个带有符号参数的机器无关IR操作。通过为这些参数赋予不同的具体值，可以表示等价类中的不同成员，即不同的机器特定指令。这也意味着目标特定的后端指令选择器只需要进行近乎简单的一对一翻译。Hydride并非要求手动为每个硬件ISA指定形式化的ISA语义（相似性检查所需），而是从硬件供应商已在其各自程序员手册中指定的指令集伪代码规范中自动生成ISA语义。这些规范来自英特尔的【13. Intel Intrinsics Guide. https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html, 2023.】，高通的【18. Qualcomm Hexagon V66 HVX Programmer’s Reference Manual. https://developer.qualcomm.com/downloads/qualcommhexagon-v66-hvx-programmer-s-reference-manual, 2022.】，以及ARM的【2. ARM Developer Intrinsics. https://developer.arm.com/architectures/instructionsets/intrinsics/f:@navigationhierarchiessimdisa=[Neon].】。图3展示了英特尔x86指令的此类规范示例。Hydride使用我们编写的特定于ISA的解析器来解析这些规范，并将其翻译成形式化的、机器可执行的ISA语义，然后利用这些指令语义进行相似性检查 。

图2. x86中相似交错指令的示例。

3.1 相似指令和等价类

相似指令的直观定义：Hydride认为两个指令是相似的，如果它们在抽象掉目标特定的数值属性（如元素位宽、向量长度、移位因子、位偏移等）后，执行等效的计算和/或等效的数据移动。例如，x86指令_mm512_add_epi16操作512位寄存器和16位元素，而_mm256_add_epi8操作256位寄存器和8位元素。两者本质上都执行相同的计算：元素级向量加法。因此，这些指令被认为是相似的。

参数化等价的表达能力：等价的参数化在实践中可以非常富有表现力。图2展示了一个更复杂的相似指令示例。这些交错混排（interleave shuffles）指令通常用于改变数据布局（例如，执行矩阵转置），通过将输入向量寄存器通道中不同偏移量的数据交错排列。尽管两个指令的向量大小、元素大小、被交错的元素窗口大小以及窗口内的偏移量都不同，但数据移动模式是相似的；在主要分析数据布局模式时，可以抽象掉指令特定的数值量和细节，从而认识到它们的相似性。

相似指令的形式化定义：现在我们形式化定义和寻找相似指令的过程。假设一个指令 $I$ 具有操作语义 $\Phi(I, \vec{p}_{num})$，该语义依赖于数值参数 $\vec{p}_{num} = p_1 \cdots p_n$。例如，_mm512_add_epi16 有两个数值参数，$p_1 = 16$（元素大小），$p_2 = 512$（向量大小）。我们通过将数值参数替换为相应的符号参数 $\vec{p}_{sym} = s_1 \cdots s_n$ 来构建 $I$ 的参数化（符号）操作语义，记为 $\Sigma(I, \vec{p}_{sym})$，更正式地表示为 $\Sigma(I, \vec{p}_{sym}) = \Phi(I, \vec{p}_{num})|_{p_i/s_i, 1 \le i \le n}$。

相似性判定：我们定义两个指令 $I$ 和 $J$ 是相似的，如果它们的语义具有相同数量的数值参数（即 $|\vec{p}_{num}^I| = |\vec{p}_{num}^J|$），并且两个指令的参数化操作语义是等价的，即对于相同的具体数值参数值，$\Sigma(I, \vec{p}_{sym}) \equiv \Sigma(J, \vec{p}_{sym})$。例如，当将_mm512_add_epi16的数值参数 $p_1=16$ 和 $p_2=512$ 替换到_mm256_add_epi8的数值参数 $p_1$ 和 $p_2$ 中时，可以使用可满足性模理论（SMT）求解器验证它们的操作语义是等价的。同样，当将_mm256_add_epi8的数值参数（$p_1=8$ 和 $p_2=256$）替换到_mm512_add_epi16的参数中时，它们的操作语义也被认为是等价的。第3.3节描述了寻找相似指令的算法。

等价类与AutoLLVM IR的构建：对于一个或多个目标硬件ISA，Hydride构建了这些ISA中所有机器指令的等价类，使得两个指令 $I, J$ 当且仅当 $\Sigma(I, \vec{p}_{sym}) \equiv \Sigma(J, \vec{p}_{sym})$ 时被分到同一个等价类。由于一个等价类中的所有指令都具有相同数量的参数，Hydride可以定义一个具有相同数量符号参数的目标无关指令来表示该类中的所有指令，例如 $O(\vec{s}_{sym})$。一旦Hydride计算出相似性，它就简单地构建相似指令的等价类，并为每个等价类以这种方式定义一个目标无关的IR操作 $O$。我们将由此产生的IR定义称为AutoLLVM IR。请注意，类中的每个目标特定指令 $I$ 都对这些符号参数有一个固定的数值赋值。因此，语言前端只需选择适当的数值参数值，就可以以优化的目标特定方式生成AutoLLTVM IR。或者，从符号化的 $O$ 到等价类中任何特定目标指令的机器代码生成，也仅需要选择适当的数值参数值。

3.2 Hydride IR生成器

Hydride IR表示：检查指令之间的相似性需要分析目标ISA指令的形式化语义（$\Phi(\cdot)$）及其抽象对应物（$\Sigma(\cdot)$）。这些指令的语义可以使用位向量和整数操作来表示【3. Isa semantics for armv8-a, risc-v, and cheri-mips. 2019.】。我们定义了一种名为Hydride IR的直接程序表示法来表示语义，并附带了IR上的几种转换，包括循环重卷（loop rerolling）、内联和常量传播，以及用于类型推断的数据流分析。

基于求解器的DSL：检查指令相似性需要证明语义的等价性。求解器辅助的DSL（SDSL）利用SMT求解器提供验证、综合和求解能力。因此，将Hydride IR定义为求解器辅助的DSL来表达形式化的、机器可执行的ISA语义在Hydride中非常有用。Hydride使用Rosette【26. Emina Torlak and Rastislav Bodik. Growing solver-aided languages with rosette. In Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software, pages 135–152, 2013.】来定义和实现Hydride IR，但对Rosette的综合引擎进行了一些改进以提高效率（第4节）。

从伪代码到Hydride IR：Hydride使用独立的解析器解析x86、ARM和HVX指令的伪代码规范（如图3(a)中的示例），并将它们翻译成以Hydride IR表示的语义。这种方法使Hydride能够最大化所支持指令的覆盖范围。

3.3 相似性检查引擎

Hydride IR代码的规范化：Hydride通过执行函数内联、循环重卷等操作来规范化Hydride IR，以确保所有指令的语义至少包含一个两层循环嵌套：一个外层循环用于表示对输入/输出向量寄存器通道的迭代，一个内层循环用于表示对给定通道中元素的迭代（如图3(b)中的示例）。这使得在抽象掉指令特定的量（如元素数量、元素大小、向量大小等）之前更容易识别它们。对于只有一个循环遍历向量元素的SIMD指令，此步骤会添加一个只有一次迭代的人工内层循环。

常量的提取：Hydride从Hydride IR中提取常量，以抽象掉任何指令特定的量，如向量大小、元素大小等。为确保不同参数的常量不被混淆，并确保如果两个位向量保证具有相同的位宽时其位宽不会被提取两次，Hydride遍历Hydride IR中的使用-定义链，并通过考虑位向量操作的合法性约束来执行简单的位宽分析。例如，如果IR代码包含 %c = bvadd %a, %b;，那么 %a, %b 和 %c 必须具有相等的位宽才能使位向量加法合法；因此，Hydride只提取其中一个的位宽一次。图3(c)显示了从高位交错指令的语义中提取为参数的常量。Hydride遍历每个具有语义 $\Phi(I, \vec{p}_{num})$ 的指令的Hydride IR，以提取常量 $\vec{p}_{num} = p_1 \cdots p_n$ 并生成符号语义 $\Sigma(I, \vec{p}_{sym})$。

等价性检查：由于在数千条指令之间天真地执行相似性检查需要数小时，Hydride使用以下标准来决定是否在两条指令之间执行相似性检查：
* IR函数中的参数数量必须相同。
* 位向量类型的参数数量必须相同。
* 整数类型的参数数量必须相同。
Hydride使用算法1来执行相似性检查。该算法显示了Hydride如何在每个等价类的代表性指令之间执行相似性检查，而不是在所有单个指令之间。在创建所有等价类之后，Hydride会执行下面讨论的进一步转换。

重新排序指令参数：像_mm512_mask_blend_epi8和_mm512_mask_mov_epi8这样的指令在语义上是等价的（输入和输出的向量长度相同，元素大小相同等），只是向量参数的顺序不同。因此，一旦通过执行算法1生成了等价类，Hydride会排列每个等价类代表函数的参数，并再次执行相似性检查，以便在它们被认为是等价的情况下合并等价类。

算法1 相似性检查引擎的算法

Input: List of canonicalized ISA semantics in Hydride IR ISA_Sema
Output: Set of equivalence classes EqClasses

function RunSimilarityCheckingEngine(ISA_Sema)
    EqClasses ← A set of Equivalent classes generated by Hydride
    SymSema ← ExtractConstants(ISA_Sema) // 产生符号化语义
    EqClasses ← {}
    PerformEqChecking(SymSema, EqClasses) // 执行相似性检查
    PermuteArgs(EqClasses) // 排列EqClasses中函数的参数
    PerformEqChecking(SymSema, EqClasses) // 再次执行相似性检查
    RefineEqClasses(EqClasses) // 细化等价类
    SymSema ← ExtractConstants(ISA_Sema) // 再次产生符号化语义
    PerformEqChecking(SymSema, EqClasses) // 再次执行相似性检查
    EliminateUnnecessaryArgs(EqClasses) // 消除无用参数
    return EqClasses
end function

function PerformEqChecking(SymSemanticsList, EqClasses)
    for all InstSema1 in SymSemanticsList do
        for all InstSema2 in SymSemanticsList do
            if InstSema1 != InstSema2 then
                // 使用SMT求解器在符号化输入上验证等价性
                if verifyEquivalence(InstSema1, InstSema2) == true then
                    EqClasses ← EqClasses ∪ InstSema1 ∪ InstSema2
                end if
            end if
        end for
    end for
end function

LATEX_INLINE_22
LATEX_INLINE_23
LATEX_INLINE_24
LATEX_INLINE_25
LATEX_INLINE_26
LATEX_INLINE_27

细化等价类：图2中两个指令的输入向量元素访问模式是相似的：唯一的区别在于提取输入向量中元素时所在通道的偏移量不同，即_mm256_unpackhi_epi16的偏移量是0，而_mm512_unpacklo_epi8的偏移量是2。Hydride的提取操作从向量中提取位片，其低位和高位索引的操作数决定了从向量中提取的切片的坐标。对于_mm512_unpacklo_epi8，通道内的偏移量可以通过在输入向量的提取操作的低位索引上加2来表示（高位索引由于表示为low_index + bitwidth - 1而已被处理）；然而，对于_mm256_unpackhi_epi16，由于偏移量为0，因此不需要这样的加法（图3(b)）。为了让Hydride捕捉到这两个指令访问模式的相似性，Hydride在_mm256_unpackhi_epi16的语义中插入一个“空洞”（hole），以在低位索引上进行加法，以弥补缺失的操作；代表这种空洞的hole.grammar函数在图3(e)中定义和调用。基于这个定义，Hydride合成一个关于内外循环迭代器、低位索引和小于位向量长度的常量值的空洞表达式。在这种情况下，Hydride合成一个加法操作，将%low.i与0相加——这个常量被提取出来，然后再次执行相似性检查（算法1），这次这两个指令被认为是相似的。这种技术也可以处理其他访问模式，如跨步访问模式。

消除不必要的参数：在检查相似性之前，Hydride会保守地从语义中提取所有常量，这导致了具有许多参数的复杂函数签名。然后，Hydride通过遍历所有等价类中的所有指令，并消除在等价类中所有指令都具有相同具体值的参数，来修正这些签名。

结果总结：通过使用所有这些技术，Hydride的相似性检查引擎为2,029个x86标量和向量指令生成了136个等价类，为1,221个ARM指令生成了177个类，为307个HVX指令生成了115个类（表1）。Hydride为x86、ARM和HVX指令组合（总共3,557个硬件指令）形成了397个等价类。详细结果见第6.2节。

3.4 AutoLLVM IR 指令

AutoLLVM IR指令的生成：Hydride使用相似性引擎生成的等价类来为AutoLLVM生成指令，这些指令实现为LLVM内在函数【24. The LLVM Project. LLVM Language Reference Manual. https://llvm.org/docs/LangRef.html, 2022.】。这些是带有参数的可重定向指令，参数代表被抽象的常量，这样每个（常量）参数值的组合都会生成等价类中的一个特定的目标特定指令。Hydride IR中函数的签名被用来生成AutoLLVM内在函数的签名，不同之处在于向量类型信息（如元素数量和每个元素的大小）被折叠到LLVM向量类型中。Hydride自动生成一个包含所有AutoLLVM内在函数定义的LLVM TableGen文件。这些AutoLLVM内在函数中的每一个都可以重定向到它所代表的等价类中的目标特定指令。下面显示了在x86上编译矩阵乘法内核时生成的AutoLLVM IR向量交错和点积指令示例。

%0 = call <32 x i16> @autollvm.interleave(<16 x i16> %arg1, <16 x i16> %arg3, 0 /* lane offset */)
%1 = call <32 x i16> @autollvm.interleave(<16 x i16> %arg2, <16 x i16> %arg4, 8 /* lane offset */)
%2 = call <32 x i16> @autollvm.dotproduct(<32 x i16> %arg0, <32 x i16> %0, <32 x i16> %1)

基于模式匹配的目标特定代码生成器：Hydride代码生成器会自动生成简单的、一对一的模式匹配规则，将AutoLLVM IR指令翻译成LLVM IR中已有的目标特定内在函数。Hydride能够做到这一点，是因为它跟踪了所有被抽象掉以形成AutoLLVM IR指令的指令特定量的原始值。例如，这有助于为上面显示的AutoLLVM IR代码生成x86指令，如表3第2行所示。

3.5 低级代码生成器

低级代码生成器组件：该组件使Hydride能够利用来自相似性检查引擎的关于相似指令（架构间和架构内）的信息，自动生成部分代码生成支持。代码生成器包括以下组件。

Rosette到LLVM转换器：Hydride的代码合成器（第4节）合成的代码是Rosette代码，其中目标无关的指令表示为不透明的函数调用。Rosette到LLVM转换器将合成的代码翻译成AutoLLVM IR指令。

Hydride代码合成器

功能概述：Hydride代码合成器是Hydride的第二个主要组成部分。它能够自动生成一个到AutoLLVM指令的前端转换器，从而消除了前端编译器中对目标特定后端的需要。它利用了Hydride相似性检查引擎生成的AutoLLVM IR语义。

Halide原型和与Rake的比较：我们为Halide DSL设计了一个原型前端，使用Hydride创建了一个从Halide到LLVM的编译器。与Rake【1. Maaz Bin Safeer Ahmad, Alexander J Root, Andrew Adams, Shoaib Kamil, and Alvin Cheung. Vector instruction selection for digital signal processors using program synthesis. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1004–1016, 2022.】类似，我们的前端接收从输入Halide程序降低并应用了所有调度优化（包括向量化、并行化和分块）后的Halide IR，并合成一个等效的目标特定程序。然而，Hydride在两个对实际使用非常重要的方面对Rake进行了重大改进。首先，Hydride从数千个潜在的ISA操作中合成等效的目标程序，而不仅仅是少数几个。Hydride离线阶段的结果对于使综合足够可扩展以实现这一点至关重要，这体现在两个方面：（1）自动生成目标特定和AutoLLVM指令语义对于支持像x86和ARM这样拥有数千条指令的大型指令集至关重要。（2）离线阶段的相似性检查结果有助于识别“可能相关的指令”，然后通过利用它们的相似性来修剪这些指令子集。其次，与Rake相比，Hydride在输入Halide代码中探索了更大的表达式深度，这使得它能够自动生成像点积这样的复杂非SIMD操作，而不需要像Rake那样手动更改Halide源程序中的算法。

4.1 自动生成的综合框架

SyGuS框架的构建：为了执行综合，Hydride的代码合成器使用自动生成的AutoLLVM指令字典，在Rosette中创建一个语法指导的综合（SyGuS）框架。Rosette的SyGuS功能要求用户提供输入和输出语言的形式化语义、一个输入程序以及输出程序的语法。然后，综合算法在语法中搜索一个与输入程序等价的候选程序。重要的是，这个合成器完全独立于目标ISA和源语言（即它不是Halide特有的）：目标细节由字典捕获，源语言由语言语义捕获，这两者都是合成器的输入。利用这些输入，它在离线阶段自动生成多个组件：
* 解释器：在Rosette中实现由Hydride的IR生成器定义的AutoLLVM IR操作的操作语义；这些语义在综合过程中使用。
* 成本模型：定义了一个成本模型，该模型将AutoLLVM IR表达式映射到一个整数成本值，使用表达式中各个指令延迟的简单总和。
* 语法生成器：为输入程序中的每个子表达式生成一个驱动SyGuS方法的语法。该语法仅包含可能相关的AutoLLVM IR指令，以使综合成本可控。语法使用有界的、参数化的深度来确保可扩展性（第4.3节）。
* 备忘录缓存：记录每个输入表达式的综合结果，以便重用。

4.2 综合策略

CEGIS方法：Hydride使用我们为其添加的“反例引导的归纳综合”（CEGIS）【22. Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. Sketching concurrent data structures. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’08, page 136–148, 2008.】能力，将Halide IR操作编译为AutoLLVM IR，同时最小化一个目标成本函数。Halide IR程序首先使用来自Rake的Halide IR语义【1. Maaz Bin Safeer Ahmad, Alexander J Root, Andrew Adams, Shoaib Kamil, and Alvin Cheung. Vector instruction selection for digital signal processors using program synthesis. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1004–1016, 2022.】，被降低为Rosette中的等价表达式。为保持综合的可行性，Hydride从Halide IR程序中提取有界深度的子表达式（我们称之为窗口），并合成AutoLLVM IR中的等价代码。窗口大小和最大输出序列大小是Hydride的参数。Hydride在搜索最小成本表达式时，会逐步增加输出序列的大小（即综合语法的深度）。这使得Hydride倾向于选择更短的指令序列和执行时间更短的序列（通过对目标指令延迟求和来估计）。此外，Hydride利用AutoLLVM IR的参数化特性，对综合过程中的向量ISA通道数进行统一缩放（而非截断）。求解器的时间复杂度随位向量的大小呈指数增长，因此减小位向量的大小使得对于像HVX这样可以有2048位向量的目标，综合变得可行。

算法2 CEGIS用于编译单个表达式

Input: Grammar G, Specification Expr, CostModel C, ScaleFactor Sc
Output: Program Sol s.t. ∀x .Sol (x) = Expr(x) ∧ C(Sol) is minimized.

1: function Lanewise_Synthesis(G, Expr, C, Sc)
2:    ScaledExpr ← ScaleDown(Expr, Sc) // 缩小通道数
3:    // 创建初始的具体输入集合用于综合
4:    CEX ← {RandomInputs(ScaledExpr), RandomInputs(ScaledExpr)}
5:    Failing-Lanes ← {0, 0} // 在通道0上测试两个输入
6:    do
7:       Constraints ← EqualOnLane(G, ScaledExpr, CEX, Failing-Lanes)
8:       // 综合满足断言并最小化成本C的解
9:       Sol ← Synthesize(G, C, Constraints)
10:      if Sol = unsat then
11:         G' ← IncreaseGrammarDepth(G)
12:         return LANEWISE_SYNTHESIS(G', Expr, C, Sc)
13:      end if
14:      // 符号化验证，返回反例
15:      CEX' ← Verify(Sol, ScaledExpr)
16:      if CEX' ≠ {} then
17:         CEX ← CEX ∪ CEX'
18:         // Diff[i] = 1 if Sol(CEX’)[i] ≠ ScaledExpr(CEX’)[i], else 0
19:         Diff ← ComputeDifferences(Sol, ScaledExpr, CEX')
20:         Failing-Lanes ← Failing-Lanes ∪ GetFailingLanes(Diff)
21:      end if
22:   while CEX' ≠ {}
23:   if Verify(ScaleUp(Sol, Sc), Expr) = {} then
24:      return ScaleUp(Sol, Sc)
25:   end if
26:   return LANEWISE_SYNTHESIS(G, Expr, C, 1)

迭代综合过程：算法2展示了Hydride使用的迭代综合过程。在为表达式Expr调用此过程之前，Hydride会自动生成一个针对该表达式的剪枝后语法G，如第4.3节所述。从一组具体的种子输入（第4行）和用于验证等价性的输出向量通道（第5行）开始，Hydride生成约束，要求合成的程序仅在Failing-Lanes中的向量通道上产生与输入程序等价的输出。向量ISA中的一个常见范式是，计算模式在某些通道集合上重复：对于SIMD操作，模式在每个通道上重复；对于非SIMD操作，它每2、4等通道重复一次。Hydride利用这种重复性，通过在输出向量通道的子集上施加约束来合成程序，因为计算模式在向量通道的区间内重复。约束表示为断言（第7行）。然后Hydride合成在这些约束下与规范等价且最小化目标成本函数C的程序（第9行）。如果求解器返回不满足（第10行），Hydride会用更大的语法深度重新尝试综合（第12行）。否则，Hydride会用符号化输入联合验证合成程序与输入程序在所有通道上的等价性（第15行）。如果验证成功，则达到期望的解，算法退出综合循环（第6-22行）。否则，求解器返回一个反例（第16行）。对于验证器识别的任何反例，Hydride会识别出输出向量不同的失败通道（第19-20行），并将其附加到下一轮约束中。然后重复综合（从第6-22行的循环），并加入这些额外的约束。一旦表达式被合成，Hydride会将其放大回原来的规模（即增加向量通道数到原始数量），并验证其对规范的正确性。如果验证发现反例，Hydride会不进行缩放重复该过程（第26行）。

综合过程优化：因此，Hydride通过两种方式优化跨向量通道的综合过程：（1）仅在一部分通道上约束综合，然后在所有其他通道上验证合成的表达式。（2）为综合缩小AutoLLVM IR操作的向量通道数，这反过来减小了操作数和结果的位向量大小，然后将通道数放大回去。

4.3 剪枝后语法生成

剪枝的必要性：为像x86这样拥有数千条指令的大型ISA的给定输入表达式合成代码可能是难以处理的，因为综合具有双指数复杂性。因此，Hydride中另一个提高可处理性和加速综合的启发式方法是生成多个版本的剪枝后语法并并行综合；换句话说，生成多个具有不同AutoLLVM IR指令子集的较小语法，而不是一个完整的语法。以下步骤描述了如何生成剪枝后的语法。

剪枝步骤：
* (a) 基于操作类型和向量属性的剪枝：如果一个等价类（在第3.3节中描述）中的所有操作（例如，bvmul, bvadd）都与输入表达式中的任何操作不匹配，或者输入表达式中给定目标的任何指令使用的向量长度和元素大小都不被该等价类支持，Hydride会省略整个等价类。
* (b) 基于元素大小的剪枝：Hydride还消除了任何使用比输入表达式中最小元素大小更小的元素大小的指令，因为生成这样的指令会导致信息丢失。
* (c) 基于分数的指令选择：对于给定的输入表达式，一些可行的指令比其他指令更可能适用——这取决于匹配的位向量操作数量，以及指令的向量长度和元素大小是否与输入表达式匹配。满足上述属性越多的AutoLLTM IR操作被赋予越高的分数值。Hydride从每个等价类中选择得分最高的k个操作加入最终语法，其中k是Hydride代码合成器的参数（在我们的评估中，k在3-4之间）。这个启发式方法的理由是，一个等价类中的所有操作都执行相似的计算，所以Hydride只选择那些与输入表达式有最多共同点的操作。计算操作（如算术操作）的分布与类型转换操作（如广播、符号扩展或截断操作）相平衡。混排（Swizzle）操作（第4.4节）总是被独立于k而包含进来。

4.4 综合混排指令序列

专门化的混排模式：在为剪枝后的语法确定了可行的非混排指令后，Hydride向语法中添加专门的混排模式，而不是添加一个通用的排列操作，因为后者会导致综合变得难以处理。这种方法使得综合变得实用，并促进了更复杂的非SIMD向量操作的使用。Hydride支持以下混排模式：
1. 完全交错两个向量：交错两个相同大小向量的元素。
2. 交错/解交错单个向量：交错/解交错一个向量的前半部分和后半部分。
3. 交错两个向量的前/后半部分：交错两个相同大小向量的前/后半部分，并产生一个相同大小的向量。
4. 连接两个向量的前/后半部分：连接两个相同大小向量的前/后半部分，并产生一个相同大小的向量。
5. 向量右旋：右旋向量元素的顺序。

手动扩展：这些混排操作在现代硬件架构中很常见；然而，如果目标架构使用一种新颖的混排模式，则需要手动将其添加到Hydride中。

A4 实验环境

基准测试：
* 数据集：来自图像处理和深度学习领域的33个Halide基准测试。
* 调优：这些基准由我们为x86手动调优，由高通和Adobe为ARM和HVX调优。
* 用途：包括在大型语言模型中常见的低批量（1, 2, 4）张量上的矩阵乘法，以及在各种神经网络中常见的深度学习核心的融合版本（如平均/最大池化+加法），特别是在MLP块中（矩阵乘法+偏置+激活函数+矩阵乘法）。

硬件配置：
* x86：Intel Xeon Silver 4216 CPU（16核，2.1GHz，22MB L3缓存），禁用超线程。
* HVX：使用高通提供的Hexagon SDK v3.5.2中的周期精确模拟器。
* ARM：Apple M2 CPU（3.49GHz，16GB内存，16MB L3缓存）。

软件配置与对比基线：
* 对比对象：
1. 业界领先的、生产级的Halide目标特定后端【11. Halide. Halide. https://github.com/halide/Halide, 2021.】。
2. Halide的LLVM后端【14. Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, 2004. CGO 2004., pages 75–86. IEEE, 2004.】，在Halide生成的LLVM IR上应用了如循环向量化、超字级并行向量化、积极指令合并等优化。
3. Rake【1. Maaz Bin Safeer Ahmad, Alexander J Root, Andrew Adams, Shoaib Kamil, and Alvin Cheung. Vector instruction selection for digital signal processors using program synthesis. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1004–1016, 2022.】。
* 实现语言：伪代码解析器使用Python实现。相似性检查引擎使用Python和Rosette。代码合成器使用Python和Rosette。

A4 实验结果

6.1 案例研究：在Hydride中支持ARM

工程效率的体现：x86和Hexagon是Hydride最初支持的两个目标，其设计和实现由两位学生（前两位作者）花费了一年多时间完成。在证明Hydride在x86和Hexagon架构上具有与生产级Halide编译器相媲美的性能后，由一位不熟悉项目实现的第三方学生在约3个月内为Hydride添加了ARM支持。他实现了ARM伪代码规范的解析器并将其集成到Hydride中，最终实现了与生产级Halide几乎相当的性能（如图6c所示）。相比之下，Google、Adobe和高通等公司在过去十年中投入了大型工程团队来开发和优化生产级Halide编译器的代码生成支持。Hydride仅用三人的工程努力，在一年多的时间里就在三个复杂架构上达到了与Halide相当的性能，这证明了Hydride提供的高度自动化和可重定向性，以及其在工程投入和时间上的显著节省。

6.2 AutoLLVM IR 结果

指令集压缩：表1显示，Hydride支持x86、HVX和ARM架构的3,557条指令，并将它们压缩为397条AutoLLVM IR指令。HVX的等价类较少，因其是更小、更专业的DSP指令集。ARM与x86和HVX的共同等价类较少，因为大量ARM指令是x86和HVX中不存在的融合指令（如融合的SIMD加减法指令）。

与Rake的比较：Rake仅支持164条HVX和200条ARM指令，而Hydride支持的指令数量分别是Rake的约2倍（HVX）和约6倍（ARM）。Rake需要手动实现目标指令的语义，这是一个繁重且耗时的过程。表2列出了在Rake的HVX语义实现中发现的错误。相比之下，Hydride在实现ISA伪代码解析器后就能自动生成语义，这是一次性的工作。Hydride支持比Rake更复杂的指令，如用于高效转置大向量的vshuffvdd和vdealvdd指令（图5），以及Rake不支持的多种点积和混排指令。与Rake一样，Hydride目前只支持整数指令。

6.3 运行时性能

x86性能 (图6a)：Hydride在x86上的性能比Halide的生产后端高出8%（几何平均），比Halide的LLVM后端高出12%。在矩阵乘法基准测试中，由于生成了更快的非SIMD指令（点积和交错），其速度比Halide的x86后端快1.30倍以上（如表3第2行所示）。在31个基准上，其性能与Halide的x86后端相当或更好。仅在2个基准上出现轻微性能下降。

Hexagon性能 (图6b)：Hydride在Hexagon上的性能与Halide的Hexagon后端相当，比Halide的LLVM后端快约2倍（几何平均）。在gaussian7x7等基准上出现性能下降，原因是Hydride无法合成覆盖多个基本块的大窗口代码来生成专用的四路点积指令，或无法执行Halide后端中的特定跨基本块优化。与Rake相比，Hydride在所有可评估的基准上性能都更好，几何平均提速25%。

ARM性能 (图6c)：Hydride在ARM上的性能比Halide的生产后端高出3%（几何平均），比Halide的LLVM后端高出26%。考虑到这是由一名学生在约三个月内完成的工作，这是一个令人印象深刻的结果。Rake自称支持ARM，但未能成功编译任何基准测试。

6.4 编译时间

编译时间分析（表4）：
* 冷缓存编译 (列 I)：从空缓存开始，综合的几何平均时间为ARM 9分钟，x86 18分钟，HVX 39分钟。HVX时间较长是由于其指令复杂，但这使其能够生成比简单SIMD指令性能更好的代码。
* 跨基准缓存 (列 II)：使用已填充其他基准结果的缓存，编译时间显著加快（ARM约7.5分钟，x86约9分钟，HVX约11分钟），表明基准之间存在大量通用子表达式。
* 热缓存重编译 (列 III)：当缓存完全命中时，重编译时间非常快（ARM约1.5分钟，x86约2.5分钟，Hexagon约2分钟），主要瓶颈在于Racket的哈希表查找和初始化开销。
* 真实场景：调整调度 (列 IV)：在只修改调度参数（如分块、融合策略）而不改变向量化因子时，Hydride可以重用缓存结果。几何平均编译时间在x86上约为3分钟，HVX上为1.5分钟，ARM上为4分钟，接近热缓存情况。

6.5 综合敏感性分析

启发式方法的效果（表5和图7）：由于大型指令集导致综合问题难以处理，Hydride采用多种启发式方法来剪枝语法。
* 基础剪枝（BVS）：仅使用基于位向量操作特征的基础剪枝，综合可在数百秒内完成，生成所需的点积表达式。
* 逐通道综合 (Lane-wise synthesis)：此启发式方法将x86的综合速度提高了2倍，ARM提高了1.4倍，HVX提高了2.8倍。
* 向量宽度缩放 (Scaling)：降低综合过程中的寄存器大小能显著减少综合时间，对拥有1024/2048位寄存器的HVX影响最大。
* 组合启发式方法：结合“逐通道综合”和“缩放”可将综合速度在x86上提高2倍，HVX上提高12.8倍，ARM上提高3.6倍。
* 基于分数的选择 (SBOS)：在应用所有其他启发式方法后，进一步根据与输入表达式的相似度选择操作，最终将综合速度在x86上提高了2.7倍，HVX上提高了20.8倍，ARM上提高了6倍。

A7 相关工作

超优化（Superoptimization）：与现有工作的比较：Bansal和Aiken的工作【4. Sorav Bansal and Alex Aiken. Automatic generation of peephole superoptimizers. ACM SIGARCH Computer Architecture News, 34(5):394–403, 2006.】、Souper【21. Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. Souper: A synthesizing superoptimizer. arXiv preprint arXiv:1711.04422, 2017.】和Minotaur【15. Zhengyang Liu, Stefan Mada, and John Regehr. Minotaur: A simdoriented synthesizing superoptimizer. arXiv preprint arXiv:2306.00229, 2023.】等超优化器专注于对短指令序列进行窥孔优化。与Hydride不同，它们不易扩展到新的ISA，因为其IR语义是手动实现的，不支持自动扩展语言无关的IR，也不支持生成向量指令。Phothilimthana等人【16. Phitchaya Mangpo Phothilimthana, Aditya Thakur, Rastislav Bodik, and Dinakar Dhurjati. Scaling up superoptimization. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, pages 297–310, 2016.】提出的缩小寄存器大小再放大的思想被Hydride借鉴，但他们的工作仅限于少量标量ARM指令。总的来说，Hydride是一个高度可重定向和可扩展的编译器系统，能为多个目标自动生成高性能代码，而这些超优化器不具备此能力。

指令选择（Instruction Selection）：与现有工作的比较：Cattel【6. RG Cattell. Automatic derivation of code generators from machine descriptions. ACM Transactions on Programming Languages and Systems (TOPLAS), 2(2):173–190, 1980.】首次提出使用机器描述生成代码生成器。Buchwald等人【5. 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.】离线地使用程序综合为32位标量x86指令生成模式匹配规则。Rake【1. Maaz Bin Safeer Ahmad, Alexander J Root, Andrew Adams, Shoaib Kamil, and Alvin Cheung. Vector instruction selection for digital signal processors using program synthesis. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1004–1016, 2022.】是一个使用程序综合为Halide生成代码的编译器，但它使用手动实现的Uber IR，且语义是手动实现的，因此无法扩展到像x86这样的大型ISA。Pitchfork【19. Alexander J Root, Maaz Bin Safeer Ahmad, Dillon Sharlet, Andrew Adams, Shoaib Kamil, and Jonathan Ragan-Kelley. Fast instruction selection for fast digital signal processing. 2023.】不支持综合混排指令，导致在矩阵乘法等核心上性能大幅下降。Hydride通过自动生成和可扩展的综合方法克服了这些局限性。

自动向量化（Autovectorization）：与现有工作的比较：Vegen【8. Yishen Chen, Charith Mendis, Michael Carbin, and Saman Amarasinghe. Vegen: a vectorizer generator for simd and beyond. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 902–914, 2021.】是一个为x86自动生成自动向量化模式匹配规则的工具，但其规则脆弱且不支持关键的混排指令。Diospyros【27. Alexa VanHattum, Rachit Nigam, Vincent T Lee, James Bornholt, and Adrian Sampson. Vectorization for digital signal processors via equality saturation. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 874–886, 2021.】和Isaria【25. Samuel Thomas and James Bornholt. Automatic generation of vectorizing compilers for customizable digital signal processors. 2024.】是针对特定目标的自动向量化器，但它们的ISA语义是手动实现的，且综合策略难以扩展到大型程序。Porcupine【10. Meghan Cowan, Deeksha Dangwal, Armin Alaghi, Caroline Trippel, Vincent T Lee, and Brandon Reagen. Porcupine: A synthesizing compiler for vectorized homomorphic encryption. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 375–389, 2021.】使用手动实现的有限SIMD指令语义，并要求用户提供带空洞的参考实现和草图。Hydride则不需要用户提供草图，并支持更广泛的指令集。

A5 结论

本文提出了Hydride，一种新颖的全自动化编译器构建方法。该方法仅需一组硬件供应商发布的机器ISA伪代码规范，即可自动生成一个具有形式化语义的核心语言和机器无关的编译器IR。该IR语义可用于通过程序综合来实现高性能语言的编译器，取代了费力且脆弱的模式匹配规则。这种方法实现了高指令集覆盖率和高性能代码生成，即使对于大型、复杂的指令集也是如此。

Hydride的方法可以使其他编译器基础设施受益。例如，我们目前正在MLIR中使用Hydride，从ISA规范中自动生成目标无关的方言（dialect）和低级的目标特定方言。这些方言类似于‘x86Vector’和‘ArmNeon’方言，但指令覆盖范围要好得多；此外，它还为目前不存在的Hexagon生成了一个方言。Hydride自动生成的形式化语义可用于通过综合自动生成从‘vector’和‘arith’方言到自动设计的方言的降低代码。目前MLIR中不存在这样的能力。