如何验证线性一致性( 二 ) _线性一致性

1，Client1: Invoke Put x=02，Client2: Invoke Put x=13，Client1: Return Put x=04，Client3: Invoke Get x5，CLient4: Invoke Get x6，Client3: Return Get 17，Client4: Return Get 08，Client2: Return Put x=1Output: 执行序列
Client1 Put x=0Client4 Get 0Client2 Put x=1Client3 Get 11，WG算法
请求的调用历史中，存在着一种偏序关系：Prev，如果一个请求的Return发生时间早于另一请求的Invoke，我们便称其Prev另一个请求。显而易见，这种偏序关系是一致性验证算法必须要保留的。祸兮福所倚，也正是这种对偏序关系的保留，给了算法加速的可能。WG算法的思路非常简单：从调用历史中找出没有Prev的项，将其对应的请求执行并取出，之后对剩下的调用历史重复该算法，直到没有更多的调用历史或执行结果不满足。
如上述例子中，“Client1 Put x=0” 和 “Client2 Put x=1” 由于其Invoke前没有任何请求Return，可以首先被取出。假如选择“Client1 Put x=0”，将其对应的Invoke和Return从调用历史中取出，得到新的历史：
2，Client2: Invoke Put x=14，Client3: Invoke Get x5，CLient4: Invoke Get x6，Client3: Return Get 17，Client4: Return Get 08，Client2: Return Put x=1和一条已经序列化的请求：
Client1 Put x=0此时可以看到剩余的历史中，每一个请求的Invoke前都没有其他请求的Return，因此都可以作为下一个取出的选择。假设这次选择Client3 Get 1，然而，明显这个时候执行Get得到应该是0，与该请求的实际执行结果返回1不同，此时，需要回退并尝试其他取出策略。可以看出WG算法其实是树的深度优先搜索，其搜索树如下图，其中每个节点标识的是本次尝试序列化的请求对应的调用历史中的Invoke序号：
由于找到一个线性序列便可以停止，因此其中虚线部分是不会被实际执行的。
2，WGL算法
WGL算法由Gavin Lowe在WG算法的基础上进行改进，其改进的方式主要是对搜索树的剪枝：通过缓存已经见过的配置，来减少重复的搜索。缓存配置有两部分组成：

当前已经序列化的请求
当前x值

由上面的搜索过程可知，如果当前序列化的请求和当前的x值完全相同，则后续的搜索过程一定一致，因此可以略过。
3，P-compositionality算法
P-compositionality算法利用了线性一致性的Locality原理，即如果一个调用历史的所有子历史都满足线性一致性，那么这个历史本身也满足线性一致性。因此，可以将一些不相关的历史划分开来，形成多个规模更小的子历史，转而验证这些子历史的线性一致性，例如kv数据结构中对不同key的操作。上面提到了算法的计算时间随着历史规模的增加急速膨胀，P-compositionality相当于用分治的办法来降低历史规模，这种方法在可以划分子问题的场景下会非常有用。
为什么Solitaire
工程实践中，不只分布式系统，还包括需要并行访问的系统，都可能需要验证系统对外暴露的线性一致性功能。当然也有不少验证线性一致性的工具，比如大名鼎鼎的Jespen使用的Knossos，是一个Clojure版本的WGL的算法实现；Porcupine是一个Go版本的P-compositionality实现；linearizability-checker是P-compositionality算法作者自己实现的一个样例。但使用中还有几个问题没有解决：

计算速度慢：由于上面提到的复杂度，一致性算法验证时间通常是相关测试中的瓶颈。尽可能的加快其计算速度，可以在相同时间内验证更多的历史，对发现系统中的潜在问题至关重要。
数据模型单一：大多数的验证工具面向的都是KV接口，这就要求使用者将千差万别的系统实际接口转化为KV接口使用，而这层转换会掩盖系统中的众多复杂性，比如将Device接口转化为KV后会丢失对相互覆盖操作的验证。
具体问题具体分析：对一些数据模型来说，可能存在多项式甚至是线性复杂度的算法，那么针对这些数据模型使用通用的WGL算法就舍近求远了。

Solitaire(https://github.com/CatKang/Solitaire)是一个C++实现，更快速，支持多数据模型的线性一致性检测工具，致力于解决上述问题。其命名来源于上世纪著名的windows桌面纸牌游戏，要求玩家在保证大小先序关系的限制下，将打乱的扑克牌整理为有序。可以说与我们的线性一致性验证工作非常契合了。

【如何验证线性一致性】