背景
建议在 ACIR Core 中增加一个由编译器原生支持的 Queue-to-Queue 原子传输
操作:
%fire = ac.try_transfer @source to @destination when %enable : i32
该操作读取当前周期的 Queue committed snapshot,并把 source pop 与
destination push 作为同一个事务组提交。两项更新必须同时成功或同时失败。
这可以让 Queue transfer 的硬件意图在 IR 中保持显式,使 verifier、ACSim
以及未来的 RTL backend 不需要从 try_send → try_recv → assert 这样的
过程式代码中猜测原子关系。
现有表达的问题
目前 Queue 之间的数据移动通常写成:
%head, %valid = ac.peek @source : i32
%sent = ac.try_send @destination %head : i32
scf.if %sent {
%value, %received = ac.try_recv @source : i32
ac.assert %received, "granted source must be readable"
%same = arith.cmpi eq, %value, %head : i32
ac.assert %same, "received value must match peeked head"
}
在当前 proposal/Xfer 仿真模型下,经过谨慎构造的这类代码可以表现出原子
传输效果,但这种关系没有直接存在于 IR 中。后续 verifier 或 RTL backend
必须分析操作顺序、嵌套 scf 和 assertion,才能推断两次 Queue 更新是否
属于同一次传输。
此外,assertion 不应承担功能正确性。综合后的硬件无法在 destination 已经
push 后,因为 source pop 失败而回滚。
Router、Crossbar、带缓冲流水线等组件都需要明确的 Queue-to-Queue transfer
语义。
建议语义
对于元素类型为 T 的两个 Queue:
fire = enable
&& source 在 committed snapshot 中可读
&& destination 在 committed snapshot 中可写
当 fire=true 时,操作创建一个不可拆分的事务组:
从 source 弹出 committed snapshot 中的旧队头
把完全相同的值压入 destination
两项更新在同一个 Xfer barrier 提交。
当任意一侧不能接受传输时:
fire = false
source 不变
destination 不变
必须保证:
- 不会只发生 source pop 或只发生 destination push;
- destination 得到的值严格等于旧 source head;
- 所有 ready/valid 判断读取同一个 committed snapshot;
- 如果现有 Queue 规则规定 pending pop 不释放本周期容量,该规则保持不变;
- 不引入 process-local 临时 holding slot;
- Queue 统计、协议状态和 readable/writable activation 只在 commit 后更新;
- reset 会清除所有尚未提交的 transfer proposal。
第一版中,只有当 verifier 能保证 grouped proposal 不会在后续仲裁中被拒绝
时,%fire 才能作为 Work 阶段可用的结果。存在竞争的 source 或
destination 必须使用静态可证明互斥的 grant,否则应诊断为暂不支持。
不能在 Work 阶段返回暂定的 fire=true,随后又在 arbitration 阶段拒绝该
transfer。
Verifier 要求
建议 verifier 检查:
ac.try_transfer 只能位于 ac.process 内;
@source 和 @destination 必须解析到当前 module 中两个不同的
ac.queue;
- 两个 Queue 的 payload type 必须一致,并与操作声明的
T 一致;
- Queue 的协议和 time domain 必须兼容;
%enable 和 %fire 的类型必须为 i1;
- transfer 不能跨越 suspension point;
- 每个单读 Queue 在一个 commit epoch 中最多 pop 一次;
- 每个单写 Queue 在一个 commit epoch 中最多 push 一次;
- 多个候选 transfer 只有在 grant 可被机械证明互斥时才合法;
- 无法证明的多 pop、多 push 或多 writer 情况必须给出确定性诊断。
该操作还应在 MLIR MemoryEffects 中声明:
- 读取和写入 source Queue state;
- 读取和写入 destination Queue state;
- 读取和写入两侧关联的 protocol state。
ACSim 和 gfsim lowering
ACIR-to-ACSim 可以把该操作 lower 为一个接收两个 native Queue owner 的
compiler-known helper:
%fire = acsim.invoke @acir_impl_queue_try_transfer_i32(
%source_owner, %destination_owner, %enable)
: (!acsim.owner<@queue_i32>,
!acsim.owner<@queue_i32>, i1) -> i1
该 helper 不能简单调用两个彼此独立、会立即产生副作用的 Queue 操作。
Work 阶段应提交一个 grouped proposal,其中至少包含:
source Queue identity
destination Queue identity
旧 source-head value
owner/process identity
transaction-group identity
runtime 必须在 Xfer 前将整个事务组作为一个整体接受或拒绝。commit 时同时
更新两个 Queue,并唤醒两个 Queue 的相关订阅者。
需要完成的编译器和 runtime 工作包括:
- ACIR ODS 定义、parser/printer、verifier 和 memory effects;
- process lowerability 和 ProcessStatePlan action 支持;
- 在 process 中捕获 source、destination 两个 native Queue owner;
- ACIR-to-ACSim invoke lowering;
- 确定性的 helper identity 和 fingerprint;
- ModelPlan 与生成 C++ 的调用支持;
- gfsim grouped Queue-transfer proposal;
- 跨两个 Queue 的原子 arbitration/Xfer;
- reset、统计和 activation 支持。
RTL lowering 意图
该 primitive 应能直接映射成同步 FIFO 控制逻辑:
fire = enable && source_valid && destination_ready;
source_pop = fire;
destination_push = fire;
destination_data = source_head;
source FIFO 和 destination FIFO 的状态在同一个时钟边沿更新。
本 Issue 不要求同时实现 RTL backend,但 Core 语义不应阻碍上述直接
lowering。
验收测试
- source 非空且 destination 可写时,恰好传输一个元素。
- source 为空时,两个 Queue 都不变化。
- destination 已满时,两个 Queue 都不变化。
- destination 得到的值严格等于旧 source head。
- 连续传输保持 FIFO 顺序。
- source pop 和 destination push 具有相同的 commit epoch。
- 删除所有 assertion 后,功能行为不变。
- reset 清除 pending grouped proposal,但不破坏 committed data。
- payload 或协议不匹配时产生确定性诊断。
- 无法证明互斥的多 pop 或多 push 被 verifier 拒绝。
- ACIR round-trip 和 ACIR-to-ACSim FileCheck 测试通过。
- 生成的 C++ 可以编译,native Queue 端到端测试通过。
非目标
本 Issue 不包含:
- 动态选择 source 或 destination Queue;
- 自动重写所有历史
try_send/try_recv 模式;
- RTL backend 本身;
- 跨 time domain 的 Queue transfer。
在该 primitive 稳定后,ACPy 和标准组件可以在其上构建结构化仲裁、
Crossbar 和 transfer-selection 等更高层封装。
背景
建议在 ACIR Core 中增加一个由编译器原生支持的 Queue-to-Queue 原子传输
操作:
该操作读取当前周期的 Queue committed snapshot,并把 source pop 与
destination push 作为同一个事务组提交。两项更新必须同时成功或同时失败。
这可以让 Queue transfer 的硬件意图在 IR 中保持显式,使 verifier、ACSim
以及未来的 RTL backend 不需要从
try_send → try_recv → assert这样的过程式代码中猜测原子关系。
现有表达的问题
目前 Queue 之间的数据移动通常写成:
在当前 proposal/Xfer 仿真模型下,经过谨慎构造的这类代码可以表现出原子
传输效果,但这种关系没有直接存在于 IR 中。后续 verifier 或 RTL backend
必须分析操作顺序、嵌套
scf和 assertion,才能推断两次 Queue 更新是否属于同一次传输。
此外,assertion 不应承担功能正确性。综合后的硬件无法在 destination 已经
push 后,因为 source pop 失败而回滚。
Router、Crossbar、带缓冲流水线等组件都需要明确的 Queue-to-Queue transfer
语义。
建议语义
对于元素类型为
T的两个 Queue:当
fire=true时,操作创建一个不可拆分的事务组:两项更新在同一个 Xfer barrier 提交。
当任意一侧不能接受传输时:
必须保证:
第一版中,只有当 verifier 能保证 grouped proposal 不会在后续仲裁中被拒绝
时,
%fire才能作为 Work 阶段可用的结果。存在竞争的 source 或destination 必须使用静态可证明互斥的 grant,否则应诊断为暂不支持。
不能在 Work 阶段返回暂定的
fire=true,随后又在 arbitration 阶段拒绝该transfer。
Verifier 要求
建议 verifier 检查:
ac.try_transfer只能位于ac.process内;@source和@destination必须解析到当前 module 中两个不同的ac.queue;T一致;%enable和%fire的类型必须为i1;该操作还应在 MLIR MemoryEffects 中声明:
ACSim 和 gfsim lowering
ACIR-to-ACSim 可以把该操作 lower 为一个接收两个 native Queue owner 的
compiler-known helper:
该 helper 不能简单调用两个彼此独立、会立即产生副作用的 Queue 操作。
Work 阶段应提交一个 grouped proposal,其中至少包含:
runtime 必须在 Xfer 前将整个事务组作为一个整体接受或拒绝。commit 时同时
更新两个 Queue,并唤醒两个 Queue 的相关订阅者。
需要完成的编译器和 runtime 工作包括:
RTL lowering 意图
该 primitive 应能直接映射成同步 FIFO 控制逻辑:
source FIFO 和 destination FIFO 的状态在同一个时钟边沿更新。
本 Issue 不要求同时实现 RTL backend,但 Core 语义不应阻碍上述直接
lowering。
验收测试
非目标
本 Issue 不包含:
try_send/try_recv模式;在该 primitive 稳定后,ACPy 和标准组件可以在其上构建结构化仲裁、
Crossbar 和 transfer-selection 等更高层封装。