- 來自Leslie Lamport的經(jīng)典論文《How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs》：
" Consider a computer composed of several such processors accessing a common memory. The customary approach to designing and proving the correctness of multiprocess algorithms for such a computer assumes that the following condition is satisfied : the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individula processor appear in this sequence in the order specified by its program. A multiprocessor satisfying this condition will be called sequentially consistent." --- LESLIE LAMPORT
【案例1】只有兩個進程的互斥協(xié)議
process 1 ：
a = 1; //1
if (b == 0) {//2
// 進入臨界區(qū)域
a = 0;
// 退出臨界區(qū)域
}else {
// 執(zhí)行其他操作
}
process 2 ：
b = 1;//3
if (a == 0) {//4
// 進入臨界區(qū)域
b = 0;
// 退出臨界區(qū)域
}else {
// 執(zhí)行其他操作
}
分析：
如果process 1先執(zhí)行if(b==0)或者process 2先執(zhí)行if (a==0)，即存在一個進程的執(zhí)行順序和定義順序不一致（可能是由于編譯器或者處理器的優(yōu)化措施導(dǎo)致）兄裂，就有可能導(dǎo)致兩個進程同時進入臨界區(qū)域检碗，從出現(xiàn)錯誤。因此必須要求：從單個進程來看询一，每個處理器的執(zhí)行順序必須和定義順序一致，從而就禁止了編譯器或者處理器的優(yōu)化措施爆存。
從上述要求1株扛，可以得出下面兩個有用的推論：
- 從全局的角度养距，每個CPU看到的其他CPU的寫操作都是按照相同的順序執(zhí)行的诉探，看到的最終執(zhí)行的視圖是一致的；
- 單個CPU對共享變量的寫操作馬上對其他CPU可見
證明：假設(shè)單個CPU對共享變量的寫操作不是馬上對其他CPU可見的棍厌，即在當前線程把寫過的數(shù)據(jù)緩存在本地內(nèi)存中肾胯，且還沒有刷新到主內(nèi)存之前，這個寫操作僅對當前線程可見耘纱；從其他線程的角度來觀察敬肚，會認為這個寫操作根本還沒有被當前線程執(zhí)行。只有當前線程把本地內(nèi)存中寫過的數(shù)據(jù)刷新到主內(nèi)存之后束析，這個寫操作才能對其他線程可見艳馒。在這種情況下，當前線程和其它線程看到的操作執(zhí)行順序?qū)⒉灰恢禄福瑥亩`反推論1鹰溜。
【案例2】假設(shè)每個內(nèi)存模塊都有多個端口虽填，一個端口服務(wù)一個處理器丁恭。假設(shè)a和b被存儲在不同的內(nèi)存模塊中，現(xiàn)在發(fā)生了以下事件：
處理器1向內(nèi)存塊1上專用于服務(wù)處理器1的端口發(fā)送
a=1的請求斋日。但是內(nèi)存塊1正忙于執(zhí)行其他處理器的操作牲览；處理器1向內(nèi)存塊2上專用于服務(wù)處理器1的端口發(fā)送
fetch b的請求。內(nèi)存2是空閑的恶守，則開始執(zhí)行第献，進入臨界區(qū)；處理器2向內(nèi)存塊2上專用于服務(wù)處理器2的端口發(fā)送
b=1的請求兔港。這個請求在處理器1的fetch b完成后開始執(zhí)行庸毫；4)處理器2向內(nèi)存塊1上專用于服務(wù)處理器2的端口發(fā)送
fetch a的請求。此時內(nèi)存塊1還忙于執(zhí)行其他處理器的操作衫樊；
現(xiàn)在有兩個操作等著被內(nèi)存塊2執(zhí)行飒赃，如果處理器2的fetch a請求先被執(zhí)行，則同時有兩個進程進入臨界區(qū)域科侈。進而有第二個要求：
單個內(nèi)存塊必須按照先來先服務(wù)的規(guī)則來處理來自多個處理器的所有請求载佳。
- 來自Java1.7語言規(guī)范里的[https://docs.oracle.com/javase/specs/jls/se7/html/jls-17.html#jls-17.4.5](Java Memory Model)里的定義：
A set of actions is sequentially consistent if all actions occur in a total order (the execution order) that is consistent with program order, and furthermore, each read r of a variable v sees the value written by the write w to v such that:
- w comes before r in the execution order, and
- there is no other write w' such that w comes before w' and w' comes before r in the execution order.
Sequential consistency is a very strong guarantee that is made about visibility and ordering in an execution of a program. Within a sequentially consistent execution, there is a total order over all individual actions (such as reads and writes) which is consistent with the order of the program, and each individual action is atomic and is immediately visible to every thread.
If a program has no data races, then all executions of the program will appear to be sequentially consistent.
Sequential consistency and/or freedom from data races still allows errors arising from groups of operations that need to be perceived atomically and are not.
If we were to use sequential consistency as our memory model, many of the compiler and processor optimizations that we have discussed would be illegal.
【參考資料】
- https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/How-to-Make-a-Multiprocessor-Computer-That-Correctly-Executes-Multiprocess-Programs.pdf
- 《聊聊高并發(fā)（三十三）Java內(nèi)存模型那些事（一）從一致性(Consistency)的角度理解Java內(nèi)存模型》http://blog.csdn.net/iter_zc/article/details/41943387
- 《深入理解Java內(nèi)存模型（三）——順序一致性》http://www.infoq.com/cn/articles/java-memory-model-3
- 《為什么程序員需要關(guān)心順序一致性（Sequential Consistency）而不是Cache一致性（Cache Coherence？）》
http://www.infoq.com/cn/articles/java-memory-model-3
