缓存一致性的形式化定义
- 缓存一致性形式化定义 原文
Parallel Computer Architecture - A Hardware Software Approach(DRAFT).pdf P266More formally, we say that a multiprocessor memory system is coherent if the results of any execution
of a program are such that, for each location, it is possible to construct a hypothetical
serial order of all operations to the location (i.e., put all reads/writes issued by all processors into
a total order) which is consistent with the results of the execution and in which:
1. operations issued by any particular processor occur in the above sequence in the order in
which they were issued to the memory system by that processor, and
2. the value returned by each read operation is the value written by the last write to that location
in the above sequence.
第一种翻译
N个待研究的location程序中 M(M>=2) 个cpu , 两个及以上cpu 共同 操作的 location 的 个数 为 N特定 location(location 1) 下 , 假设 操作了该location 的CPU的个数为 P , P>=2 && P<=M基于 location 1 跑出来 的 不确定个数的 结果 P个cpu 都操作了 location 1,那么 都操作完之后 会有一个结果 , 结果是 L1_R1P个cpu 都操作了 location 1,那么 都操作完之后 可能会有第二个结果 , 结果是 L1_R2...基于 location 1 的形式化结果形式化要求如下我们把 P个cpu 的操作 排列成一个假象的串行操作序列,在这个序列中1. 对于上述构造的操作序列来说，每个处理器自己发出的操作，必须保持该处理器本身的发出顺序（即操作在程序中发出到内存系统的顺序）2. 对于上述序列中的每一个读操作，它所返回的值必须是这个序列中，在它之前的最后一次写操作所写入的值基于这个形式化要求的结果 , 即 形式化结果是一个集合 L1_RS如果 L1_R1 L1_R2 ... 都是 集合 L1_RS 中的元素那么 我们就说 "在location 1, 符合 multiprocessor memory system is coherent"所有location 下如果 在 N 个 location 中的 任意一个 location ,都符合 符合 multiprocessor memory system is coherent那么我们就说 multiprocessor memory system is coherent
第二种翻译
给定一个并行程序中：
- 有 N 个待分析的 memory location；
- 有 M (M ≥ 2) 个处理器；
- 每个 location 至少被两个处理器操作（即参与共享），我们记为：该 location 被 P 个处理器操作，其中 2 ≤ P ≤ M。
对于一个特定的 location Li，被 P 个处理器共同访问，执行该程序一次，可能得到一个观测结果 Li_R1，
执行相同程序的另一次可能得到另一个结果 Li_R2，依此类推。
每个结果描述了一组读写顺序与每个读操作所读到的值。
对于某个具体的 location Li，如果存在某个“假设的串行操作序列”（hypothetical serial order）满足：
- 该序列包括所有对 Li 的读写操作；
- 每个处理器对 Li 发出的操作，在该序列中保持其发出顺序（program order）；
- 每个读操作的返回值，等于该序列中其之前最近的一次写操作的写入值；
且该序列能解释该次执行中所有处理器对 Li 的读写观察结果，
那么我们称该次执行结果为 Li 的一个合法一致性结果。
如果对 Li 的所有可能执行结果(Li_R1 Li_R2 …)，都可以被某个满足上述三条规则的串行序列解释，
那么我们称 Li 在该系统下是coherent（一致的）。
若系统中每个共享的 memory location Li（1 ≤ i ≤ N）都满足上述 coherence 条件，
则我们称该 multiprocessor memory system 是 coherent 的。
注意 :
- 这里描述的序列,是不存在的,不对应任何实现下的序列,不要将这个序列与 任何 实现 挂钩.
- 针对一个地址, 只要实现跑出来的结果在集合中即可.实际顺序如何都无所谓.
- point1 和 point2 主要是重点 描述 形式化定义 和 实际实现 的 割裂感,不要混淆.
- 缓存一致性 考虑的是 多个CPU 对 同一个地址 的访问