第一段An invalidate operation may change the set of values that can be returned by a load.翻译：一个 invalidate 操作可能会改变一个 load 所能返回的值的集合。解释：在普通情况下（没有 invalidate），load 看到的值来自某个 store 或内存初始值。执行cbo.inval会丢弃缓存中的副本，使得后续 load 必须从更高级别的缓存或内存重新读取。因此，原来可能从旧缓存中得到的老值，在 inval 之后可能就不再可能出现。所以“可返回值的集合”发生了变化。第二段（关键）In particular, an additional condition is added to the Load Value Axiom:翻译：具体来说，在加载值公理中增加了一个附加条件。背景：RVWMO 内存模型定义了一个“加载值公理”，规定了在全局内存顺序下，一个 load 可能返回哪些值。这个公理原本已经考虑了 stor
