Quiescent consistency，Sequential consistency 和 Linearizability

其实，这个问题我之前一直没有深入的理解，因为我不搞分布式。 但是，在学习 C++ memory model 的时候，我发现有一些东西开始看不懂了。

1. 两个 CPU 写 cache ，那么其他的 CPU 是否需要看到相同的顺序?

但是，Sequential consistency memory model 可以来保证看到的都是一样的?

动机

多线程执行，如何描述线程之间的相互关联的方法和强度。

1. Quiescent consistency 适合描述计数器，只要保证计数不重不漏就可以了。
2. Sequential consistency 是现代架构读写内存的一种模式(使用 fence 或者 memory barrier)。

In the end, the architectures do implement sequential consistency, but only on demand. We discuss further issues related to sequential consistency and the Java programming language in detail in Section 3.8.

1. Linearizability 则是最强的要求，也是最常见的要求，比如 queue stack 等数据结构的操作。

定义

1. Quiescent consistency 要求当出现时间点没有任何程序执行的时候，那么该时间点之前和时间点之后的程序执行的顺序不可以改变。

2. 而 Sequential consistency 则要求，每一个线程内的函数调用都按照程序顺序执行，且所有操作能排成单一全局顺序；但跨线程操作的相对先后没有约束。 因为两个线程的函数调用的先后关系没有要求，所以，下面两种情况对于 Sequential consistency 是等价的

// A:
P1 -- q.enq(x) -----------------------------
P2 ---------------------------- q.deq():x --

// B:
P1 ----------------------q.enq(x) ----------
P2 ---q.deq():x ----------------------------

1. 当 Linearizability 在 Sequential consistency 的要求，如果两个函数调用没有重叠，那么函数调用顺序不可改变。所以对于上面举得例子， 在 Linearizability 看来就是不同的，而且例子 B 没有就不满足 Linearizability， 因为 q 看到自己首先 dequeue 出来了 x 然后才 enqueue 了一个 x。 还有一个很容易理解的说法，Linearizability 希望程序的执行是瞬间发生，所以重叠的两个函数的顺序没有要求，但是不重叠的函数的顺序关系必须保持。

A sequential history H is legal if each object subhistory is legal for that object.

为什么要强调函数调用的移动，因为给定一个历史(History)，进行函数调用的移动总是为了将该历史变化为一个合法历史，如果先后顺序的约束强，那么意味着更加难以转换为合法历史。

关系

1. Linearizability 是 sequential consistency　的子集，因为 linearizability 是在 sequential consistency 的基础上添加了一个保持没有 overlapping 的顺序的要求。
2. quiescent consistency 和 sequential consistency 没有包含关系，其实容易理解，
   1. 这里举出一个是 sequential consistency 但是不是 quiescent concurrency 的例子。
   2. 这里是一个对称的例子
   3. 两者都是 : 对于一个原子寄存器读写。
   4. 两者都不是的例子 : 一个线程 enqueue 一个 1,另一个线程 dequeue 一个 2 出来。
3. 仅仅满足 Sequential consistency 但是不满足 Linearizability，

Compositional

何为组合: A correctness property is compositional if, whenever each object in the system satisfies , the system as a whole satisfies .

• quiescent consistency is compositional

Can we, in fact, compose a collection of independently implemented quiescently consistent objects to construct a quiescently consistent system? The answer is, yes: quiescent consistency is compositional, so quiescently consistent objects can be composed to construct more complex quiescently consistent objects

• Figure 3.8 说明 sequential consistency 不是 compositional 的。
• Linearizability 也是可组合的，证明方法是递归的方法(假设对于任意小于 k 个函数调用的历史是组合的)

Limit Concurrency

在当前上下文中间，not limit concurrency 其实只是说当前历史是符合某种一致性，比如顺序一致性，并且含有 pending 的 inv，那么当其获得 response 的时候，可以保证历史还是满足该一致性。

Linearizability’s nonblocking property states that any pending invocation has a correct response, but does not talk about how to compute such a response.

三者都不会 limit concurrency

• How much does quiescent consistency limit concurrency? Specifically, under what circumstances does quiescent consistency require one method call to block waiting for another to complete? Surprisingly, the answer is (essentially), never.
• How much does linearizability limit concurrency? Linearizability, like sequential consistency, is nonblocking. Moreover, like quiescent consistency, but unlike sequential consistency, linearizability is compositional; the result of composing linearizable objects is linearizable.
• Sequential consistency, like quiescent consistency, is nonblocking: any pending call to a total method can always be completed.

虽然三者都是不会 limit concurrency 的，但是没有保证获得返回需要的步数，所以这三个一致性条件（safety）与 wait-free 之类的进展性条件（progress/liveness）是描述一个函数或对象的两个维度。

For now, it suffices to recall the two key properties of their design: safety, defined by consistency conditions, and liveness, defined by progress conditions

杂谈

1. 证明一个函数是可线性化的一般方法是什么 ?

The usual way to show that a concurrent object implementation is linearizable is to identify for each method a linearization point where the method takes effect. For lock-based implementations, each method’s critical section can serve as its linearization point. For implementations that do not use locking, the linearization point is typically a single step where the effects of the method call become visible to other method calls.

1. 对于可线性化的形式化证明体系，其基本的策略是什么 ?

   TODO

• https://stackoverflow.com/questions/54865399/what-are-the-differences-between-linearizability-and-quiescent-consistency

• https://stackoverflow.com/questions/69925465/how-does-the-x86-tso-memory-consistency-model-work-when-some-of-the-stores-being

就是这个没有理解，导致假设一直有问题，实在是关键

参考

• 周刊（第 22 期）：图解一致性模型

https://lotabout.me/2019/QQA-What-is-Sequential-Consistency/

• 介绍什么是顺序一致性

分析一下这些

3.4　一致性模型 3.4.1　线性一致性 3.4.2　实现线性一致性 3.4.3　线性一致性的代价 3.4.4 顺序一致性 3.4.5　因果一致性 3.4.6　最终一致性

3. 顺序一致性

Lamport 对顺序一致性的形式化定义是：任何执行的结果都等同于所有处理器的操作按某种顺序依次执行的结果，并且每个单独处理器的操作在此序列中按其程序顺序出现。

顺序一致性包含两个核心方面：

1. 程序顺序：维护单个处理器操作之间的顺序。
2. 原子性/全局串行化：维护所有处理器操作之间的单一全局顺序，使每个操作看起来瞬时完成。

图 4 用 Dekker 算法示例说明程序顺序的重要性，用多处理器共享变量示例说明原子性的重要性。

本站所有文章转发 CSDN 将按侵权追究法律责任，其它情况随意。