💻 computer science

Separation Logic for Memory Conflict Detection in High-Level Synthesis

本文提出了一种在 LLVM IR 层级的空间验证框架，该框架利用分离逻辑（Separation Logic）和 SMT 求解器，通过将非仿射数组访问建模为多态空间谓词，来检测并防止高层次综合中的内存冲突，从而在实现安全并行化的同时，避免了传统多面体方法所带来的性能退化型过度近似。

原作者： Yeonseok Lee

发布于 2026-07-09

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Yeonseok Lee

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一位繁忙工厂的厂长（即高层次综合或 HLS 过程）。你的目标是建造一台能够同时执行多项任务的超级快速机器。为此，你告诉你的工人：不要再一个接一个地做事，而是要在同一个“时钟周期”内同时进行所有操作。

然而，出现了一个重大问题：内存瓶颈（The Memory Bottleneck）。

问题所在：单门仓库

在你的工厂里，所有的工人都需要从一个巨大的仓库（内存库）中获取零件。但这个仓库只有一个门。

如果工人 A 和工人 B 试图在同一秒钟通过这扇单门，他们就会撞在一起。这就是内存冲突（Memory Conflict）。
为了防止这种情况，旧的安全规则（称为多面体框架/Polyhedral Frameworks）非常谨慎。如果指令涉及复杂的数学运算（例如涉及随时间变化的动态数值的除法或乘法，即非仿射算术/non-affine arithmetic），旧规则就会感到困惑。
因为它们无法证明工人之间不会发生碰撞，所以旧规则会说：“以防万一，宁可错杀不可。”于是让大家排队等待。这把你原本超高速的并行工厂变回了缓慢的单行队列，从而破坏了你获得的性能增益。

解决方案：“分离逻辑”地图

这篇论文介绍了一种更聪明的方法，利用一种被称为分离逻辑（Separation Logic）的概念来检查碰撞。请不要将此视为一个数学方程，而应将其视为一张工厂车间的空间地图。

1. “Getelementptr” 翻译器
首先，系统将复杂的代码转换为简单的、扁平化的指令（就像 GPS 提供一个单一的街道地址，而不是一套复杂的路线指南）。它查看计算机理解的原始指令（LLVM IR），以精确观察工人正试图前往何处。

2. “排他性所有权”规则
分离逻辑有一个黄金法则：你不能同时拥有两块相同的土地。

想象仓库被分成了 4 个较小的房间（内存库）。
系统会询问：“工人 A 是否拥有 1 号房间，而工人 B 是否拥有 2 号房间？”
如果答案是肯定的，那么他们就是安全的。由于他们在不同的房间，他们可以同时进入。
奇妙之处在于，如果他们两人都试图声称“我拥有 1 号房间”。在这种逻辑中，试图同时说“我拥有 1 号房间”且“我也拥有 1 号房间”会导致逻辑上的矛盾（逻辑本身的崩溃）。系统会立即识别出这是“不可能”的情况，并标记为一个冲突。

3. “数学侦探”（SMT Solver）
系统使用一位强大的数学侦探（SMT Oracle）来检查工人的路径。

如果数学很简单： 侦探会迅速证明：“是的，工人 A 去 1 号房间，工人 B 去 2 号房间。没有碰撞！”工厂并行运行。
如果数学太奇怪（不可判定/undecidable）： 有时工人的路径涉及极其复杂的数学，以至于侦探无法及时求解。
- 旧系统： 会猜测“也许会碰撞”，并强制要求排队。
- 本系统： 会承认“我无法证明它们是安全的”。随后，它会触发一个安全回退机制（Safe Fallback）。它会说：“既然我无法证明它是安全的，那么我会让他们轮流进行。”这确保了机器永远不会真正发生碰撞，即使它的速度可能比理论上能达到的最高速稍慢。

结果：一个更安全、更快速的工厂

通过使用这种“空间地图”方法，该论文声称实现了以下目标：

停止猜测： 它不再仅仅因为数学难题就假设一切都是危险的。它尝试精确证明哪些房间可以安全地同时使用。
捕捉隐形碰撞： 它能捕捉到那些旧有的“排队”规则会遗漏的冲突，从而允许更多的工人进行并行工作。
保证安全性： 如果数学过于复杂无法求解，它会默认切换到安全模式。它承诺最终的机器（硬件）绝不会出现两个工人试图同时通过同一扇门的情况。

简而言之： 这篇论文用一种基于地图的智能系统，取代了那种谨慎的、“假设最坏情况”的安全规则；该系统尝试证明工人能否安全协作。如果无法证明，它会强制要求等待，从而确保最终的硬件是完美无碰撞的。

技术摘要：用于高层次综合中内存冲突检测的分离逻辑

问题陈述

高层次综合（HLS）通过将 C/C++ 代码转换为寄存器传输级（RTL）设计来加速硬件开发，并利用循环展开和数组分区来最大化并行性。然而，当涉及非仿射算术（例如符号乘法、除法或取模运算）的并发内存访问调度时，会出现一个关键瓶ing点。

传统的 HLS 框架依赖于多面体模型（Polyhedral Model）进行依赖分析。这种几何方法要求循环边界和数组访问函数是仿射的（即循环变量的线性组合）。面对非仿射索引时，多面体求解器会系统性地过度近似依赖关系以确保安全性。这导致了一种保守的退化方案：假设所有内存语句都相互依赖，从而导致单体堆分配（Monolithic Heap Allocation），并将本可以并行运行的操作串行化。这种人为的串行化降低了硬件的吞吐量和效率。此外，现有的动态技术通常需要运行时检查或专门的控制器，从而增加了开销。

方法论

本文提出了一种直接作用于 LLVM 中间表示（LLVM IR） 的空间验证框架，用于检测内存冲突，而不依赖于仿射几何约束。该核心方法论集成了**分离逻辑（Separation Logic, SL）与可满足性模理论（SMT）**求解器。

1. LLVM IR 层级的空间建模

不同于以往分析 C/C++ 抽象语法树（AST）的方法，本框架作用于 LLVM IR。它利用 getelementptr (GEP) 指令——编译器通过该指令将多维数组索引机械地扁平化为一维算术表达式。

双状态架构： 框架使用两个不同的组件来建模系统状态：
- 单调存储 ( $s$ )： 将不可变的静态单赋值（SSA）虚拟寄存器映射到值。由于 SSA 的特性，寄存器永不被覆盖，简化了状态追踪。
- 空间堆 ( $h$ )： 将物理内存地址（值的子集）映射到数据，代表片上 SRAM 存储库（Banks）。
多态存储库谓词： 框架定义了空间谓词 bank(k, A, N)，用于断言在将数组 $A$ 分为 $N$ 个存储库的场景下，拥有第 $k$ 个存储库的排他性所有权。这些谓词根据从 LLVM 元数据中提取的分区策略（循环、块或完全分区）进行动态调整。

2. 无冲突展开（CFU）条件

为了验证 $U$ 次展开的循环迭代能否并发执行且不产生结构冲突，框架制定了**无冲突展开（Conflict-Free Unrolling, CFU）**条件。

分离连接符 ( $\ast$ )： 验证的核心是迭代分离连接：
$cfu(E, A, N) \triangleq \ast_{i=1}^{U} bank(B(expr_i, N), A, N)$
这断言 $U$ 次并发内存访问必须拥有 $U$ 个严格不相交的物理内存区域。
空间坍缩： 分离逻辑的一个基本公理是，资源不能被自身不相交地拥有（ $P \ast P \implies \bot$ ）。如果两个并发迭代指向同一个物理存储库 $k$ ，则空间公式会尝试计算 $bank(k) \ast bank(k)$ ，这在逻辑上会坍缩为矛盾 ( $\bot$ )。这种坍缩作为数学手段，用于检测内存冲突。

3. 向 SMT 转换与回退机制

为了使空间逻辑具有可计算性，框架采用了一个转换函数 $T$ ，将空间不相交性要求简化为基于 SSA 变量的成对不等式矩阵。

验证条件 (VC)： 空间要求被转换为一阶逻辑公式：
$\pi \implies \bigwedge_{1 \le i < j \le U} (k_i \neq k_j)$
其中 $\pi$ 是路径条件， $k_i$ 是符号存储库索引。
SMT Oracle： SMT 求解器（如 Z3）尝试证明该 VC。
- Sat (可满足)： 索引被证明是互不相同的；进行并行综合。
- Unsat/Unknown/Timeout： 如果求解器无法证明不相交性（由于非线性整数算术的不可判定性），框架会触发确定性的顺序回退（Deterministic Sequential Fallback）。它假设存在冲突，通过多路复用器驱动的停顿逻辑将操作串行化，以确保物理安全性。

核心贡献

形式化硬件内存模型： 本文建立了一个基于 LLVM IR 的静态内存框架，通过 GEP 指令抽象多维数组索引，并将其绑定到处理循环、块和完全分区的多态空间谓词上。
无冲突展开 (CFU) 条件： 提出了一个明确的空间执行要求，使用迭代分离连接进行表述。它通过自动的空间逻辑坍缩（ $cfu \implies \bot$ ）而非几何过度近似来检测物理存储库冲突。
自动化 SMT 转换与回退： 一个数学完备的转换函数将空间命题还原为基于不可变 SSA 寄存器的成对不等式。至关重要的是，它包含一个保守的顺序回退模型，以确保在非线性整数算术不可判定时仍能保证绝对安全。
正确性定理： 本文证明了，如果代数验证条件被 SMT 求解器验证通过，则生成的 RTL 在结构上对于内存存储库碰撞是免疫的。

结果与意义

本文声称弥合了形式化分离逻辑理论与实际硬件综合之间的鸿沟。通过将验证负担从几何多面体模型转向 LLVM IR 上的代数 SMT 求解，该框架：

最小化保守串行化： 当遇到非仿射索引时，它避免了传统工具中那种“安全但缓慢”的回退方案，只要 SMT 求解器能够解析这些代数约束。
确保结构安全性： 通过“空间坍缩”机制和保守回退机制，框架保证了生成的硬件不会遭受结构性内存冲突，即使在存在不可判定算术的情况下也是如此。
绕过仿射限制： 它解决了复杂的存储库映射依赖问题，而无需要求线性的几何边界，也不需要生成额外的运行时状态机开销。

其意义在于为 HLS 调度提供了一种严谨的、基于代数的替代方案，用于处理多面体模型，从而在处理非仿射内存访问模式的设计中实现更高的并行度，同时保持硬件生成所需的绝对安全保证。作者指出，未来的工作将包括将其实现为自定义的 LLVM pass，并探索利用分数权限（Fractional Permissions）来优化只读并发访问。