Greta Yorsh 谈编译器优化与反馈

Ron Minsky 欢迎 Greta Yorsh 做客，她是 Jane Street 伦敦团队的编译器工程师。她的背景涵盖程序分析、验证、工业界和学术界；自 2018 年起，她一直从事 OCaml 编译器工作。

Yorsh 在以色列学习计算机科学和经济学，之后攻读计算机科学博士，重点研究软件验证。她曾在 IBM Watson 从事程序分析、参与 ARM 的 GCC 后端工作，后来在 Queen Mary University of London 教授和研究编译器，之后加入 Jane Street。

验证研究试图通过对源代码的推理证明程序满足所需属性。Yorsh 发现一般性问题很难解决，也希望了解真实用户需要什么。与开发者交谈让她看到，除了正确性，性能也可能很重要，因此编译器优化成为形式化技术一个有吸引力的应用领域。

在 ARM，她看到针对特定指令和机器的优化如何改变性能。由于大量软件依赖编译器输出，编译器也必须正确。这种结合为她提供了实际、可测量的优化目标，同时对正确性提出严格要求。

Minsky 将形式化验证描述为证明实现符合规范。关于程序行为的一般性问题不可判定，但工具仍然可以在受限情况下或程序员提供额外工作的情况下提供帮助。

Yorsh 区分了独立的逻辑规范和由类型提供的更紧密集成的规范。随着代码演进，维护独立规范很困难。工具可以同时检查代码和规范，但程序员仍需要编写两者；自动化可以减少负担。

测试检查具体执行，当一般性证明成本很高时，它可能迅速发现漏洞。Yorsh 对结合两种方法感兴趣：形式化方法可以提出有用的测试，而具体执行可以帮助指导或加速对更大行为空间的推理。

Minsky 从程序员角度补充：类型对所有执行中的某些属性提供保证，测试则检查特定运行。类型正确的程序和少量通过的测试都不能确保完全正确，但两者结合可能比任何一种单独使用更有效。

Yorsh 概述了一类技术：执行程序，收集观察到的状态，再将它们抽象为覆盖相关状态的描述。判定过程可以找出尚未覆盖的状态或路径，进而指导下一次执行。这样的相互作用可以提高覆盖率，并减少剩余验证的高成本工作。

话题转向超优化。Yorsh 解释，后端需要了解指令成本、寄存器和硬件行为。传统编译器分别执行指令选择、寄存器分配和调度等遍次；这些选择跨遍次相互影响，因此各自合理的决策不一定产生整体最佳结果。

她在处理 ARM 微架构时发现，很难让编译器生成已知更好的指令序列，因为改变一个遍次会影响其他遍次。超优化提供了另一种视角：搜索同时满足约束的方案，而不是只依赖固定顺序的局部变换。

超优化器接收一个指令序列，并寻找在某种成本度量下优化的等价序列。历史上目标可能是最短序列，但在现代硬件上，较多指令有时比包含昂贵操作的较短序列运行得更快。

候选序列必须在相关输入上表现得与原始序列相同。证明任意程序等价是不可判定的，因此早期工作将问题限制在无分支的直线序列并使用测试；后来的方法将语义表达为约束，使用判定过程。验证和搜索仍有显著成本。

Minsky 将传统编译器的模块化中间表示与遍次，同超优化对可能代码的搜索作比较。模块化设计让大型系统更容易理解，但可能掩盖相互作用；搜索方式明确了成本和正确性标准，却可能十分昂贵。

Yorsh 希望看到超优化得到更多使用，尤其是作为编译器开发者的工具，以及用于对性能极其关键的代码。根据当时的技术状况，她不认为昂贵搜索会成为开发者日常构建中的常规步骤。

硬件架构的形式化描述也可以作为搜索的参数。在理想化方案中，新的机器描述可以帮助生成好的代码，而无需手工重新设计每个复杂的后端遍次。Yorsh 认为，这有望帮助硬件和编译器设计者探索新架构能够带来多大收益。

Minsky 指出，超优化器可以衡量实用编译器输出与更优序列之间的差距。他担心长达数小时的搜索会让应用开发反馈过慢。Yorsh 同意最直接的用途是帮助基础设施设计者，同时提出部分昂贵工作也许可以针对源语言与目标架构组合复用。

被问到学术界与工业界之间的转换时，Yorsh 说，研究提供时间来理解和设计强大的技术，但接触用户可能有限，学术环境也奖励新颖性。工业界有不同约束和规模，却能让她直接了解熟悉的工具是否真正帮助开发者。

在 Jane Street，她参与反馈驱动优化，也称配置文件引导优化。传统插桩会在程序中加入测量点；采样可以在较少扰动下收集配置文件。有代表性的运行能够指出哪些路径较热，这是纯静态编译器无法知道的信息。

在她描述的工作中，配置文件指导代码布局：可执行文件中函数的顺序，以及函数内基本块的顺序。经常一起执行的代码放得更近，可以更好地利用指令缓存，减少从较慢内存层获取指令的时间。

Minsky 回忆，早期一些重要程序仅通过重新排列指令就获得了约 10%、15% 或 20% 的性能提升。Yorsh 解释，这些收益取决于工作负载和局部性，不是适用于所有程序的普遍承诺。

团队还发现稳定性很有价值。一位开发者在无关程序库修改后观察到变慢；反馈驱动布局通过将常用代码放在一起，消除了观察到的差异。结果更可预测时，人们更容易判断小幅优化是真实效果还是布局造成的现象。

他们讨论在编译器基准测试中使用反馈驱动布局来减少噪声。另一种研究方向则有意随机化布局，研究结果分布，可能结合统计采样。Minsky 指出，反复扰动和重跑基准测试可能很昂贵。

Minsky 将反馈驱动优化放在静态编译与即时编译等完全动态方法之间。硬件本身也会预测和重排工作。他问，不同处理器的能力如何改变编译器值得进行的工作。

Yorsh 说，硬件观察最近的执行，而编译器可以推理更多程序结构和可能的未来路径。每种优化也都有成本，可能体现在编译时间、运行时间或能源上。硬件改进可以惠及多个编译器，而语言编译器的改进则跨架构服务自己的用户。

对某些程序而言，内存访问、分配和垃圾回收的成本超过小规模指令级优化。此时数据布局和访问模式可能更重要。Yorsh 提到同事正在开发分析工具，让这些模式可见。

加入 Jane Street 之前，Yorsh 没有用 OCaml 编程。调整思维方式后，她发现与自己曾使用的 Java 基础设施相比，OCaml 简洁且适合表达程序分析和转换。垃圾回收也减少了部分显式内存管理的负担。

她在学会理解类型检查器的信息后，很重视它：它能在工作时发现许多错误，尽管测试仍然必要。Minsky 同意，类型系统在表现力和对程序员的帮助方面差异很大。

作为优化目标，OCaml 编译器展示了她不熟悉的设计选择。Yorsh 逐渐欣赏一个相对可移植的后端：它首先追求正确、可理解的代码，并让硬件承担部分优化。架构专用部分很小，但固定遍次也使某些转换难以加入。

她解释了常见的前端、中端和后端划分。前端解析源语言并进行类型检查；中端执行可以较少依赖源语言和目标架构的变换；后端为特定处理器生成代码。共享中间阶段让编译器基础设施能够支持多种语言和架构。

Minsky 问到 ARM 使用不断扩大，包括 Apple 宣布转向基于 ARM 的桌面电脑时 OCaml 的情况。Yorsh 没有在 ARM 上对 OCaml 做过基准测试，并限定自己的回答只是阅读后端代码后的印象：与 GCC 等高度优化的编译器相比，它可能较少获得架构专门化关注。

不同 ARM 微架构有不同需求。顺序执行可能使指令调度尤其重要，而寄存器限制影响分配选择。她也认为 AMD64 的寄存器分配可能有改进空间，但希望有代表性证据表明投入能帮助实际工作负载。

能够接触真实应用、开发者和基准测试，是她工作的一项好处：编译器团队可以测试想法并快速获得反馈。这也让错误的后果更加可见。

Yorsh 回忆一次优化由于她误解了 OCaml 编译器的细节而引入错误编译。一个测试发现了问题，尽管该测试并非常规运行。她说自己认为这没有损害正在运行的生产系统，但同事仍需要协调回滚，并花时间避免触发问题。

她很欣赏团队的回应：修复错误，询问为什么漏掉测试，将其加入流程，并研究编译器中间表示是否可以防止类似错误。Minsky 说，这种以学习为导向的回应是他们努力保持的文化的一部分。

两人转向上游协作。Jane Street 并不拥有 OCaml，修改必须说服更广泛的维护者。由内部应用推动的优化可能难以在外部展示，尤其是最大型可执行文件含有专有代码时。

Yorsh 建议与其他工业界和学术界 OCaml 用户分享性能工具和基准测试。社区参与和信任有助于技术讨论，但不能保证一个对某家公司有用的功能就适合通用编译器。

Minsky 提到围绕多核 OCaml 开发的 Sandmark 基准测试集合，认为它是有前景的共享资源。开源代码可以暴露部分问题，但大规模行为可能取决于无法完整公开的工作负载。

Yorsh 指出，上游维护者必须在性能、可移植性、可预测行为和维护复杂功能的成本之间权衡。让特定遍次更容易添加或启用的编译器，可能在固定后端与长期维护大量优化之间提供折中。

Minsky 同意，模块化可以降低共同维护负担，让实验更容易作为独立修改保留。团队可以收集证据、迭代，最终向上游提出成熟改进。Yorsh 补充说，如果试用功能不需要修改构建系统，其他用户也更容易提供反馈。

他们最后指出，对话再次回到了反馈：性能分析数据帮助优化程序，用户反馈则帮助改进编译器本身。