硬件內存模型 Hardware Memory Models

(Memory Models, Part 1)

Posted on Tuesday, June 29, 2021.

簡介：童話的終結

很久以前，當人們還在寫單線程程序的時候，讓程序跑的更快的一個最有效的辦法就是什么也不做，因為下一代硬件和編譯器的優化會使得程序更快但行為不發生改變。在這個童話般的時代，區分優化是否有效有一個簡單的測試方法：如果程序員無法區分一個正確程序經過優化和未經優化的版本之間的（運行結果）差異（除速度更快外）那么優化就是有效的，也就是說，正確的優化不會改變程序的行為。

但是多年前的某一天，硬件工程師們發現讓單個處理器越來越快的魔法消失了，與此同時，他們發現了一種新的魔法，這能使得他們創造出擁有越來越多處理器的計算機。操作系統將這種硬件并行性抽象成線程 Threads 暴露給開發者。這種通過操作系統線程提供多處理器（能力）的魔法對硬件工程師很友好，但它給語言設計師、編譯器作者和程序員帶來了嚴重的問題。

之前許多在單線程程序中不可見（因此有效）的硬件和編譯器優化在多線程程序中變得可見。如果我們說有效的優化不會改變正確程序的行為，那么現在來看只能要么說這些優化是無效的，要么說程序是錯誤的，我們改如何抉擇呢？

下面是一個用類 C 語言編寫的簡單示例程序。在這個程序以及我們將要考慮的所有程序中，所有變量的初始值都被設為零。

// Thread 1        // Thread 2
x = 1;             while (done == 0) { /* loop */ }
done = 1;              print(x);

如果線程 1 和線程 2 都運行在自己的特定的處理器上，并且都運行到結束，那么這個程序可能輸出0 嗎？直接逐行翻譯成運行在 x86 平臺上的匯編后它總是輸出 1，但是直接翻譯成運行在 ARM 或 POWER 多處理器上的匯編后卻可以輸出 0。此外，不管底層硬件是什么，標準的編譯器優化都可以使這個程序輸出 0 或進入無限循環。

這得視情況而定。因為它既取決于硬件，也取決于編譯器。直接逐行轉換到運行在x86多處理器上的匯編總是輸出1。但是直接逐行轉換到在ARM或POWER多處理器上運行的匯編程序可以輸出0。此外，無論底層硬件是什么，標準的編譯器優化都可以使這個程序輸出0或進入無限循環。

“視情況而定” 這似乎不是一個令人愉快的結局，程序員需要一個明確的答案來確定一個程序是否能在新的硬件或新的編譯器下繼續工作，同時硬件設計師和編譯器開發者也需要一個明確的答案來確定在執行一個給定的程序時，硬件和編譯后的代碼可以有多精確。因為這里主要涉及的問題是內存中數據更改的可見性和一致性，所以這個契約被稱為內存一致性模型或簡稱內存模型。

最初，硬件模型的目標是定義對編寫匯編的程序員來說，硬件能提供什么保證，在這種定義中是不包含編譯器的。25 年前，人們嘗試修改內存模型，用來定義對使用像 Java 或 C++ 這種高級語言的程序員來說，（編譯器）能提供什么保證，在內存模型中加入編譯器會使得定義一個合理的模型的工作變得更加復雜。

這是硬件和編譯器內存模型系列的第一篇，我寫這篇文章的目的在于為后面討論我們可能想要在 Go 的內存模型中做出的潛在改變建立背景。但在理解 Go 的發展方向和我們的目標之前，我們必須先了解目前其他硬件內存模型和語言內存模型的發展方向，以及它們實現這一目標的坎坷道路。

這篇文章是關于硬件的。讓我們假設我們正在為多處理器計算機編寫匯編語言。為了寫出正確的程序，你需要從計算機硬件中得到什么保證? 四十多年來，計算機科學家一直在尋找這個問題的答案。

順序一致性模型

Leslie Lamport 在1979年的論文 How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs（如何使多處理器計算機正確執行多進程程序）中引入了順序一致性的概念：

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 individual processor appear in this sequence in the order specified by its program. A multiprocessor satisfying this condition will be called sequentially consistent.

為這類計算機設計和證明多進程算法正確性的通常方法假定滿足以下條件：所有的執行結果都是一致的，就像在處理器上的所有操作都按某種順序執行的一樣，并且每個處理器的操作都是按程序指定的順序出現的。滿足這一條件的多處理器系統將被稱為順序一致的

今天我們不僅僅討論計算機硬件，也將討論滿足順序一致性的編程語言，一個程序唯一可能的執行方式對應于將（多個）線程的操作交錯為順序執行。順序一致性模型通常被認為是最理想的模型，也是程序員使用起來最自然的模型，它允許你可以假定程序是按您頁面上顯示的順序執行的，并且單個線程的執行只是以某種順序進行交錯，但未以其他方式重新排列。

有人可能會質疑順序一致性是不是一個理想的模型，但這超出了本文的討論范圍。我只注意到像 1979 年那樣考慮線程交錯執行的所有可能性，對于 Leslie Lamport 提出的 “the customary approach to designing and proving the correctness of multiprocess algorithms” 四十年時間內還沒人能取代他。

早些時候，我問這個程序能不能輸出 0：

// Thread 1           // Thread 2
x = 1;                while(done == 0) { /* loop */ }
done = 1;             print(x);

為了讓程序更易于分析，讓我們刪除循環和打印，并思考讀取共享變量的可能結果：

Litmus Test: Message Passing
Can this program see r1 = 1, r2 = 0?// Thread 1           // Thread 2
x = 1                 r1 = y
y = 1                 r2 = x

我們假設每個示例開始時，所有變量的初始值都被設為 0，因為我們試圖確定硬件允許做什么，我們假設每個線程都在自己的專用處理器上執行，并且編譯器沒有對線程中運行的指令進行重排：上面清單中的指令就是實際處理器執行的指令。下面的名稱 $r_N$ 表示線程局部寄存器，而不是局部變量，我們會問一個線程的本地寄存器的值在運行結束后是否存在某種可能。

這種關于示例程序的執行結果的問題被稱為 Litmus Test, 因為它只有兩種答案——結果可能或不可能, Litmus Test 給我們提供了一個清晰的方式來區分內存模型：如果一個模型允許特定的執行，另一個模型不允許，這兩個模型顯然是不同的，不幸的是，正如我們稍后將看到的，一個特定模型對一個特定的 Litmus 測試給出的答案往往是令人驚訝的。

如果 Litmus Test 的執行順序是一致的，那么只有六種可能的交錯：

因為線程交叉執行后，不存在 r1 = 1, r2 = 0 的情況，所以說這種結果是不存在的。也就是說，在順序一致的硬件上，不存在這個程序的運行結果是 r1 = 1, r2 = 0 的情況。

理解順序一致性一個很好的思維模型就是想象所有的處理器都連接到同一個共享內存上，而這個共享內存一次只可以為一個線程的讀或寫請求提供服務。我們這里暫不涉及緩存，處理器每次需要從內存讀數據或需要寫數據到內存時，這個請求都會被發送到共享內存中。這種一次性的共享內存使得所有對內存的訪問都有了順序：順序一致性。

(本文中三個內存模型圖摘自 Maranget et al. [“A Tutorial Introduction to the ARM and POWER Relaxed Memory Models.”](https://colobu.com/2021/06/30/hwmm/A Tutorial Introduction to the ARM and POWER Relaxed Memory Models))

上圖展示了一個序列一致的機器的模型，而不是構建它的唯一方法，實際上，可以使用多個共享內存模塊和高速緩存構建一個順序一致的計算機，以幫助預測從內存讀的結果，但保證順序一致就以為著機器的行為必須與上圖模型一致，如果我們只是試圖了解順序一致的執行方式，我們就可以忽略所有具體的復雜實現方式，只考慮這個模型。

不幸的是，對于程序員來說，放棄嚴格的順序一致性可以讓硬件更快地執行程序，因此，所有現代硬件都在以各種方式偏離順序一致性。準確定義具體的硬件偏離是相當困難的。本文以當今廣泛使用的硬件中的兩種內存模型為例: x86、ARM 和 POWER 處理器系列。

x86 Total Store Order (x86-TSO)

現代x86系統的內存模型對應于這個硬件圖：

所有處理器還是連接到一塊共享內存中，但每個處理器在自己的寫隊列上執行寫操作，然后處理器繼續執行其他指令的同時，寫操作進入共享內存，一個處理器上的讀取操作會在讀取共享內存前會優先讀本地的寫隊列，但這個寫隊列對其他處理器是不可見的，其結果就是本處理器會比其他處理器優先看倒自己的寫操作。但是有一點很重要——所有處理器都必須保證寫入（stores）到共享內存時的總順序，這也是這種內存模型 TSO(總存儲有序) 名字的來源。一旦一個值被寫入到共享內存，以后所有處理器都將看到并使用這個值，直到它被本地寫操作覆蓋或被來自其他處理器的緩沖寫操作覆蓋。

本地寫隊列是一個標準的先進先出的隊列：內存寫操作將會根據處理器執行他們的順序作用于共享內存，因為寫操作的順序由寫隊列保存，而且由于其他處理器可以立刻看倒對共享內存的寫操作，所以前面我們考慮的 Litmus 測試的結果中， r1 = 1; r2 = 0 的情況依然不存在。

Litmus Test: Message Passing
Can this program see r1 = 1, r2 = 0?// Thread 1           // Thread 2
x = 1                 r1 = y
y = 1                 r2 = xOn sequentially consistent hardware: no.
On x86 (or other TSO): no.

寫隊列保證線程 1 在 y 之前將 x 寫入內存，并且內存寫入順序的系統級協議（TSO）保證了線程 2 在讀 y 的新值前一定能看到 x 的新值，因此，如果 r2 = x 沒有看倒新的 x 那 r1 = y 就不可能看到新的 y, 在這里，存儲順序是至關重要的：線程 1 在 y 之前寫 x, 所以在寫 x 之前，線程 2 不可能看到新寫的 y 的內容。

在這種情況下，順序一致性和 TSO 模型是一致的，但是他們在其他 litmus 測試的結果上并不一致，例如，這是區分兩種型號的常用示例:

Litmus Test: Write Queue (also called Store Buffer)
Can this program see r1 = 0, r2 = 0?// Thread 1           // Thread 2
x = 1                 y = 1
r1 = y                r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): yes!

任何一個順序一致的系統中，x = 1 或 y = 1 一定會先被執行到，并且這對在其他線程中的讀一定是可見的（and then the read in the other thread must observe it）所以 r1 = 0; r2 = 0 的結果是不存在的，但是在 TSO 系統中，可能發生兩個線程都將寫操作放入隊列，并且在寫操作到達內存之前從內存中讀，因此兩個讀都可能得到 0.

這個示例可能看起來像是人為的，但是在著名的同步算法中，確實有使用兩個同步變量的情況，例如 Dekker’s algorithm 或 Peterson’s algorithm 和一些其他的方案。如果一個線程沒有看到來自另一個線程的所有寫操作，它們就會中斷。

為了修復這些依賴于更強內存順序的算法，非順序一致性的硬件提供了顯式的指令，稱為內存屏障，可以用他們來控制順序，我們可以添加一個內存屏障，保證線程在開始讀之前將之前所有的寫操作刷入到內存中：

// Thread 1           // Thread 2
x = 1                 y = 1
barrier               barrier
r1 = y                r2 = x

隨著屏障的添加， r1 = 0; r2 = 0 的情況將不復存在，Dekker 和 Petersion 的算法也可以正常工作了。內存屏障有很多不同的類型，具體情況因系統而異，這已經超出了本文的范圍，關鍵問題在于，存在這樣一種內存屏障技術，他為程序員或語言實現者提供了一種在關鍵時刻保證強一致性的方法。

最后一個例子，說明這個模式為什么被稱為 TSO：在這種模式下，有本地寫隊列，但在讀的路徑上沒有緩存，一旦一個寫操作到達內存，所有處理器不僅都認同該值（在內存）存在，而且還認同它相對于來自其他處理器寫操作的先后順序。考慮一下 Litmus 測試：

Litmus Test: Independent Reads of Independent Writes (IRIW)
Can this program see r1 = 1, r2 = 0, r3 = 1, r4 = 0?
(Can Threads 3 and 4 see x and y change in different orders?)// Thread 1    // Thread 2    // Thread 3    // Thread 4
x = 1          y = 1          r1 = x         r3 = yr2 = y         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.

如果線程 3 看到 y 先于 x 改變，那線程 4 也可以看到 y 先于 x 改變嗎？在 x86 或其他的 TSO 機器上，答案是不能：對主存的所有寫入操作都有一個統一的順序，所有的處理器都認可這個順序，但前提是每個處理器在它們到達主存之前都知道了他們的寫入。

譯者注：

順序一致性模型可以理解為一種完全互斥模型，共享內存同時只允許一個線程操作，所以一定不會有問題。

TSO 有點像讀寫鎖它能保證寫順序，在此之上的內存屏障可以提供更強的一致性。

x86-TSO 之路

x86-TSO 現在看起來相當清晰明了，但它一路走來卻充滿了坎坷和錯誤的彎路，20 世紀 90 年代，第一代x86多處理器的手冊中幾乎沒有提到硬件提供的內存模型。

作為該問題的一個例子，Plan 9 是第一款真正運行在 x86 上的多處理器操作系統（沒有全局內核鎖）。在 1997 年將它移植到奔騰 Pro 處理器上時，開發人員被歸結為寫隊列 Litmus 測試的行為困擾，在一段微妙的同步代碼中，按假設 r1 = 0; r2 = 0 是不可能存在的，但它卻確實發生了，更糟糕的是，英特爾手冊對內存模型詳細的信息介紹地含糊不清。

有郵件列表建議：it’s better to be conservative with locks than to trust hardware designers to do what we expect（寧可使用更保守地鎖，也不要期望硬件設計師能做我們所期望的事），對此，一名 Plan 9 的開發者很好的解釋到 (explained the problem well)：

I certainly agree. We are going to encounter more relaxed ordering in multiprocessors. The question is, what do the hardware designers consider conservative? Forcing an interlock at both the beginning and end of a locked section seems to be pretty conservative to me, but I clearly am not imaginative enough. The Pro manuals go into excruciating detail in describing the caches and what keeps them coherent but don’t seem to care to say anything detailed about execution or read ordering. The truth is that we have no way of knowing whether we’re conservative enough.

我當然同意，我們會在多處理器中遇到更寬松的順序，但問題在于，在硬件設計師眼中，什么是保守的？強制在需要鎖定的部分（臨界區）的首尾加鎖對我來說應該是相當保守的了，但我顯然沒有足夠的想象力。奔騰 Pro 的手冊在描述緩存以及如何保證他們的一致性時給出了相當詳細的細節，但對執行或讀取順序的細節只字不提，以此導致的就是我們根本無法知道自己做的是否足夠保守。

在討論期間，一名英特爾的架構師也對內存模型做出了非正式的解釋，他指出，即使是在使用 486 多處理器的奔騰系統中也會出現 r1 = 0; r2 = 0 的情況，只是奔騰 Pro 更大的流水線和寫隊列讓這種問題更容易暴露。

這名英特爾架構師還寫到：

Loosely speaking, this means the ordering of events originating from any one processor in the system, as observed by other processors, is always the same. However, different observers are allowed to disagree on the interleaving of events from two or more processors.

Future Intel processors will implement the same memory ordering model.

粗略來說，（內存模型）這意味著從系統中任何一個處理器產生的事件的順序，對在其他處理器上的觀察者來說，始終是相同的。但是，允許觀察者對來自兩個或多個處理器的事件持不同意見。（注：保證單個處理器上的事件順序，允許不同處理器的事件亂序執行）

未來英特爾也將實現相同的內存模型。

對于 “different observers are allowed to disagree on the interleaving of events from two or more processors” 的說法，意味著 IRIW 的 Litmus 測試的結果在 x86 上是肯定的，盡管在前一節中我們看到 x86 的答案是否定的，這怎么可能呢？

答案似乎是英特爾處理器從未對這個 Litmus 測試做出 yes 的回答，而當時這位英特爾的架構師也不愿意尾未來的處理器做出任何保證。且體系結構手冊中僅有的少量文本幾乎沒有做出任何保證，這使得對它們編程非常困難。

Plan 9 的討論并不是孤立的事件，Linux 內核開發人員在 1999 年 11 月下旬開始有一百多封郵件討論類似英特爾內存保證的問題。

在接下來的十年里，越來越多的人遇到了這些困難，英特爾的一組架構師承擔了為當前和未來處理器編寫有用的處理器行為保證的任務。其第一個成果是 2007 年 8 月發布的《英特爾 64 架構內存順序白皮書（Intel 64 Architecture Memory Ordering White Paper）》,其目的在于幫助軟件開發者清楚地理解不同順序的內存訪問指令可能產生的結果，同年晚些時候 AMD 在 [AMD64 架構程序員參考手冊 3.14 版本（AMD64 Architecture Programmer’s Manual revision 3.14）](https://courses.cs.washington.edu/courses/cse351/12wi/supp-docs/AMD Vol 1.pdf)中發布了類似的描述。這些描述基于一個名為 “總鎖順序 + 因果一致性（TLO + CC）” 的模型，故順序性比 TSO 要弱，在公開的談話中，英特爾的架構師講到 TLO + CC 如同要求的那樣強大，但還不是足夠將大的(as strong as required but no stronger.) 特別的是，該模型保留了 x86 處理器對 IRIW 的 Litmus 測試做出肯定回答的權力。不幸的是，內存屏障的定義還沒強大到重新建立順序一致性的內存語義，即便在每條指令之后都加一個屏障。更糟糕的是，研究人員發現英特爾 x86 的硬件實際上違反了 TLO + CC 模型，例如：

Litmus Test: n6 (Paul Loewenstein)
Can this program end with r1 = 1, r2 = 0, x = 1?// Thread 1    // Thread 2
x = 1          y = 1
r1 = x         x = 2
r2 = y
On sequentially consistent hardware: no.
On x86 TLO+CC model (2007): no.
On actual x86 hardware: yes!
On x86 TSO model: yes! (Example from x86-TSO paper.)

2008 年晚些的時候，英特爾和 AMD 修訂了規范，保證了對 IRIW case 的否決，并增強了內存屏障，但仍然允許一些似乎在任何合理的硬件上都不應該出現的意外行為，例如：

Litmus Test: n5
Can this program end with r1 = 2, r2 = 1?// Thread 1    // Thread 2
x = 1          x = 2
r1 = x         r2 = x
On sequentially consistent hardware: no.
On x86 specification (2008): yes!
On actual x86 hardware: no.
On x86 TSO model: no. (Example from x86-TSO paper.)

為了解決這些問題，歐文斯等人提出了 x86-TSO 模型 ,它基于早期的 SPARCv8 TSO 模型，當時它們聲稱：“據我們所知，x86-TSO 是可靠的，足夠強大的，可以進行以上編程，并且大體上符合供應商的意圖”，幾個月后，英特爾和 AMD發布了廣泛使用這種模式的新手冊。

看起來英特爾處理器從一開始就實現了 x86-TSO, 實際上英特爾花了十年時間才決定致力于此，回顧過去，顯然英特爾和 AMD 的架構師曾為如何編寫一個內存模型而苦苦掙扎，這個模型既要為未來的處理器優化留下空間，還要為編譯器作者和匯編語言程序員提供有用的保證。“As strong as required but no stronger” 是一種艱難的平衡行為。

ARM/POWER 寬松的內存模型（Relaxed Memory Model）

現在讓我們看看一個更寬松的內存模型，ARM 和 POWER 處理器上的內存模型，在實現層面，這兩個系統有諸多不同，但保證內存一致性的模型被證明是大致相似的，而且相比 x86-TSO 甚至是 x86-TLO-CC 要弱一些。

ARM 和POWER 系統的模型概念是：每個處理器對自己的完整內存副本進行讀寫操作，每個讀寫操作都獨立地傳播到其他處理器，并允許在寫操作傳播時重新排序。

這里沒有總存儲順序，雖然沒有描述，但每個處理器都允許延遲讀，直到讀到它需要地結果：讀可以延遲到之后地寫之后。在這個寬松地模型中，目前為止我們所看到的所有 Litmus 測試地結果都是肯定地，這確實有可能發生。

對于通過 Litmus 測試的原始消息，單個處理器的寫入重新排序意味著其他線程以相同的順序無法觀察到線程 1 的寫入：

Litmus Test: Message Passing
Can this program see r1 = 1, r2 = 0?// Thread 1           // Thread 2
x = 1                 r1 = y
y = 1                 r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: yes!

在 ARM/POWER 模型中，我們可以認為線程 1 和線程 2 都有各自單獨的內存副本，寫操作以任何可能的順序在內存之間傳播。如果線程 1 在發送 x 的更新之前將 y 的更新發送給線程 2 并且線程 2 在這兩個更新之間執行，它確實會看到 r1 = 1, r2 = 0 的結果。

該結果表明，ARM/POWER 模型比 TSO 更弱，對硬件的要求更低。ARM/POWER 模型仍承認 TSO所做的各種重排序:

Litmus Test: Store Buffering
Can this program see r1 = 0, r2 = 0?// Thread 1           // Thread 2
x = 1                 y = 1
r1 = y                r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): yes!
On ARM/POWER: yes!

在 ARM/POWER 上，對 X 和 Y 的寫入可能會在本地存儲器進行，但如果在相反的線程上讀取時，可能寫操作還沒有傳播開。

下面是一個 Litmus test，它展示了 x86 擁有的總存儲順序意味著什么:

Litmus Test: Independent Reads of Independent Writes (IRIW)
Can this program see r1 = 1, r2 = 0, r3 = 1, r4 = 0?
(Can Threads 3 and 4 see x and y change in different orders?)// Thread 1    // Thread 2    // Thread 3    // Thread 4
x = 1          y = 1          r1 = x         r3 = yr2 = y         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: yes!

在 ARM/POWER 中，不同的線程可能以不同的順序觀察到不同的寫操作，它們不能保證到達主存時總寫入順序是一致的，所以線程 3 可以看到 x 在 y 之前發生變化，而線程 4 也可能看到 y 在 x 之前發生變化。

作為另一個例子，ARM/POWER 系統具有內存讀取的可見緩沖或重新排序，如下面 Litmus 測試所見：

Litmus Test: Load Buffering
Can this program see r1 = 1, r2 = 1?
(Can each thread's read happen after the other thread's write?)// Thread 1    // Thread 2
r1 = x         r2 = y
y = 1          x = 1
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: yes!

在任何順序一致性的機器上交錯執行必然是從線程 1 的 r1 = x 或線程 2 的 r2 = y 開始的，讀到的一定是 0，因此不可能得到 r1 = 1, r2 = 1 的結果，然而在 ARM/POWER 模型中，處理器被允許延遲讀操作，直到指令流后面的寫操作完成，這樣在兩次讀之前 y = 1 和 x = 1 其實已經被執行了。

盡管 ARM 和 POWER 的內存模型都允許這個結果，但 Maranget 等人在 2012 年的這篇報告中還是講到只能在 ARM 上得到復現，POWER 上從來沒有出現過。在這里，模型和現實之間的分歧開始發揮作用，正如我們在英特爾 x86 中所做的那樣：硬件實現了比技術上的保證更強的模型，我們鼓勵（程序）依賴于更強的行為，這代表著將來，較弱的硬件將會會破壞程序行為，不管其是否有效。

如同 TSO 系統， ARM 和 POWER 也有一些屏障，我們可以在上面的例子中插入這些屏障來保證強順序一致的行為。但一個顯而易見的問題是一個沒有使用屏障的 ARM/POWER 是否排除了任何行為？難道所有 Litmus 測試的結果都是 “不，這不可能發生？”。當我們關注于單一的內存位置時，它可以！

譯者注：

這里說的其實是如果 ARM/POWER 不使用屏障技術，那它的順序是否是完全不可控的，體現在 Litmus 測試上就是難道所有的情況都可能發生？

這里有一個 Litmus 測試，它可以測試即視在 ARM/POWER 上也不會發生的事情：

Litmus Test: Coherence
Can this program see r1 = 1, r2 = 2, r3 = 2, r4 = 1?
(Can Thread 3 see x = 1 before x = 2 while Thread 4 sees the reverse?)// Thread 1    // Thread 2    // Thread 3    // Thread 4
x = 1          x = 2          r1 = x         r3 = xr2 = x         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: no.

這個 Litmus 測試與前一個類似，只不過現在兩個線程 1 2 都在寫同一個變量 x 而不是不同的變量 x 和 y 。線程 1 和線程 2 向 x 寫入了沖突的值 1 和 2 ，而線程 3 和線程 4 都讀取了 x 兩次。如果線程 3 看到 x = 1 被 x = 2 覆蓋，那么線程 4 是否可以看到相反的結果呢？

答案是 no 即使在 ARM/POWER 上，系統中的線程必須就寫入單個內存位置的總順序達成一致。也就是說，線程必須同意哪個寫會覆蓋其他寫。這種性值叫做 相干性 coherence, 沒有相干性，處理器要么不同意內存的最終結果，要么報告內存位置從一個值切換到另一個值，然后返回到第一個值。編寫這樣一個系統的程序是非常困難的。

譯者注：

相關性是說不管多個值讀寫的順序能不能保證有序，如果多個線程并發修改同一內存位置的值，修改的結果落實到主從上時，對所有觀察者來說，一定是有唯一順序的，不可能存在觀察者 A 觀察到 x 先被線程 1 修改，觀察者 B 觀察到 x 先被線程 2 修改的情況。

我故意忽略了ARM 和 POWER 弱內存模型中的許多細微之處。更詳細的內容可以參考 Peter Sewell 關于該主題的論文, 此外，ARMv8 通過使多副本原子化來增強內存模型，但我在這里不打算詳細解釋這意味著什么。

有兩點值得注意, 首先，這里的微妙之處令人難以置信，這是一個由非常執著、非常聰明的人進行了超過十年的學術研究的課題。我并沒有說我自己能完全理解。這不是我們應該希望向普通程序員解釋的東西，也不是我們在調試普通程序時希望保持清晰的東西。其次，允許的情況和觀察到的情況之間的差距造成了不幸的未來的 “驚喜”。如果當前的硬件沒有顯示所有允許的行為，特別是當很難解釋什么是允許的時候, 然后不可避免地，程序會意外地依賴于實際硬件的更受限制的行為。如果一個新芯片的該行為不受限制，那么硬件內存模型在技術上允許這種新行為破壞你的程序，也就是說，從技術上來說，這個 bug 是你的錯，這一點也不能安慰你。這不是寫程序的方法。

譯者注：

第二點是說你不要去過度依賴這種由具體硬件所保障的行為，否則如果換一個芯片你不就麻了嗎！

弱排序與無數據競爭序列一致性 Weak Ordering and Data-Race-Free Sequential Consistency

到目前為止，我希望您明確硬件的細節是復雜的且微妙的，但卻并不是你每次編寫代碼時都需要考慮的東西，相反，你只需要明確：“如果遵循這些簡單的規則，您的程序將會向順序執行的那樣產生確定的結果”（我們任然在討論硬件，所以我們討論的依然是交錯執行的獨立的匯編指令）

Sarita Adve 和 Mark Hill 在 1990 年的論文 “Weak Ordering – A New Definition(《弱排序——一種新的定義》)” 提出了這個方法，他們對 “弱排序 Weak Ordering” 的定義如下：

Let a synchronization model be a set of constraints on memory accesses that specify how and when synchronization needs to be done.

假設同步模型是對內存訪問的一組約束，這些約束指定了如何，以及何時完成同步。

Hardware is weakly ordered with respect to a synchronization model if and only if it appears sequentially consistent to all software that obey the synchronization model.

當且僅當硬件看起來與所有遵循同步模型的軟件順序一致時，硬件相對于該同步模型是弱排序的。

雖然他們的論文聚焦于當時的額硬件（并不是 x86 ARM 或 POWER）但是這種將討論提升到具體設計之上的想法使得這篇論文與今天的話題相關。

我之前說過，有效的優化不會改變有效程序的行為，這些規則首先定義了有哪些有效的手段，然后所有硬件的優化都必須使得（遵循這些規則）這些程序像是在順序一致的機器上執行的那樣。當然，更有趣的細節是這些規則本身，即定義程序有效含義的約束條件。

譯者注：

硬件的細節是復雜且微妙的，但這并不是我們每次寫程序都需要考慮的問題，我們應該關注的是這樣一組規則，它定義了什么樣的程序是有效的，硬件的優化應該保證遵循這組規則的程序的行為。

Adve 和 Hill 提出了一個同步模型，他們將其稱之為無數據競爭（data-race-free DRF）,該模型假設硬件的內存同步操作是與普通的內存讀寫操作分開的。普通內存讀寫可以在同步操作之間重新排序，但（普通讀寫）不會跨越它們（硬件內存同步）也就是說，同步操作成為了成為了重排序的 “屏障”。對于所有理想化的順序一致的執行，如果來自不同線程的兩個對普通內存的訪問操作要么都是讀，要么被同步操作分割開，這些同步操作強制一個發生在另一個之前，那么這個程序就是五數據競爭的（DRF）。

讓我們看一些來自 Adve 和 Hill 論文中的例子（經過重新繪制），下面是一個線程，它執行對變量x的寫操作，然后再執行對同一個變量的讀操作：

垂直的箭頭標記了單個線程中的執行順序:先寫，再讀。在這個程序中沒有競爭，因為所有的東西都在一個線程中。

相比之下，在這個雙線程程序中就存在一個競爭：

在這里，線程 2 在不與線程 1 協調的情況下寫入 x。線程 2 的寫與線程 1 的讀寫產生競爭。如果線程 2 正在讀 x 而不是寫 x，那么程序將只有一次競爭，即線程 1 的寫操作和線程 2 的讀操作之間的競爭。每個競爭至少包含一個寫操作: 兩個不協調的讀不會相互競爭。

為了避免競爭，我們必須添加同步操作，他將強制在不同線程共享同步變量的操作上添加順序，如果同步操作 S(a) (在變量a上同步，用虛線箭頭標記) 強制線程 2 在線程 1 結束之后再寫入，則消除了競爭：

現在線程 2 的寫操作不能與線程 1 的操作同時發生。

如果線程 2 只是在讀，那么我們只需要同步線程 1 的寫操作。兩個讀取仍然可以同時進行：

線程可以按同步序列排序，甚至可以使用中間線程。這個程序沒有競爭

另一方面，使用同步變量本身并不能消除競爭: 甚至可能會錯誤地使用它們。這個程序存在競爭：

線程 2 的讀操作與其他線程的寫操作是同步的，它肯定發生另外兩個線程的寫之后，但另外兩個線程本身并沒有同步。這個程序便不是無數據競爭的。

Adve 和 Hill 將弱排序描述為 “ 軟件和硬件之間的規約 ”，具體地說，如果軟件避免了數據競爭，那么硬件的行為就應該好像它是順序一致的，這比我們在前面幾節中研究的模型更容易推理。但是，硬件如何才能履行規約呢？

Adve 和 Hill 給出了硬件 “遵循 DRF 弱排序” 的證明，這意味著它只要滿足一組特定的最低要求，那么它無數據競爭的程序在其上執行時就像在順序一致的機器上執行時一樣。我不準備探討更多細節，但重點是，在 Adve 和 Hill 的論文發表之后，硬件工程師有了一份由理論支持的菜譜：做了這些事情，您就可以斷言您的硬件將與無數據競爭程序的順序一致。事實上，假設同步操作的適當實現，大多數寬松的硬件確實是這樣做的，并且還在繼續這樣做。Adve 和 Hill 最初關注的是 VAX，但 x86、ARM 和 POWER 肯定也能滿足這些限制。這系統向無數據競爭程序保證順序一致性的想法通常縮寫為 DRF-SC。

DRF-SC 標志著硬件內存模型的一個轉折點，為硬件設計人員和軟件作者(至少是那些用匯編語言編寫軟件的人)提供了一個清晰的策略。但正如我們將在下一篇文章中看到的那樣，高級編程語言的內存模型問題沒有那么清晰明了的答案。

本系列中的下一個帖子是關于編程語言內存模型。