Lindsey Kuper：为正确高效的并行计算设计抽象

我的研究关注如何构建计算既快速又正确的并行系统，以及如何让分布式系统在网络分区和无界延迟下保持正确。这两个领域有不同的研究文化和词汇，因此我寻找能帮助我们理解两者的抽象。

我会讨论基于格的数据结构 LVars、用于并行化现有代码的非侵入式语言，以及神经网络验证。共同的思想是：用高层方式表达程序员意图，让它促进效率，而不是牺牲效率。

我们常以为性能意味着更接近硬件。但高层次的意图表示可以向系统提供调度和优化所需的信息。同样的原则也有助于形式化验证用于安全关键场景的神经网络。

确定性编程意味着相同输入产生相同的可观察输出。假设网上商店的购物车用共享映射表示。我在两个异步线程中分别添加一本书和一双鞋，再在另一个线程中读取购物车。

我反复运行这个程序的一个版本时，有时返回两件商品，有时只有书，有时只有鞋。结果取决于调度。如果把购物车复制到多台机器上，问题会更加困难。

这个程序的同步不足：我们可以等两次写入都完成再读取。但与其为每个程序临时添加屏障，不如寻找一种编程模型，保证在其中编写的所有程序都有确定性结果。

一种已有方法是 IVar：只能写入一次的共享变量，读取会阻塞，直到写入发生。如果所有通信都使用 IVar，单次写入与阻塞读取的组合就能保证确定性。

购物车例子提示了一种限制更少的方案。添加书和添加鞋不会相互覆盖，这两次更新可交换。不确定性出现在读取过早观察到中间状态的时候。

LVars 允许多次写入，条件是写入可交换且具有膨胀性：每次写入要么不改变状态，要么按照应用特定的格将状态向上推进。读取则限于阈值读取，在状态达到合适阈值前会阻塞。

在购物车的格中，空购物车位于底部，上方状态包含不同数量的书和鞋。两次写入无论以何种顺序执行，都会达到同一个组合状态。询问书有多少本的读取，会阻塞到跨过相关阈值。

读取返回的是阈值结果，不一定是解除阻塞时的完整内容。鞋可能已经到达，也可能没有，但关于两本书的答案仍然确定。可以把阈值集合想象成横跨这个格的一道触发线。

有效的阈值集合需要满足一种称为两两不兼容的性质。LVar 库的用户不必对每次读取都推导这些数学条件，因为库只暴露合适的操作。库的实现者必须确保写入可交换、具有膨胀性，读取也满足阈值条件。

再看并行图遍历。从一个节点出发，将它标记为已见，并探索邻居，可能把这些工作分配给不同线程。已见节点集合单调增长，直到发现所有可达节点并达到不动点。

集合并集符合 LVar 模型，但仅靠阈值读取，无法表达通常用来判断节点是否尚未被看到的测试。如果无法决定何时停止，图中的环就可能导致反复遍历。

我们用事件和处理器扩展 API。改变状态的写入会产生事件，新节点到达时处理器可以运行回调。quiesce 操作会阻塞，直到该处理器启动的回调都完成。

我们还增加 freeze：它不阻塞，直接读取精确内容，此后改变状态的写入会抛出异常。如果程序过早冻结，就不能悄悄返回不完整结果并让冲突写入随后成功；它可能收到冻结后写入错误。

这称为准确定性。两次终止的执行会产生相同结果，或者其中一次以错误结束。错误表明存在同步问题，消息可以指出发生竞争的写入与冻结操作，帮助程序员调试。

证明关注外部结果，而不是要求执行步骤序列完全相同。其中的独立性性质表达了这样一种想法：即使初始存储以相关方式变大，计算仍然可以前进一步，因为独立效果不会相互干扰。

我把它与分离逻辑中的框架规则作比较。如果一个命令把满足某个条件的状态转变为满足另一个条件的状态，那么一个无关且不相交的性质可以始终保持成立。这个规则帮助我们推理程序没有改变什么。

我们的独立性性质类似框架性质，但状态片段可以重叠，只要它们仍不相互干扰。知道效果能够安全共存后，运行时就可以自由地把工作调度到可用的并行资源上。

分布式系统增加了复制状态和不可靠网络。理想情况下，购物车的每个副本都应始终一致；但网络分区阻止副本通信时，这一目标与高可用性相冲突。

CAP 取舍促使我们考虑较弱的保证，例如最终一致性：副本可以暂时不一致，但最终会收敛。接下来需要用适合应用的方式协调冲突版本；简单选择最后一次写入，并不总是用户想要的。

Dynamo 的研究以购物车为例：应用可以合并有冲突的购物车，而不是丢弃一个。无冲突复制数据类型，即 CRDT，用格形式化相关思想：副本可以通过最小上界合并不同状态。

这启发我们把 LVar 风格的阈值读取应用于 CRDT。查询一本书是否存在时，可以等某个副本观察到它，而不必等待所有副本一致。这类查询也许无需各处完全一致，就能提供确定性的观察结果，从而减少同步。

下一个例子来自科学计算。我的朋友 Laura 所在的团队收集飞机飞越南极洲时的雷达数据，研究冰层及其下方岩石。她希望专注于地球物理，而不是手动管理内存或调度并行任务。

研究人员可能用 MATLAB、Python、R 或 Julia 编写原型，随后发现面对更大输入或更高分辨率时代码太慢。把慢的部分移植到 C、C++ 或 Fortran，并常常使用 OpenMP 等工具，可以提高速度，却会产生更难实验和维护的代码。这就是双语言问题。

高性能领域专用语言提供一种解决办法。Delite 等框架放弃一部分通用性，以换取高层编程模型和性能。领域信息让编译器更了解计算，从而有机会进行更好的优化。

但现有用户必须学习 DSL 并移植代码；如果语言只支持所需功能的 95%，剩下的部分就可能成为难以跨越的障碍。即使设计良好的 DSL 也无法预见未来所有用途。

在 Intel Labs，我们为 Julia 构建了非侵入式嵌入 DSL：Parallel Accelerator。它重点加速现有数值数组操作，而不要求用户用另一种语言重写整个程序。宏 @acc 用来标记需要加速的代码。

对于 runStencil 等新结构，包同时提供 Julia 库实现和高性能原生实现。用户可以关闭编译器，在开发和调试时使用库模式，部署时再启用编译。

第一个例子是 Black-Scholes 期权定价基准。输入是数值数组，函数大部分由逐点算术运算构成。这个例子旨在展示适合并行化的代码类型，而不是解释期权定价。

要加速它，我们导入包并用 @acc 标注函数；其余部分仍是普通 Julia。Parallel Accelerator 将数组操作转换成数据并行映射，在已确定大小时避免部分边界检查，并融合操作以避免中间数组。

使用包含 1 亿个元素的数组时，原始 Julia 代码耗时约 22 秒。在一台 36 核机器上，加速版本用一个线程耗时略多于 13 秒；即使没有并行执行，优化也带来了收益。

使用 36 个线程后，运行时间降至约半秒，比原始版本快 40 多倍。这个例子是专门挑选来展示方法优势的；我们并非总能得到如此大的收益。MATLAB 对比同时使用了默认并行设置和单线程设置。

结果也突出了当时 Julia 的一个惯例：显式循环可能比聚合数组操作更快，有些人担心这个库会鼓励不符合语言习惯的写法。Julia 团队支持这一方法，但讨论表明工具也会影响人们如何编写代码。

第二个例子是模板计算。要模糊黑白图像，可以使用每个像素自身及邻居的加权平均值来更新它。runStencil 结构表达了这种模式，同时与原有的 Julia 数组风格保持接近。

在一张大图上迭代 100 次，普通 Julia 耗时近 900 秒。加速版本使用一个线程不到 40 秒，使用 36 个线程约 1.4 秒，在这个例子中快了 600 多倍。与 Black-Scholes 不同，这需要使用领域专用结构并改写几行代码。

Parallel Accelerator 本身并未对 Julia 产生持久的重大影响，但其技术影响了其他系统。它成为深度神经网络和分布式分析工作的基础，Intel 同事还将它移植到 Python，并整合进 Numba，用于多线程数值代码。

最后一个项目涉及使用 SMT 求解器验证安全关键软件中的神经网络。在这种场景中，严格证明特定不良结果不会发生是审慎的，有时也是法律要求。随着神经网络进入这些系统，验证工具却难以跟上。

Stanford 的研究人员希望减少飞机防撞策略所需的存储空间，让它能装入经过验证的机载硬件内存。他们训练神经网络来近似原始策略表，大幅降低存储需求，但这也带来了认证方面的疑虑。

系统每秒接收一次传感器测量，输出五种建议之一：无冲突、轻度或大幅左转、轻度或大幅右转。原始表为约 1.2 亿种可能的相遇状态下这些选择打分，需要数百 GB 的空间。

训练后的网络将相遇状态映射到建议分数，存储需求只有几 MB，约为原来的千分之一。它的输出与原表并不完全相同，因此关键问题是我们关心的具体性质是否仍然成立。

例如，我们可能想证明：当另一架飞机从左侧接近且距离很近时，网络总会建议大幅右转。我们把网络和期望性质编码成公式，再用 SMT 求解器检查它。

SAT 询问一个布尔公式是否存在满足赋值。SMT，即模理论可满足性，将问题扩展到包含某种理论中表达式的公式，例如线性实数算术。求解器因此既能推理布尔结构，也能推理实数变量的约束。

即使理论本身可判定，求解也可能很慢。急切式 SMT 架构把整个问题归约为布尔 SAT 公式，但这样可能丢失高层结构。例如，直接推理加法，比只推理低层布尔表达式更容易利用加法的交换性。

惰性 SMT 架构保留 SAT 求解器，并将其与针对算术、数组和位向量等领域的专用理论求解器结合。保留领域结构后，系统可以先利用高层知识，而不是立即把所有内容归约为布尔情况。

对于神经网络，仅有线性算术还不够：非线性激活函数让公式更加复杂。ReLU 激活可以编码为析取，但如果把每个选择都急切地交给 SAT 求解器，验证可能慢到无法实际使用。

我的 Stanford 合作者让线性规划理论求解器理解 ReLU 约束。它可以暂时不拆分 ReLU，先求解问题的其余部分，只有必要时才拆分。这个高层原语让所研究性质的飞机网络验证变得可行。

例子中的每个子网络有 300 个 ReLU 激活，因此有 2^300 种开关组合。求解器不需要全部拆分：其中一个列出的性质最大拆分深度为 22。这些检查仍可能需要几十小时，但比遍历所有组合实际得多。

在一篇研讨会论文中，我们还提出用分段线性近似将此方法扩展到其他激活函数，例如 sigmoid。演讲时，这项扩展尚未实现。

展望未来，我希望领域专用求解器能够理解与并行和分布式计算有关的结构，包括格和偏序。我也希望将求解器并行化，让处理公式的子任务安全共享各自发现的信息。

我尚未验证的假设是：为其他场景开发的确定性技术也可能有助于并行 SMT 求解。长期目标是让领域专家更容易构建高性能理论求解器，而不必成为 SMT 求解器每个内部细节的专家。

有人问现有 SMT 求解器能否作为起点。原则上可以：Z3 和 CVC4 等系统已有求解器核心和理论组件。但在实践中，它们即使开源也可能难以修改，原因可能是技术障碍、文档或文化。

一位听众询问与底层代码的比较。我们的论文针对三个工作负载包含了专家编写的并行 C++ 实现。我们认为能达到这些实现约两倍耗时以内就是成功，尽管幻灯片没有显示这一比较。

非侵入式 DSL 是嵌入式 DSL 的一种。两者区别并不严格，但目标是让它与宿主语言的边界更加开放。Elvish 这样的 LVar 库也是嵌入式 DSL，其操作组织在 monad 中，与其他代码有更清晰的边界。

Parallel Accelerator 不能并行化所有 Julia 代码：它针对一部分聚合数值数组操作，无法处理时会回退到顺序执行。我建议标注较小的函数，而不是巨大的代码块，让加速代码能够与其他部分交互。

错误消息也是嵌入式 DSL 的可用性问题。消息可能以宿主语言而非 DSL 的术语出现，要让它们有用需要大量工作。Parallel Accelerator 的消息还没有达到应有的质量，这是研究实现的局限。

有人问到 Bloom 和 BloomL，我指出它们有密切联系。BloomL 将基于任意格的分布式编程扩展出去，目标是最终一致性，但最终收敛不同于确定性：在副本收敛之前，读取者仍可能观察到不同的中间状态。

BloomL 在整个模型中限制非单调操作。使用 Haskell LVar 库时，可以先让结构单调增长，再冻结它，随后把它作为普通数据结构使用。这些项目同期发展，揭示了不同研究社区之间有用的联系。

另一个问题将 Parallel Accelerator 与自动向量化作比较。它只能加速自己认识的操作；否则顺序回退能够保持正确性，但可能很慢。对不支持的操作提供警告或优化建议会有帮助，不过我对如何做到这一点还没有完整答案。

有人问能够验证多大的网络。我认为现有技术仍然不够。Reluplex 处理的网络比早期基于 SMT 的工作更大，但这个例子把更大的系统拆成约 300 个神经元的子网络，与许多现代网络相比仍然很小。

后续使用抽象解释的工作探索了更高效地剪枝或组合搜索空间的方法。但更大的挑战可能是陈述要验证的性质。飞机位置和速度是相对高层的输入；如果输入是由像素构成的摄像头图像，那么“避开行人”这样的性质就更难形式化。

另一个问题是：如何知道选择的防撞性质覆盖了重要危险？我们并不声称证明了完整的功能正确性，只证明了能够写下来的特定性质。与安全研究一样，安全声明的价值取决于考虑了哪些故障或威胁。

最后有人询问能否静态验证 LVar 的假设。Deterministic Parallel Java 等类型系统可以表达并检查一些交换性性质。我们的 LVar 库则依赖实现者确保写入和阈值读取遵守所需规律。

经过验证的 LVar 在我的研究计划中。使用 Liquid Haskell 验证序关系规律的工作表明，借助 SMT 的方法也可能帮助建立格所需的性质。目标是检查目前由库实现者负责保证的假设。