Go 硬件內存模型

簡介: 童話之終局

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

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

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

這裏有一個類似 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 = yr2 = 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 = 1y = 1必須首先發生,然後另一個線程中的讀取必須能夠觀察到它 (此賦值事件),因此r1 = 0r2 = 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 標誌着硬件內存模型的一個轉折點,爲硬件設計者和軟件作者提供了一個清晰的策略,至少是那些用匯編語言編寫軟件的人。正如我們將在下一篇文章中看到的,高級編程語言的內存模型問題沒有一個整潔的答案。

致謝

這一系列的帖子從我有幸在谷歌共事的一長串工程師的討論和反饋中受益匪淺。我感謝他們。我對任何錯誤或不受歡迎的意見承擔全部責任。

本文由 Readfog 進行 AMP 轉碼,版權歸原作者所有。
來源https://mp.weixin.qq.com/s/t0mWCya8DH0hXl21viAIRA