簡介: 童話之終局

很久以前，當每個人都寫單線程程序的時候，讓程序運行得更快最有效的方法之一是坐下來袖手旁觀。下一代硬件和編譯器的優化結果可以讓程序像以前一樣運行，只是速度會更快。在這個童話般的年代，有一個判斷優化是否有效的簡單測試方法:如果程序員不能區分合法程序的未優化執行結果和優化執行的結果之間的區別(除了速度的區別)，那么這個優化就是有效的。也就是說，有效的優化不會改變有效程序的行為。

幾年前， 某個悲傷的日子，硬件工程師發現讓單個處理器越來越快的魔法失效了。不過，他們發現了一個新的魔法，可以讓他們創造出擁有越來越多處理器的計算機，操作系統使用線程抽象模型向程序員展示了這種硬件并行能力。這種新的魔法——多處理器以操作系統線程的形式提供并行能力——對硬件工程師來說效果更好，但它給編程語言設計者、編譯器作者和程序員帶來了嚴重的問題。

許多在單線程程序中不可見(因此有效)的硬件和編譯器優化會在多線程程序中產生明顯的結果變化。如果有效的優化沒有改變有效程序的行為，那么這些優化應該被認為是無效的。或者現有程序必須被聲明為無效的。到底是哪一個，怎么判斷？

這里有一個類似C語言的簡單示例程序。在這個程序和我們將要考慮的所有程序中，所有變量最初都設置為零。

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

如果線程1和線程2都運行在自己專用處理器上，都運行到完成，這個程序能打印 0 嗎？

看情況(It depends)。這取決于硬件，也取決于編譯器。在x86多處理器上, 如果逐行翻譯成匯編的程序執行的話總是會打印1。但是在ARM或POWER多處理器上，如果逐行翻譯成匯編的程序可以打印0。此外，無論底層硬件是什么，標準編譯器優化都可能使該程序打印0或進入無限循環。

“看情況”(It depends)并不是一個圓滿的結局。程序員需要一個明確的答案來判斷一個程序是否在新的硬件和新的編譯器上能夠正確運行。硬件設計人員和編譯器開發人員也需要一個明確的答案，說明在執行給定的程序時，硬件和編譯后的代碼可以有多精確。因為這里的主要問題是對存儲在內存中數據更改的可見性和一致性，所以這個契約被稱為內存一致性模型（memory consistency model）或僅僅是內存模型(memory model)。

最初，內存模型的目標是定義程序員編寫匯編代碼時硬件提供的保證。在該定義下，是不包含編譯器的內容的。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.

為這種計算機設計和證明多處理算法正確性的通常方法假定滿足下列條件:任何執行的結果都是相同的，就好像所有處理器的操作都是按某種順序執行的，每個處理器的操作都是按程序指定的順序出現的。滿足這一條件的多處理器系統將被稱為順序一致的。

今天，我們不僅討論計算機硬件，還討論保證順序一致性的編程語言，當程序的唯一可能執行對應于某種線程操作交替成順序執行時。順序一致性通常被認為是理想的模型，是程序員最自然的工作模式。它允許您假設程序按照它們在頁面上出現的順序執行，并且單個線程的執行只是以某種順序交替(interleaving)，而不是以其他方式排列。

人們可能會有理由質疑順序一致性是否應該是理想的模型，但這超出了本文的范圍。我只注意到，考慮到所有可能的線程交替(interleaving)依然存在，就像在1979年一樣，即使過了四十幾年，Leslie Lamport的“設計和證明多處理算法正確性的慣用方法”，依然沒有什么能取代它。

之前我問這個程序能不能打印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

我們假設每個例子都是所有共享變量最初都被設置為零。因為我們試圖確定硬件允許做什么，我們假設每個線程都在自己的專用處理器上執行，并且沒有編譯器來對線程中發生的事情進行重新排序:列表中的指令就是處理器執行的指令。rN這個名字表示一個線程本地寄存器，而不是一個共享變量，我們會問一個線程本地寄存器的值在執行結束時是否存在某種可能。

這種關于樣本程序執行結果的問題被稱為litmus test。因為它只有兩個答案——這個結果可能還是不可能？——litmus test為我們提供了一種區分內存模型的清晰方法:如果一個模型支持特定的執行，而另一個不支持，那么這兩個模型顯然是不同的。不幸的是，正如我們將在后面看到的，一個特定的模型對一個特定的litmus test給出的答案往往令人驚訝。

If the execution of this litmus test is sequentially consistent, there are only six possible interleavings:

如果該litmus test的執行順序一致，則只有六種可能的交替:

因為沒有交替執行的結果會產生r1 = 1, r2 = 0,所以這個結果是不允許的。也就是說，在順序執行的硬件上，litmus test執行結果出現r1 = 1, r2 = 0是不可能的。

順序一致性的一個很好的思維模型是想象所有處理器直接連接到同一個共享內存，它可以一次處理一個線程的讀或寫請求。 不涉及緩存，因此每次處理器需要讀取或寫入內存時，該請求都會轉到共享內存。 一次使用一次的共享內存對所有內存訪問的執行施加了順序順序：順序一致性。

(本文中三個內存模型圖摘自 Maranget et al. “A Tutorial Introduction to the ARM and POWER Relaxed Memory Models.”)

上圖是順序一致機器的模型，而不是構建機器的唯一方法。 實際上，可以使用多個共享內存模塊和緩存來構建順序一致的機器來幫助預測內存獲取的結果，但順序一致意味著機器的行為必須與該模型并無二致。 如果我們只是想了解順序一致執行意味著什么，我們可以忽略所有這些可能的實現復雜性并只考慮這個模型。

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

x86 Total Store Order (x86-TSO)

現代x86系統的內存模型對應于以下硬件圖:

所有處理器仍然連接到一個共享內存，但是每個處理器都將對該內存的寫入(write)放入到本地寫入隊列中。處理器繼續執行新指令，同時寫操作(write)會更新到這個共享內存。一個處理器上的內存讀取在查詢主內存之前會查詢本地寫隊列，但它看不到其他處理器上的寫隊列。其效果就是當前處理器比其他處理器會先看到自己的寫操作。但是——這一點非常重要——所有處理器都保證寫入(存儲store)到共享內存的(總)順序，所以給這個模型起了個名字:總存儲有序，或TSO。當一個寫操作到達共享內存時，任何處理器上的任何未來讀操作都將看到它并使用該值(直到它被以后的寫操作覆蓋，或者可能被另一個處理器的緩沖寫操作覆蓋)。

寫隊列是一個標準的先進先出隊列:內存寫操作以與處理器執行相同的順序應用于共享內存。因為寫入順序由寫入隊列保留，并且由于其他處理器會立即看到對共享內存的寫入，所以我們之前考慮的通過litmus test的消息與之前具有相同的結果: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 = x
On sequentially consistent hardware: no. 
On x86 (or other TSO): no.

寫隊列保證線程1在y之前將x寫入內存，關于內存寫入順序(總存儲有序)的系統級協議保證線程2在讀y的新值之前讀x的新值。因此，r1 = y在r2 = x看不到新的x之前不可能看到新的y。存儲順序至關重要:線程1在寫入y之前先寫入x，因此線程2在看到x的寫入之前不可能看到y的寫入。

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

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必須首先發生，然后另一個線程中的讀取必須能夠觀察到它(此賦值事件)，因此r1 = 0，r2 = 0是不可能的。但是在一個TSO系統中，線程1和線程2可能會將它們的寫操作排隊，然后在任何一個寫操作進入內存之前從內存中讀取，這樣兩個讀操作都會看到零。

這個例子看起來可能是人為制造的，但是使用兩個同步變量確實發生在眾所周知的同步算法中，例如德克爾算法或彼得森算法，以及特定的方案。如果一個線程沒有看到另一個線程的所有寫操作，線程就可能會中斷。

為了修復同步算法，我們需要依賴于更強的內存排序，非順序一致的硬件提供了稱為內存屏障(或柵欄)的顯式指令，可用于控制排序。我們可以添加一個內存屏障，以確保每個線程在開始讀取之前都會刷新其先前對內存的寫入:

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

加上正確的障礙，r1 = 0，r2 = 0也是不可能的，德克爾或彼得森的算法就可以正常工作了。內存屏障有很多種；具體細節因系統而異，不在本文討論范圍之內。關鍵是內存屏障的存在給了程序員或語言實現者一種在程序的關鍵時刻強制順序一致行為的方法。

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

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 = y
                              r2 = y         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.

如果線程3看到x先于y變化，那么線程4能看到y先于x變化嗎？對于x86和其他TSO機器，答案是否定的:對主內存的所有存儲(寫入)都有一個總順序，所有處理器都認同這個順序，只是每個處理器在到達主內存之前都先知道自己的寫入而已。

x86-TSO 之路

x86-TSO模型看起來相當整潔，但是這條道路充滿了路障和錯誤的彎道。在20世紀90年代，第一批x86多處理器可用的手冊幾乎沒有提到硬件提供的內存模型。

作為問題困擾的一個例子，Plan 9 是第一個在x86上運行的真正多處理器操作系統(沒有全局內核鎖)。1997年，在移植到多處理器 奔騰Pro的過程中，開發人員被寫隊列litmus test的不期望的行為所困擾。一小段同步代碼假設r1 = 0，r2 = 0是不可能的，但它確實發生了。更糟糕的是，英特爾手冊對內存模型的細節模糊不清。

針對郵件列表中提出的“使用鎖最好保守一點，不要相信硬件設計師會做我們期望的事情”的建議，Plan 9的一名開發人員很好地解釋了這個問題:

我當然同意。我們會在多處理器中遇到更寬松的順序(relaxed ordering )。問題是，硬件設計者認為什么是保守的？在臨界區的開頭和結尾強制互鎖對我來說似乎相當保守，但我顯然不夠富有想象力。奔騰Pro的手冊在描述緩存和怎么使它們保持一致時非常詳細，但似乎不在乎說任何關于執行或read順序的細節。事實是，我們無法知道自己是否足夠保守。

在討論過程中，英特爾的一名架構師對內存模型做了非正式的解釋，指出理論上，即使是多處理器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.

粗略地說，這意味著從系統中任何一個處理器產生的事件的順序，正如其他處理器所觀察到的，總是相同的。然而，允許不同的觀察者對來自兩個或更多處理器的事件的交替有不同的觀察結果。
未來的英特爾處理器將采用相同的內存順序模式。

聲稱“允許不同的觀察者對來自兩個或更多處理器的事件的交替有不同的觀察結果”是在說，IRIW litmus test的答案在x86上可以回答“是”，盡管在前面的部分我們看到x86回答“否”。這怎么可能呢？

答案似乎是，英特爾處理器實際上從未對這一litmus test做出“是”的回答，但當時英特爾架構人員不愿意為未來的處理器做出任何保證。體系結構手冊中存在的少量文本幾乎沒有任何保證，使得很難針對它們進行編程。

Plan 9的討論不是一個孤立的事件。從11月下旬開始，Linux內核開發人員在他們的郵件列表上討論了100多條消息。

在接下來的十年里，越來越多的人遇到了這些困難，為此，英特爾的一組架構師承擔了為當前和未來的處理器寫下有用的處理器行為保證的任務。第一個結果是2007年8月出版的Intel 64 Architecture Memory Ordering White Paper，旨在為“軟件作者提供對不同順序的內存訪問指令可能產生的結果的清晰理解”。同年晚些時候，AMD在AMD64 Architecture Programmer's Manual revision 3.14中發布了類似的描述。這些描述基于一個被稱為“總鎖序+因果一致性”(TLO+CC)的模型，故意弱于TSO。在公開訪談中，英特爾架構師表示，TLO+CC“像要求的那樣強大，但并不足夠強大。”特別是，該模型保留了x86處理器在IRIW litmus test中回答“是”的權利。不幸的是，內存屏障的定義不夠強大，不足以重建順序一致的內存語義，即使每個指令之后都有一個屏障。更糟糕的是，研究人員觀察到實際的英特爾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.)

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

似乎所有英特爾處理器從一開始就實現了x86-TSO，盡管英特爾花了十年時間才決定致力于此。回想起來，很明顯，英特爾和AMD的設計師們正在努力解決如何編寫一個能夠為未來處理器優化留出空間的內存模型，同時仍然為編譯器作者和匯編語言程序設計者提供有用的保證。“有多強就有多強，但沒有多強”是一個艱難的平衡動作。

ARM/POWER Relaxed Memory Model

現在讓我們來看看一個更寬松的內存模型，在ARM和POWER處理器上找到的那個。在實現層面上，這兩個系統在許多方面有所不同，但保證內存一致性的模型大致相似，比x86-TSO甚至x86-TLO+CC稍弱。

ARM和POWER系統的概念模型是，每個處理器從其自己的完整內存副本中讀取和向其寫入，每個寫入獨立地傳播到其他處理器，隨著寫入的傳播，允許重新排序。

這里沒有總存儲順序。雖然沒有描述，但是每個處理器都被允許推遲讀取(read)，直到它等到它需要結果:讀取(read)可以被延遲到稍后的寫入(write)之后。在這個寬松的(relaxed)模型中，我們迄今為止所看到的每一個litmus test的答案都是“yes，這真的可能發生。”

對于通過litmus test的原始消息，單個處理器對寫入的重新排序意味著線程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的更新(update)之前向線程2發送y的更新，并且如果線程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的寫入(write)可能會寫入本地存儲器，但當讀取發生在相反的線程上時，寫入可能尚未傳播開來。

下面是一個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 = y
                              r2 = y         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: yes!

在ARM/POWER上，不同的線程可能以不同的順序觀察到不同的寫操作。它們不能保證對到達主內存的總寫入順序達成一致的觀察效果，因此線程3可以在y變化之前之前看到x的變化，而線程4可以在x變化之前看到y的變化。

作為另一個例子，ARM/POWER系統具有內存讀取(負載 load)的可見緩沖或重新排序，如下面litmus test所示:

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 test的答案是否都是“no，那不可能發生？” 當我們專注于一個單一的內存位置時，它可以。

這里有一個litmus test，它可以測試即使在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 = x
                              r2 = x         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: no.

這個litmus test與前一個測試類似，但是現在兩個線程都在寫入單個變量x，而不是兩個不同的變量x和y。線程1和2將沖突的值1和2都寫入x，而線程3和線程4都讀取x兩次。如果線程3看到x = 1被x = 2覆蓋，那么線程4能看到相反的情況嗎？

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

我故意忽略了ARM和POWER弱內存模型中的許多微妙之處。更多詳細信息，請參閱彼得·蘇厄爾關于該主題的論文。有兩個要點要記住。首先，這里有令人難以置信的微妙之處，這是由有非常持久力、非常聰明的人進行了十多年學術研究的主題。我自己并不聲稱完全理解。這不是我們應該希望向普通程序設計人員解釋的事情，也不是我們在調試普通程序時希望能夠堅持的事情。第二，允許和觀察到的結果之間的差距造成了不幸的未來驚喜。如果當前的硬件沒有展現出所有允許的行為——尤其是當首先很難推理出什么是允許的時候！—那么不可避免地會編寫一些程序，這些程序會偶然地依賴于實際硬件的更受限制的行為。如果一個新的芯片在行為上受到的限制更少，那么硬件內存模型在技術上允許破壞程序的新行為——也就是說，這個錯誤在技術上是你的錯——這一事實并不能給你帶來什么安慰。這不是寫程序的方法。

弱排序和無數據競爭的順序一致性

到目前為止，我希望您確信硬件細節是復雜而微妙的，而不是您每次編寫程序時都想解決的問題。 相反，它有助于識別“如果你遵循這些簡單的規則，你的程序只會產生結果，就像通過一些順序一致的執行的那樣。” （我們仍在談論硬件，所以我們仍在談論交替獨立的匯編指令。）

Sarita Adve and Mark Hill proposed exactly this approach in their 1990 paper “Weak Ordering – A New Definition”. They defined “weakly ordered” as follows.

Sarita Adve和Mark Hill在他們1990年的論文“Weak Ordering – A New Definition”中正是提出了這種方法。他們把“弱有序”定義為如下。

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

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

硬件相對于同步模型是弱有序的，當且僅當它在順序上與遵守同步模型的所有軟件一致時。

雖然他們的論文是關于捕捉當時的硬件設計(不是x86、ARM和POWER)，但將討論提升到特定設計之上的想法使論文與今天的討論依然相關。

我之前說過“有效的優化不會改變有效程序的行為。”這些規則定義了什么是有效的手段，然后任何硬件優化都必須讓這些程序像在順序一致的機器上一樣工作。當然，有趣的細節是規則本身，定義程序有效的約束。

Adve和Hill提出了一種同步模型，他們稱之為無數據競爭(data-race-free，DRF)。該模型假設硬件具有獨立于普通內存讀寫的內存同步操作。普通的內存讀寫可以在同步操作之間重新排序，但不能在跨它們移動。(也就是說，同步操作也可用來做重新排序的內存屏障。)如果對于所有理想化的順序一致的執行，從不同線程對同一位置的任何兩個普通存儲器訪問要么都是讀取，要么通過同步操作強制一個在另一個之前發生而分開執行，則程序被稱為無數據競爭的。
我們來看一些例子，摘自Adve和Hill的論文(為了演示而重新繪制)。這里有一個線程執行變量x的寫操作，然后讀取同一個變量。

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

相比之下，在這個雙線程程序中有一個競爭:

這里線程2在不與線程1協調的情況下寫入x。線程2的寫入與線程1的寫入和讀取競爭。如果線程2讀x而不是寫x，程序在線程1寫和線程2讀之間只有一個競爭。每個競爭至少涉及一次寫入:兩次不協調的讀取不會相互競爭。

為了避免競爭，我們必須添加同步操作，這將在共享一個同步變量的不同線程上的操作之間強制一個特定的順序。如果同步S(a)(在變量a上同步，用虛線箭頭標記)迫使線程2的寫操作在線程1完成后發生，則競爭被消除-

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

如果線程2只是讀取，我們只需要與線程1的寫入同步。兩次讀取仍然可以同時進行:

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

另一方面，同步變量的使用本身并不能消除競爭:錯誤地使用它們是可能的。下面這個程序有一個競爭:

線程2的讀取與其他線程中的寫入完全同步——這肯定發生在兩者之后——但是這兩個寫入本身并不同步。這個程序并不是data-race-free。

Adve和Hill將弱排序描述為“軟件和硬件之間的契約”，具體來說，如果軟件避免了數據競爭，那么硬件就好像是順序一致的，這比我們在前面部分研究的模型更容易推理。但是硬件如何滿足它的契約呢？

Adve和Hill給出了硬件“遵循DRF弱排序”的證明，這意味著它執行無數據競爭的程序，就好像是按照順序一致的順序一樣，只要它滿足一組特定的最低要求。我不打算詳談細節，但重點是在Adve和Hill的論文發表后，硬件設計師們有了一份由理論支持的手冊:做這些事情，你就可以斷言你的硬件將與data-race-free程序順序一致。事實上，假設同步操作的適當實現，大多數寬松的硬件確實是這樣做的，并且一直在繼續這樣做。Adve和Hill最初關注的是VAX，但x86、ARM和POWER肯定也能滿足這些限制。這種系統保證無數據競爭程序的順序一致性的觀點通常被縮寫為DRF-SC。

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

本文轉自：https://colobu.com/2021/06/30/hwmm/