x86-TSO : 適用於x86體系架構併發編程的內存模型

 Abstract :

　　現在大數據，雲計算，分佈式系統等對算力要求高的方向如火如荼。提高計算機算力的一個低成本方法是增長CPU核心，而不是提升單個硬件工做效率。

　　這就要求軟件開發者們能準確，熟悉地運用高級語言編寫出可以充分利用多核心CPU的軟件，同時程序在高併發環境下要準確無誤地工做，尤爲是在商用環境下。

　　可是作爲軟件工程師，實際上不太可能花大量的時間精力去研究CPU硬件上的同步工做機制。

　　退而求其次的方法是總結出一套比較通用的內存模型，而且運用到併發編程中去。

　　本文結合對CPU的黑盒測試，介紹一個可以通用於 x86 系列CPU的併發編程的內存模型。

　　此內存模型 被測試在 AMD 與 x86 系列CPU上具備可行性，正確性。

---

本文章節：

　　1.關於各型號CPU的說明書規定或模型規定

　　2.官方發佈的黑盒測試及它們可復現/不可復現的CPU型號

　　3.指令重排的發生

　　4.根據黑盒測試定義抽象內存模型 x86-TSO

　　5.A Rigorous and Usable Programmer’s Model for x86 Multiprocessors 的發佈團隊在AMD/Intel系列CPU上進行的一系列黑盒測試及它們與x86-TSO模型結構的關係

　　6.擴展

　　　　6.1 經過Hotspot源碼分析 java volatile 關鍵字的語意及其與x86-TSO/普通TSO內存模型的關係

　　　　6.2 Linux內存屏障宏定義 與 x86-TSO 模型的關係

　　7.總結

　　8.參考文獻

---

 

1.各個型號CPU的規定

CPU相關的模型或規定：

　　x86-CC 模型（出自 The semantics of x86-CC multiprocessor machine code. In Proc. POPL 2009, Jan. 2009）

　　IWP (Intel White Paper，英特爾在2007年8月發佈的一篇CPU模型準則，內容給出了P1~P8共8條規則，而且用10個在CPU上的黑盒測試

　　來支持這8條規則)

　　Intel SDM (繼承IWP的Intel 模型)

　　AMD3.14 說明手冊對CPU的規定

---

 

2.官方黑盒測試　　

　　下面的可在...觀察到，不可在...觀察到，都是針對 最後的 State 而言，亦即 Proc 0: EAX = 0 ^ ... 語句表示的最終狀態

　　其中倒着的V是且的意思

　　如下提到的StoreBuffer即CPU核心暫時緩存寫入操做的物理部件，StoreBuffer中的寫入操做會在任意時刻被刷入共享存儲（主存/緩存），前提是總線沒被鎖/緩存行沒被鎖

　　如下提到的Store Fowarding 指的是CPU核心在讀取內存單元時 會去 StoreBuffer中尋找該變量，若是找到了就讀取，以便獲得該內存單元在本核心上最新的版本

---

　  1.測試SB : 可在現代Intel CPU 和 AMD x86 中觀察到

　　核心0 和 核心1 各有本身的Store Buffer，會形成上述狀況。

　　核心0將 x = 1 緩存在本身的StoreBuffer裏，而且從共享內存中獲取 y = 0，之因此見不到 y = 1 是由於 核心1 將 y = 1 的操做緩存在本身的StoreBuffer裏

　　核心1將 y = 1 緩存在本身的StoreBuffer裏，而且從共享內存中獲取 x = 0，沒法見到 x = 1 與上述同理

---

 

　  2.測試IRIW : 實際上不容許在任何CPU上觀察到，可是有的CPU模型的描述可能讓該測試發生

    

　　若是 核心0 和 核心2 共享 StoreBuffer，由於讀取時會先去 StoreBuffer 讀取修改，因此 核心0 執行的 x = 1 會被 CPU2 讀取，故 EAX = 1 , 由於核心1 和 核心2 不共享StoreBuffer，核心1 的 y = 1 操做緩存在本身和核心3的共享StoreBuffer中

　　因此 EBX = 0 ， CPU3的寄存器狀態同理 

---

 

　 3.測試n6 : 在 Intel Core 2 上能夠觀察到，但倒是被X86-CC模型和IWP說明禁止的

　　核心0 和 核心1 有各自的Store Buffer

　　核心0將 x = 1 緩存在本身的Store Buffer 中，而且根據 Store Forwarding 原則 , 核心0 讀取 x 到 EAX 的時候

　　會讀取本身的Store Buffer，讀取x 的值是 1，故EAX = x = 1

　　同理，核心1也會緩存本身的寫操做， 即緩存 y = 2 和 x = 2 到本身的 StoreBuffer，所以 y = 2 這個操做不會被

　　核心0 觀察到，核心0 從主內存中加載 y 。故 EBX = y = 0

---

 

　　4.測試n5 / n4b ：實際上不能在任何CPU上觀察到

   

　　n5和n4b是一樣類型的測試，假如 核心0和 核心1都有本身的StoreBuffer

　　對於n5，核心0的EAX若是等於2，那麼說明 核心1的StoreBuffer刷入到 共享的主存中, 那麼 EAX = x 必然=執行於 x = 2

　　以後，一位 x = 1 對 EAX = x 來講是有影響的，EAX = x 和 x = 1 禁止重排，那麼 x = 1 必然不能出如今 x = 2 以前，

　　更不可能出如今 ECX = x 以前 （x = 2 對 ECX = x 也是有影響的，語義上嚴禁重排）

　　對於n4b，若是EAX = 2 ，說明 核心1的 x = 2 操做已經刷入主存被 核心0 觀察到，那麼對於 核心0來講 x = 2 先於 EAX = x 執行

　　同上理，ECX = x 和 x = 2 也是嚴禁重排的，故 ECX = x 要先於 EAX = x 執行，更先於 x = 1 執行

 

　　n5 和 n4b 測試在AMD3.14 和Intel SDM 中好像是能夠被容許的，也就是上面的 Forbidden Final State 被許可，但實際上不能

　　A Rigorous and Usable Programmer’s Model for x86 Multiprocessors 中做者原話 ： However, the principles stated in revisions 29–34 of the Intel SDM appear, presumably unintentionally, to allow them. The AMD3.14 Vol. 2, §7.2 text taken alone would allow them, but the implied coherence from elsewhere in the AMD manual would forbid them

---

 

　　其實是概念模型若是從局部描述，沒有辦法說確切，可是從總體上看，整個模型的說明不少地方都禁止了n5和n4b的發生，可見想描述一個鬆散執行順序的CPU模型是多麼難的一件事。軟件開發者也沒辦法花大量的時間精力去鑽研硬件的結構組成和工做原理，只能依靠硬件廠商提供的概念模型去理解硬件的行爲

　　在AMD3.15的模型說明中，語言清晰地禁止了IRIW，而不是模棱兩可的否認。

　　如下表格總結了上述的黑盒測試在不一樣CPU模型中的觀察結果（3.14 3.15是AMD不一樣版本的模型，29~34是Intel SDM在這個版本範圍的模型）

    

---

 

 3.指令重排的發生　

　　上述的黑盒測試的解釋中，提到了重排的概念，讓咱們看一下從軟件層面的指令到硬件上，哪些地方可能出現 重排序：

　　CPU接收二進制指令流，流水線設計的CPU會依照流水線的方式串行地執行每條指令的各個階段

　　舉例描述：一個餐廳裏 每一個人的就餐須要三個階段：盛飯，打湯，拿餐具。有三個員工，每人各負責一個階段，顯然每一個員工只能同時處理一個客人，也就是同一時刻，同一階段只能有一個客人，也就是任什麼時候刻不可能出現兩位客人同時打湯的狀況，固然也不可能出現兩個員工同時服務一個客人。能造成一條有條不紊的進餐流水線，不用等一個客人一口氣完成3個階段其餘客人才能開始盛飯。

　　對於CPU也是，指令的執行分爲 取指，譯碼，取操做數，寫回內存 等階段，每一個階段只能有一條指令在執行。

　　CPU應當有 取值工做模塊，譯碼工做模塊，等等模塊來執行指令。每種模塊同一時刻只能服務一條指令，對於CPU來講，流水線式地執行指令，是串行的，沒有CPU聰明到給指令重排序一說，若是指令在CPU內部的執行順序和高級語言的語義順序不同，那麼極可能是編譯器優化重排，致使CPU接受到的指令

原本就是編譯器重排過的。

　　真正的指令重排出如今StoreBuffer的不可見上，緩存一致性已經保證了CPU間的緩存一致性。具體重拍的例子就是第一個黑盒測試SB: 

　　初值：x = 0, y = 0

     

 

　  在咱們常規的併發編程思惟中，會爲這4條語句排列組合（按咱們的認知，1必定在2以前，3必定在4以前），而且認爲不管線程怎麼切換，這四條語句的排列組合（1在2前，3在4前的組合）必定有一條符合最後的實際運行結果。假如按照 1 3 2 4 這樣的組合來執行，那麼最後 EAX = 1 , EBX = 1，或者 1 2 3 4 這樣的順序來執行，最後 EAX = 0 且 EBX = 1，怎麼都不可能 EAX = 0, EBX = 0 

　  但實際上SB測試能夠在Intel系列上觀察到，從軟件開發者的角度上看，就好像 按照 2 4 1 3 的順序執行了同樣，如同 2 被排在1 以前，3 被排在4 以前，是所謂 指令重排 的一種狀況 

　  實際上，是由於StoreBuffer的存在，才致使了上述的指令重排。

　  試想一下，CPU0將 x = 1 指令的執行緩存在了本身的StoreBuffer裏，CPU1也把 y = 1 的執行緩存在本身的StoreBuffer裏，這樣的話當二者執行各自的讀取操做的時候，亦即CPU0執行 EAX = y

CPU1執行 EBX  = x , 都會直接去緩存或主存中讀取，而緩存又MESI協議保證一致，可是不保證StoreBuffer一致，因此二者沒法互相見到對方的StoreBuffer中對變量的修改，因而讀到x, y都是初值 0

 　

---

 

4.根據黑盒測試定義抽象內存模型 x86-TSO

    　從以上的試驗沒法總結出一套通用的內存模型，由於每一個CPU的實現不一樣，可是咱們能夠總結出一個合理的關於x86的內存模型

　　而且這個模型適合軟件開發者參考，而且符合CPU廠商的意圖

　　首先是關於StoreBuffer的設計：

　　　　1.在Intel SDM 和 AMD3.15模型中，IRIW黑盒測試是明文禁止的，而IRIW測試意味着某些CPU能夠共享StoreBuffer因此咱們想創造的合理內存模型不能讓CPU共享StoreBuffer

　　　　2.可是在上述黑盒測試中，好比n6和SB，都證實了，StoreBuffer確實存在

　　　　總結:StoreBuffer存在且每一個CPU獨佔本身的StoreBuffer

　　上述的黑盒測試代表，除了StoreBuffer形成的CPU寫不能立刻被其餘CPU觀察到，各個CPU對主存的觀察應該都是一致的，能夠忽略掉緩存行，由於MESI協議會保證各個CPU的緩存行之間的一致性，可是沒法保證StoreBuffer中的內容的一致性，由於MESI是緩存一致性協議，每一個字母對應緩存（cache）的一種狀態，保證的只是緩存行的一致性。

 

　 總結一下：咱們想構造的x86模型的特色：

　　　1. 在硬件上必然是有StoreBuffer存在的，設計時須要考慮進去

　　   2. 緩存方面由於MESI協議，各個CPU的緩存之間不存在不一致問題，因此緩存和主存能夠抽象爲一個共享的內存

　　   3. 額外的一個特色是 總線鎖，x86提供了 lock 前綴 ，lock前綴能夠修飾一些指令來達到 read-modify-write 原子性的效果，好比最多見的 read-modify-write 指令 ADD，CPU須要從內存中取出變量，

加一後再寫回內存，lock前綴可讓當前CPU鎖住總線，讓其餘CPU沒法訪問內存，從而保證要修改的變量不會在修改中途被其餘CPU訪問，從而達到原子性 ADD 的效果。在x86中還有其餘的指令自帶

lock 前綴的效果，好比XCHG指令。帶鎖緩存行的指令在鎖釋放的時候會把StoreBuffer刷入共享存儲

　最後能夠獲得以下模型：

　　

　　其中各顏色線段的含義：

　　紅色：CPU的各個核心能夠爭奪總線鎖，佔有總線鎖的CPU能夠將本身的storeBuffer刷入到共享存儲中（其實總線鎖不是真的必定要鎖總線，也能夠鎖緩存行，若是要鎖的目標不僅一個緩存行，則鎖總線），佔有期間其餘CPU沒法將本身的storeBuffer刷入共享存儲

　　橙色：根據StoreFowarding原則，CPU核心讀取內存單元時，首先去StoreBuffer讀取最近的修改，而且x86的StoreBuffer是遵循FIFO的隊列，x86不容許CPU直接修改緩存行，因此StoreStore內存屏障在x86上是空操做，由於對於一個核心來講，寫操做都是FIFO的，寫操做不會重排序。x86不容許直接修改緩存行也是緩存和主存能抽象成一體的緣由。

　　紫色:  核心向StoreBuffer寫入數據，在一些英文文獻中會表示爲：Buffered writes to 變量名，也就是對變量的寫會被緩存在StoreBuffer，暫時不會被其餘CPU觀察到

　　綠色:  CPU核心將緩存的寫操做刷入共享存儲，除了有其餘核心佔有鎖的狀況 (由於其餘核心佔有鎖的話，鎖住了緩存行或總線，則當前核心不能修改這個緩存行或訪問共享存儲)，任何狀況下，StoreBuffer均可以被刷入共享存儲

　　藍色：若是要讀取的變量不在StoreBuffer中，則去共享存儲讀取（緩存或主存）

---

5.A Rigorous and Usable Programmer’s Model for x86 Multiprocessors 的發佈團隊在AMD/Intel系列CPU上進行的一系列黑盒測試及它們與x86-TSO模型結構的關係

　　在A Rigorous and Usable Programmer’s Model for x86 Multiprocessors 一文中，做者爲了驗證x86-TSO模型的正確性，在廣泛流行的 AMD和 Intel 處理器上使用嵌入彙編的C程序進行測試。

而且使用memevents工具監視內存而且查看最終結果,而且用HOL4監控指令執行先後寄存器和內存的狀態，最後進行驗證，共進行了4600次試驗。

　　結果以下：

       1.寫操做不容許重排序，不管是對其餘核心來講仍是本身來講

　　

　　解釋：

　　從核心1 的角度看 核心0，x 和 y 的寫入順序不能顛倒　　

　　從x86-TSO模型的物理構件角度解釋就是，寫操做會按照 FIFO 的規則 進入 StoreBuffer，而且按照FIFO的順序刷入共享存儲，因此 寫操做沒法重排序。

　　因此 x = 1 寫操做先入StoreBuffer隊列，接着 y = 1 入，刷入共享存儲的時候， x = 1 先刷入，y = 1 再刷入， 因此若是 y 讀到 1 的話，x 必定不能是 0

---

 

　　2.讀操做不能延遲 ：對於其餘核心來講，對於本身來講若是不是同一個內存單元，是否重排可有可無，（由於讀不能通知寫，只有寫改變了某些狀態才能通知讀去作些什麼， 好比 x = 1; if (x == 1); ）

　　

　　解釋：

　　從核心1的角度觀察，若是EBX = 1 , 那麼說明 核心0的 y = 1 操做已經從 StoreBuffer中刷入到共享存儲，以前說過，CPU流水線執行指令在物理上是不能對指令流進行重排的，因此 EAX = x 的操做 在 y = 1 以前執行

　　同理，EBX = y 這個讀操做也不能延後到 x = 1 以後執行，因此 EAX = x 先於 y = 1 ，y = 1 先於 EBX = y , EBX = y 先於 x = 1 , 因此 EAX 不可能接受到 x = 1 的結果

---

 

　　3.讀操做能夠提早：上述2是讀操做不能延後，可是能夠提早，而且是從其餘核心的角度觀察到的

　　例子是 上面的 SB測試，

　　

 

　　若是忽視StoreBuffer，從核心1的角度看，EBX = 0，說明 x = 1 未執行，那麼 EBX = x 應該在 x = 1 以前執行，又由於 y = 1 在 EBX = x 以前，那麼 y = 1 應該在 x = 1 以前，EAX = y 在 x = 1 以後，理應在 y = 1 以後

　　那麼EAX 理應 = 1。

　　

　　可是最後狀態能夠二者均爲0.。就好像 讀取的指令被從新排到前面（下面是一種重排狀況）

         

 

 　在x86-TSO模型中，寫操做是容許被提早的，從物理硬件的角度解釋以下：

　 假設核心0是左邊的核心，核心1是右邊的核心，若是二者都把 寫操做緩存在 StoreBuffer中，而且讀操做執行以前，StoreBuffer沒有同步回共享存儲，那麼二者讀到的 x 和 y 都來自共享存儲，而且都是 0。

    

---

 

　　4.對於單個核心來講，由於Store Forwarding 原則，同一個內存單元 以前的寫操做必對以後的讀操做可見

 　　

　　解釋：對一個核心而言，本身的寫入是能立刻爲本身所見的

---

 

 　　5.寫操做的可見性是傳遞的，這一點與 happens-before 原則的傳遞性相似，若是 A 能 看到 B 的動做，B能看到 C 的動做，那麼 A必定能看到C 的動做

　　

 

　　解釋： 對於核心1，若是EAX = 1 ，那麼說明核心1已經見到了 核心0的動做，對於核心2，EBX = 1，說明核心2已經見到了 核心1的動做，又根據以前的 讀操做不能延後，EAX = x 不能延遲到 y = 1 以後，

　　因此 核心2 必能見到 核心0 的動做，因此 ECX = x 不能爲 0

---

 

　　6.共享存儲的狀態對全部核心來講都是一致的

　　上面的IRIW測試就是違反共享內存一致性的例子：

　　

 

　　核心2 和 核心3 觀察到 核心0 和 核心1 的行爲，那麼他們的行爲應該都是同樣的，由於都刷入到共享存儲中了

---

 

　　7.帶lock前綴的指令或者 XCHG指令，會清空StoreBuffer，使得以前的寫操做立刻被其餘核心觀察到

　　

 

　　解釋：EAX一開始是1，將EAX的值寫入 x ，核心0 的 XCHD會把StoreBuffer清空，亦即將 x = EAX (1) 刷入共享存儲，核心1若是看到 x = 0 (EDX = 0 )，說明 x = EAX 在後面才執行。推得y = ECX 在 x = EAX 以前執行

　　y = ECX 也會立刻刷入共享存儲，必然對 核心 0 可見，因此 最後不可能 x = 0, y = 0

　　

 

　　MFENCE指令在x86-TSO模型上也能達到刷StoreBuffer的效果。

 

---

　　總結：在x86-TSO模型上，惟一可能重排序的清空是 讀被提早了（從多個CPU的視角看），其實是 StoreBuffer緩存了寫操做，致使寫操做沒寫出來。

---

6.擴展：

　　6.1 經過Hotspot源碼分析 java volatile 關鍵字的語意及其與x86-TSO/普通TSO內存模型的關係

　　Java 的 volatile語意：Hotspot實現

　　

　　在JVM的字節碼解釋器中，若是putstatic字節碼或putfield字節碼的變量是java層面的volatile關鍵字修飾的，就會在指令執行的最後插入一道 storeLoad 屏障，前文已經說過，在x86中

　　惟一可能重排的是 讀操做提早到 寫操做以前，這裏的storeLoad操做作的就是阻止重排

　　

　　在os_cpu/linux_x86下的實現以下：

　　其實只是執行了一條帶lock前綴的空操做嵌入彙編指令（棧頂指針+0是空操做），實現的效果就是把StoreBuffer中的內容刷入到 共享存儲中

　　其實還有一層增強， __ asm __ 後面的volatile關鍵字 會阻止編譯器對本條指令先後的指令重排序優化，這保證了CPU獲得的指令流是符合咱們程序的語意的

 　　

 　　在模板解釋器中： 

　　

 　  

　　一開始我驚訝於此，這句話沒有爲不一樣平臺實現選擇不一樣的實現方法，而是簡單檢查若是不是須要 storeLoad 屏障就跳過。

 　 

　 其實做者註解已經說的很明白，如今大部分RISC的SPARC架構的CPU的實現都知足TSO模型，因此只須要StoreLoad屏障而已

　 我在新南威爾斯大學的網站上找到了關於TSO的比較正宗的解釋：

  

 　下面的討論中，是否須要重排序是根據CPU最後的行爲是否符合咱們高級語言程序的語意順序決定的，若是相同則不須要，不相同則須要。

 　也就是單個核心中，寫操做之間是順序的，會按二進制指令流的寫入順序刷到共享存儲，不須要考慮重排的狀況，因此不須要StoreStore屏障

　 遵循Store Forwarding，因此對於本核心，本核心的寫操做對後續的讀操做可見。這三點已經十分符合本文的x86-TSO模型。

　 有一點沒有呈現，就是單個CPU核心中，是否禁止讀延遲，也就是寫操做不能跨越到讀操做以前，根據上面的 只有StoreLoad 屏障有操做，其餘屏障，包括LoadStore屏障無操做能夠推斷

　 普通的TSO模型也是遵循禁止讀延遲原則的

---

 　　6.2 Linux內存屏障宏定義 與 x86-TSO 模型的關係

 　　Linux 的內存屏障宏定義　 

 　　在Linux下定義的具備全功能的內存屏障，是有實際操做的，和JVM的storeLoad一模一樣

　　 讀屏障是空操做，寫屏障只是簡單的禁止編譯器重排序，防止CPU接收的指令流被編譯器重排序。

 　　只要編譯器能編譯出符合咱們高級語言程序語意順序的二進制流給CPU，根據TSO模型的，CPU執行這些指令流的中的寫操做對外部呈現出來的（刷入共享存儲被全部CPU觀察到）就是FIFO順序

　　 讀操做不涉及任何狀態變動，因此不須要內存屏障（也許只有在x86上纔不須要，在其餘有Invaild Queue的CPU結構中或許須要）

---

7.總結

本文總結：

　　x86-TSO模型的特色總結：

　　由於緩存有MESI協議保證一致性，因此緩存能夠和主存合併抽象成共享存儲

　　x86-TSO的寫操做嚴格遵循FIFO

　　CPU流水線式地執行指令會使得CPU對接受到的指令流順序執行

　　x86-TSO中惟一重排的地方在於StoreBuffer，由於StoreBuffer的存在，核心的寫入操做被緩存，沒法立刻刷新到共享存儲中被其餘核心觀察到，因此就有了 「 寫 」 比 「讀」 晚執行的直觀感覺，也能夠說是讀操做提早了，排到了寫操做前

　　阻止這種重排的方法是 使用帶 lock 前綴的指令或者XCHG指令，或MFENCE指令，將StoreBuffer中的內容刷入到共享存儲，以便被其餘核心觀察到

---

8.本文參考文獻　

　參考文獻:

　　《Linux內核源代碼情景分析》：毛德操

　　x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors

　　Memory Barriers: a Hardware View for Software Hackers