如何验证 LR/SC 序列的约束（RISC-V ISA）答案

【问题标题】：How to verify constraints of LR/SC sequence (RISC-V ISA)如何验证 LR/SC 序列的约束（RISC-V ISA）
【发布时间】：2020-04-23 12:38:27
【问题描述】：

我已经阅读了关于 RV32A 扩展的 RISC-V 规范，我有一个问题：如果程序执行这些指令，CPU 如何验证 LR/SC 序列的约束：

lr.w x6,x0,(x0)
jal x0,dest
.......
beq x0,x0,-1
.......
dest:
sc.w x1,x6,(x0)

规范说“为了保证序列最终成功，在 LR 和 SC 指令之间执行的动态代码只能包含来自基本“I”指令集中的其他指令，不包括加载、存储、向后跳转或采用后向分支，JALR、FENCE、FENCE.I 和 SYSTEM 说明。”。

因此，如果程序跳过 beq（采用违反上述约束的反向分支），CPU 如何检测 'beq' 出现在 LR/SC 序列中。在我的设计中，如果程序执行上述指令，硬件无法检测到'beq'，那么SC可以成功地将数据存储到数据存储器中，但实际上应该导致存储失败。

【问题讨论】：

【解决方案1】：

beq 不是 LR 和 SC 之间执行的动态代码的一部分。这并不违反您引用的约束，因为beq 不执行。它只是坐在内存中无所事事，就像您使用 jal 跳过的所有其他潜在兆字节内存一样。

动态表示按执行顺序，静态表示按内存地址顺序。

此外，CPU 不是需要来使此类序列总是失败，它只是允许。因此，如果程序员想要确保每个 RISC-V CPU 都可以通过 LR/SC 序列而不会因为某些特定的非法条件（如执行向后beq而中止），程序员应该避免使用它们。

【讨论】：