以下使用QC SC 和 L 代指三者。
動機
多線程執(zhí)行琢唾，如何描述線程之間的相互關聯(lián)的方法和強度载荔。
-
QC適合描述計數器，只要保證計數不重不漏就可以了采桃。 -
SC是現代架構讀寫內存的一種模式(使用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.
-
L則是最強的要求，也是最常見的要求普办，比如queue stack 等數據結構的操作工扎。
定義
QC要求當出現時間點沒有任何程序執(zhí)行的時候，那么該時間點之前和時間點之后的程序執(zhí)行的順序不可以改變衔蹲。而
SC則要求肢娘，每一個線程函數調用都是按照程序順序執(zhí)行的，但是程序之間的順序沒有關系舆驶。 因為兩個線程的函數調用的先后關系沒有要求橱健，所以，下面兩種情況對于SC是等價的
// A:
P1 -- q.enq(x) -----------------------------
P2 ---------------------------- q.deq():x --
// B:
P1 ----------------------q.enq(x) ----------
P2 ---q.deq():x ----------------------------
- 當
L在SC的要求沙廉，如果兩個函數調用沒有重疊拘荡，那么函數調用順序不可改變。所以對于上面舉得例子撬陵，在L看來就是不同的俱病，而且例子B沒有就不滿足L，因為q看到自己首先dequeu出來了x 然后才enqueue了一個x袱结。還有一個很容易理解的說法亮隙，L希望程序的執(zhí)行是瞬間發(fā)生，所以重疊的兩個函數的順序沒有要求垢夹，但是不重疊的函數的順序關系必須保持溢吻。
A sequential history H is legal if each object subhistory is legal for that object.
為什么要強調函數調用的移動，因為給定一個歷史(History)，進行函數調用的移動總是為了將該歷史變化為一個合法歷史促王，如果先后順序的約束強犀盟，那么意味著不能更加難以轉換為合法歷史。
關系
Linearizability 是 sequential consistency 的子集蝇狼，因為 linearizability 是在 sequential consistency 的基礎上添加了一個保持沒有 overlapping 的順序的要求阅畴。
-
quiescent consistency 和 sequential consistency 沒有包含關系，其實容易理解迅耘，
僅僅滿足
SC但是不滿足L纽哥，
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 的。
-
L也是可組合的栖秕，證明方法是遞歸的方法(假設對于任意小于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 的吼句，但是沒有保證獲得返回需要的步數，所以這三個一致性描述和wait free之類blocking描述其是對于一個函數或者對象兩個維度的描述梯投。
For now, it suffices to recall the two key properties of their design: safety, defined by consistency conditions, and liveness, defined by progress conditions
雜談
- 證明一個函數是可線性化的一般方法是什么 ?
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 lineariza?tion point is typically a single step where the effects of the method call become
visible to other method calls.
- 對于可線性化的形式化證明體系命辖，其基本的策略是什么 ?
TODO
