簡介: 童話之終局
很久以前,當(dāng)每個人都寫單線程程序的時候,讓程序運行得更快最有效的方法之一是坐下來袖手旁觀。下一代硬件和編譯器的優(yōu)化結(jié)果可以讓程序像以前一樣運行,只是速度會更快。在這個童話般的年代,有一個判斷優(yōu)化是否有效的簡單測試方法:如果程序員不能區(qū)分合法程序的未優(yōu)化執(zhí)行結(jié)果和優(yōu)化執(zhí)行的結(jié)果之間的區(qū)別(除了速度的區(qū)別),那么這個優(yōu)化就是有效的。也就是說,有效的優(yōu)化不會改變有效程序的行為。
幾年前, 某個悲傷的日子,硬件工程師發(fā)現(xiàn)讓單個處理器越來越快的魔法失效了。不過,他們發(fā)現(xiàn)了一個新的魔法,可以讓他們創(chuàng)造出擁有越來越多處理器的計算機(jī),操作系統(tǒng)使用線程抽象模型向程序員展示了這種硬件并行能力。這種新的魔法——多處理器以操作系統(tǒng)線程的形式提供并行能力——對硬件工程師來說效果更好,但它給編程語言設(shè)計者、編譯器作者和程序員帶來了嚴(yán)重的問題。
許多在單線程程序中不可見(因此有效)的硬件和編譯器優(yōu)化會在多線程程序中產(chǎn)生明顯的結(jié)果變化。如果有效的優(yōu)化沒有改變有效程序的行為,那么這些優(yōu)化應(yīng)該被認(rèn)為是無效的?;蛘攥F(xiàn)有程序必須被聲明為無效的。到底是哪一個,怎么判斷?
這里有一個類似C語言的簡單示例程序。在這個程序和我們將要考慮的所有程序中,所有變量最初都設(shè)置為零。
1 2 3 |
// Thread 1 // Thread 2 x = 1; while(done == 0) { /* loop */ } done = 1; print(x); |
如果線程1和線程2都運行在自己專用處理器上,都運行到完成,這個程序能打印 0 嗎?
看情況(It depends
)。這取決于硬件,也取決于編譯器。在x86多處理器上, 如果逐行翻譯成匯編的程序執(zhí)行的話總是會打印1。但是在ARM或POWER多處理器上,如果逐行翻譯成匯編的程序可以打印0。此外,無論底層硬件是什么,標(biāo)準(zhǔn)編譯器優(yōu)化都可能使該程序打印0或進(jìn)入無限循環(huán)。
“看情況”(It depends
)并不是一個圓滿的結(jié)局。程序員需要一個明確的答案來判斷一個程序是否在新的硬件和新的編譯器上能夠正確運行。硬件設(shè)計人員和編譯器開發(fā)人員也需要一個明確的答案,說明在執(zhí)行給定的程序時,硬件和編譯后的代碼可以有多精確。因為這里的主要問題是對存儲在內(nèi)存中數(shù)據(jù)更改的可見性和一致性,所以這個契約被稱為內(nèi)存一致性模型(memory consistency model
)或僅僅是內(nèi)存模型(memory model
)。
最初,內(nèi)存模型的目標(biāo)是定義程序員編寫匯編代碼時硬件提供的保證。在該定義下,是不包含編譯器的內(nèi)容的。25年前,人們開始嘗試寫內(nèi)存模型 ,用來定義高級編程語言(如Java或C++)對用該語言編寫代碼的程序員提供的保證。在模型中包含編譯器會使得定義一個合理模型的工作更加復(fù)雜。
這是關(guān)于硬件內(nèi)存模型和編程語言內(nèi)存模型的兩篇文章中的第一篇。我寫這些文章的目的是先介紹一下背景,以便討論我們可能想要對Go的內(nèi)存模型進(jìn)行的改變。但是,要了解Go當(dāng)前狀況,我們可能想去哪里,首先我們必須了解其他硬件內(nèi)存模型和語言內(nèi)存模型的現(xiàn)狀,以及他們采取的道路。
還是那句話,這篇文章講的是硬件。假設(shè)我們正在為多處理器計算機(jī)編寫匯編語言。程序員為了寫出正確的程序,需要從計算機(jī)硬件上得到什么保證?四十多年來,計算機(jī)科學(xué)家一直在尋找這個問題的好答案。
順序一致性
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.
為這種計算機(jī)設(shè)計和證明多處理算法正確性的通常方法假定滿足下列條件:任何執(zhí)行的結(jié)果都是相同的,就好像所有處理器的操作都是按某種順序執(zhí)行的,每個處理器的操作都是按程序指定的順序出現(xiàn)的。滿足這一條件的多處理器系統(tǒng)將被稱為順序一致的。
今天,我們不僅討論計算機(jī)硬件,還討論保證順序一致性的編程語言,當(dāng)程序的唯一可能執(zhí)行對應(yīng)于某種線程操作交替成順序執(zhí)行時。順序一致性通常被認(rèn)為是理想的模型,是程序員最自然的工作模式。它允許您假設(shè)程序按照它們在頁面上出現(xiàn)的順序執(zhí)行,并且單個線程的執(zhí)行只是以某種順序交替(interleaving
),而不是以其他方式排列。
人們可能會有理由質(zhì)疑順序一致性是否應(yīng)該是理想的模型,但這超出了本文的范圍。我只注意到,考慮到所有可能的線程交替(interleaving
)依然存在,就像在1979年一樣,即使過了四十幾年,Leslie Lamport的“設(shè)計和證明多處理算法正確性的慣用方法”,依然沒有什么能取代它。
之前我問這個程序能不能打印0:
1 2 3 |
// Thread 1 // Thread 2 x = 1; while(done == 0) { /* loop */ } done = 1; print(x); |
為了讓程序更容易分析,讓我們?nèi)サ粞h(huán)和打印,并詢問讀取共享變量的可能結(jié)果:
1 2 3 4 5 6 |
Litmus Test: Message Passing Can this program see r1 = 1, r2 = 0? // Thread 1 // Thread 2 x = 1 r1 = y y = 1 r2 = x |
我們假設(shè)每個例子都是所有共享變量最初都被設(shè)置為零。因為我們試圖確定硬件允許做什么,我們假設(shè)每個線程都在自己的專用處理器上執(zhí)行,并且沒有編譯器來對線程中發(fā)生的事情進(jìn)行重新排序:列表中的指令就是處理器執(zhí)行的指令。rN這個名字表示一個線程本地寄存器,而不是一個共享變量,我們會問一個線程本地寄存器的值在執(zhí)行結(jié)束時是否存在某種可能。
這種關(guān)于樣本程序執(zhí)行結(jié)果的問題被稱為litmus test
。因為它只有兩個答案——這個結(jié)果可能還是不可能?——litmus test
為我們提供了一種區(qū)分內(nèi)存模型的清晰方法:如果一個模型支持特定的執(zhí)行,而另一個不支持,那么這兩個模型顯然是不同的。不幸的是,正如我們將在后面看到的,一個特定的模型對一個特定的litmus test
給出的答案往往令人驚訝。
If the execution of this litmus test is sequentially consistent, there are only six possible interleavings:
如果該litmus test
的執(zhí)行順序一致,則只有六種可能的交替:
因為沒有交替執(zhí)行的結(jié)果會產(chǎn)生r1 = 1, r2 = 0
,所以這個結(jié)果是不允許的。也就是說,在順序執(zhí)行的硬件上,litmus test執(zhí)行結(jié)果出現(xiàn)r1 = 1, r2 = 0
是不可能的。
順序一致性的一個很好的思維模型是想象所有處理器直接連接到同一個共享內(nèi)存,它可以一次處理一個線程的讀或?qū)懻埱蟆?不涉及緩存,因此每次處理器需要讀取或?qū)懭雰?nèi)存時,該請求都會轉(zhuǎn)到共享內(nèi)存。 一次使用一次的共享內(nèi)存對所有內(nèi)存訪問的執(zhí)行施加了順序順序:順序一致性。
(本文中三個內(nèi)存模型圖摘自 Maranget et al. “A Tutorial Introduction to the ARM and POWER Relaxed Memory Models.”)
上圖是順序一致機(jī)器的模型,而不是構(gòu)建機(jī)器的唯一方法。 實際上,可以使用多個共享內(nèi)存模塊和緩存來構(gòu)建順序一致的機(jī)器來幫助預(yù)測內(nèi)存獲取的結(jié)果,但順序一致意味著機(jī)器的行為必須與該模型并無二致。 如果我們只是想了解順序一致執(zhí)行意味著什么,我們可以忽略所有這些可能的實現(xiàn)復(fù)雜性并只考慮這個模型。
不幸的是,對于我們程序員,放棄嚴(yán)格的順序一致性可以讓硬件更快地執(zhí)行程序,所以所有現(xiàn)代硬件在各方面都會偏離了順序一致性。準(zhǔn)確定義具體的硬件偏離是相當(dāng)困難的。本文以當(dāng)今廣泛使用的硬件中的兩種內(nèi)存模型為例:x86、ARM和POWER處理器系列。
x86 Total Store Order (x86-TSO)
現(xiàn)代x86系統(tǒng)的內(nèi)存模型對應(yīng)于以下硬件圖:
所有處理器仍然連接到一個共享內(nèi)存,但是每個處理器都將對該內(nèi)存的寫入(write
)放入到本地寫入隊列中。處理器繼續(xù)執(zhí)行新指令,同時寫操作(write
)會更新到這個共享內(nèi)存。一個處理器上的內(nèi)存讀取在查詢主內(nèi)存之前會查詢本地寫隊列,但它看不到其他處理器上的寫隊列。其效果就是當(dāng)前處理器比其他處理器會先看到自己的寫操作。但是——這一點非常重要——所有處理器都保證寫入(存儲store
)到共享內(nèi)存的(總)順序,所以給這個模型起了個名字:總存儲有序,或TSO
。當(dāng)一個寫操作到達(dá)共享內(nèi)存時,任何處理器上的任何未來讀操作都將看到它并使用該值(直到它被以后的寫操作覆蓋,或者可能被另一個處理器的緩沖寫操作覆蓋)。
寫隊列是一個標(biāo)準(zhǔn)的先進(jìn)先出隊列:內(nèi)存寫操作以與處理器執(zhí)行相同的順序應(yīng)用于共享內(nèi)存。因為寫入順序由寫入隊列保留,并且由于其他處理器會立即看到對共享內(nèi)存的寫入,所以我們之前考慮的通過litmus test
的消息與之前具有相同的結(jié)果: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寫入內(nèi)存,關(guān)于內(nèi)存寫入順序(總存儲有序)的系統(tǒng)級協(xié)議保證線程2在讀y的新值之前讀x的新值。因此,r1 = y
在r2 = x
看不到新的x之前不可能看到新的y。存儲順序至關(guān)重要:線程1在寫入y之前先寫入x,因此線程2在看到x的寫入之前不可能看到y(tǒng)的寫入。
在這種情況下,順序一致性和TSO模型是一致的,但是他們在其他litmus test的結(jié)果上并不一致。例如,這是區(qū)分兩種型號的常用示例:
1 2 3 4 5 6 7 8 |
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! |
在任何順序一致的執(zhí)行中,x = 1
或y = 1
必須首先發(fā)生,然后另一個線程中的讀取必須能夠觀察到它(此賦值事件),因此r1 = 0,r2 = 0
是不可能的。但是在一個TSO系統(tǒng)中,線程1和線程2可能會將它們的寫操作排隊,然后在任何一個寫操作進(jìn)入內(nèi)存之前從內(nèi)存中讀取,這樣兩個讀操作都會看到零。
這個例子看起來可能是人為制造的,但是使用兩個同步變量確實發(fā)生在眾所周知的同步算法中,例如德克爾算法或彼得森算法,以及特定的方案。如果一個線程沒有看到另一個線程的所有寫操作,線程就可能會中斷。
為了修復(fù)同步算法,我們需要依賴于更強的內(nèi)存排序,非順序一致的硬件提供了稱為內(nèi)存屏障(或柵欄)的顯式指令,可用于控制排序。我們可以添加一個內(nèi)存屏障,以確保每個線程在開始讀取之前都會刷新其先前對內(nèi)存的寫入:
1 2 3 4 |
// Thread 1 // Thread 2 x = 1 y = 1 barrier barrier r1 = y r2 = x |
加上正確的障礙,r1 = 0,r2 = 0
也是不可能的,德克爾或彼得森的算法就可以正常工作了。內(nèi)存屏障有很多種;具體細(xì)節(jié)因系統(tǒng)而異,不在本文討論范圍之內(nèi)。關(guān)鍵是內(nèi)存屏障的存在給了程序員或語言實現(xiàn)者一種在程序的關(guān)鍵時刻強制順序一致行為的方法。
最后一個例子,說明為什么這種模式被稱為總存儲有序。在該模型中,讀路徑上有本地寫隊列,但沒有緩存。一旦一個寫操作到達(dá)主存儲器,所有處理器不僅都認(rèn)同該值存在,而且還認(rèn)同它相對于來自其他處理器的寫操作的先后順序??紤]一下這個litmus test:
1 2 3 4 5 6 7 8 9 |
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(tǒng)先于x變化嗎?對于x86和其他TSO機(jī)器,答案是否定的:對主內(nèi)存的所有存儲(寫入)都有一個總順序,所有處理器都認(rèn)同這個順序,只是每個處理器在到達(dá)主內(nèi)存之前都先知道自己的寫入而已。
x86-TSO 之路
x86-TSO模型看起來相當(dāng)整潔,但是這條道路充滿了路障和錯誤的彎道。在20世紀(jì)90年代,第一批x86多處理器可用的手冊幾乎沒有提到硬件提供的內(nèi)存模型。
作為問題困擾的一個例子,Plan 9 是第一個在x86上運行的真正多處理器操作系統(tǒng)(沒有全局內(nèi)核鎖)。1997年,在移植到多處理器 奔騰Pro的過程中,開發(fā)人員被寫隊列l(wèi)itmus test的不期望的行為所困擾。一小段同步代碼假設(shè)r1 = 0,r2 = 0
是不可能的,但它確實發(fā)生了。更糟糕的是,英特爾手冊對內(nèi)存模型的細(xì)節(jié)模糊不清。
針對郵件列表中提出的“使用鎖最好保守一點,不要相信硬件設(shè)計師會做我們期望的事情”的建議,Plan 9的一名開發(fā)人員很好地解釋了這個問題:
我當(dāng)然同意。我們會在多處理器中遇到更寬松的順序(relaxed ordering )。問題是,硬件設(shè)計者認(rèn)為什么是保守的?在臨界區(qū)的開頭和結(jié)尾強制互鎖對我來說似乎相當(dāng)保守,但我顯然不夠富有想象力。奔騰Pro的手冊在描述緩存和怎么使它們保持一致時非常詳細(xì),但似乎不在乎說任何關(guān)于執(zhí)行或read順序的細(xì)節(jié)。事實是,我們無法知道自己是否足夠保守。
在討論過程中,英特爾的一名架構(gòu)師對內(nèi)存模型做了非正式的解釋,指出理論上,即使是多處理器486和奔騰系統(tǒng)也可能產(chǎn)生r1 = 0,r2 = 0
的結(jié)果,并且奔騰Pro只是具有更大的流水線和寫隊列,所以會更頻繁地暴露了這種行為。
這位英特爾架構(gòu)師還寫道:
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.粗略地說,這意味著從系統(tǒng)中任何一個處理器產(chǎn)生的事件的順序,正如其他處理器所觀察到的,總是相同的。然而,允許不同的觀察者對來自兩個或更多處理器的事件的交替有不同的觀察結(jié)果。
未來的英特爾處理器將采用相同的內(nèi)存順序模式。
聲稱“允許不同的觀察者對來自兩個或更多處理器的事件的交替有不同的觀察結(jié)果”是在說,IRIW litmus test的答案在x86上可以回答“是”,盡管在前面的部分我們看到x86回答“否”。這怎么可能呢?
答案似乎是,英特爾處理器實際上從未對這一litmus test做出“是”的回答,但當(dāng)時英特爾架構(gòu)人員不愿意為未來的處理器做出任何保證。體系結(jié)構(gòu)手冊中存在的少量文本幾乎沒有任何保證,使得很難針對它們進(jìn)行編程。
Plan 9的討論不是一個孤立的事件。從11月下旬開始,Linux內(nèi)核開發(fā)人員在他們的郵件列表上討論了100多條消息。
在接下來的十年里,越來越多的人遇到了這些困難,為此,英特爾的一組架構(gòu)師承擔(dān)了為當(dāng)前和未來的處理器寫下有用的處理器行為保證的任務(wù)。第一個結(jié)果是2007年8月出版的Intel 64 Architecture Memory Ordering White Paper,旨在為“軟件作者提供對不同順序的內(nèi)存訪問指令可能產(chǎn)生的結(jié)果的清晰理解”。同年晚些時候,AMD在AMD64 Architecture Programmer's Manual revision 3.14中發(fā)布了類似的描述。這些描述基于一個被稱為“總鎖序+因果一致性”(TLO+CC)的模型,故意弱于TSO。在公開訪談中,英特爾架構(gòu)師表示,TLO+CC“像要求的那樣強大,但并不足夠強大。”特別是,該模型保留了x86處理器在IRIW litmus test中回答“是”的權(quán)利。不幸的是,內(nèi)存屏障的定義不夠強大,不足以重建順序一致的內(nèi)存語義,即使每個指令之后都有一個屏障。更糟糕的是,研究人員觀察到實際的英特爾x86硬件違反了TLO+CC模型。例如:
1 2 3 4 5 6 7 8 9 10 11 |
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年晚些時候?qū)τ⑻貭柡虯MD規(guī)范的修訂保證了IRIW case的“不”,并加強了內(nèi)存屏障,但仍允許不可預(yù)期的行為,這些行為似乎不會出現(xiàn)在任何合理的硬件上。例如:
1 2 3 4 5 6 7 8 9 10 |
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模型的基礎(chǔ)上提出了x86-TSO模型提案。當(dāng)時,他們聲稱“據(jù)我們所知,x86-TSO是可靠的,足夠強大,可以在上面編程,并且大致符合供應(yīng)商的意圖?!皫讉€月后,英特爾和AMD發(fā)布了廣泛采用這一模式的的新手冊。
似乎所有英特爾處理器從一開始就實現(xiàn)了x86-TSO,盡管英特爾花了十年時間才決定致力于此。回想起來,很明顯,英特爾和AMD的設(shè)計師們正在努力解決如何編寫一個能夠為未來處理器優(yōu)化留出空間的內(nèi)存模型,同時仍然為編譯器作者和匯編語言程序設(shè)計者提供有用的保證?!坝卸鄰娋陀卸鄰姡珱]有多強”是一個艱難的平衡動作。
ARM/POWER Relaxed Memory Model
現(xiàn)在讓我們來看看一個更寬松的內(nèi)存模型,在ARM和POWER處理器上找到的那個。在實現(xiàn)層面上,這兩個系統(tǒng)在許多方面有所不同,但保證內(nèi)存一致性的模型大致相似,比x86-TSO甚至x86-TLO+CC稍弱。
ARM和POWER系統(tǒng)的概念模型是,每個處理器從其自己的完整內(nèi)存副本中讀取和向其寫入,每個寫入獨立地傳播到其他處理器,隨著寫入的傳播,允許重新排序。
這里沒有總存儲順序。雖然沒有描述,但是每個處理器都被允許推遲讀取(read
),直到它等到它需要結(jié)果:讀取(read
)可以被延遲到稍后的寫入(write
)之后。在這個寬松的(relaxed
)模型中,我們迄今為止所看到的每一個litmus test的答案都是“yes,這真的可能發(fā)生?!?/p>
對于通過litmus test的原始消息,單個處理器對寫入的重新排序意味著線程1的寫入可能不會被其他線程以相同的順序觀察到:
1 2 3 4 5 6 7 8 9 |
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都有各自獨立的內(nèi)存副本,寫操作以任何順序在內(nèi)存之間傳播。如果線程1的內(nèi)存在發(fā)送x的更新(update
)之前向線程2發(fā)送y的更新,并且如果線程2在這兩次更新之間執(zhí)行,它將確實看到結(jié)果r1 = 1,r2 = 0
。
該結(jié)果表明,ARM/POWER內(nèi)存模型比TSO更弱:對硬件的要求更低。ARM/POWER模型仍然承認(rèn)TSO所做的各種重組:
1 2 3 4 5 6 7 8 9 |
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
)可能會寫入本地存儲器,但當(dāng)讀取發(fā)生在相反的線程上時,寫入可能尚未傳播開來。
下面是一個litmus test,它展示了x86擁有總存儲順序意味著什么:
1 2 3 4 5 6 7 8 9 10 |
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上,不同的線程可能以不同的順序觀察到不同的寫操作。它們不能保證對到達(dá)主內(nèi)存的總寫入順序達(dá)成一致的觀察效果,因此線程3可以在y變化之前之前看到x的變化,而線程4可以在x變化之前看到y(tǒng)的變化。
作為另一個例子,ARM/POWER系統(tǒng)具有內(nèi)存讀取(負(fù)載 load)的可見緩沖或重新排序,如下面litmus test所示:
1 2 3 4 5 6 7 8 9 10 |
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,使得結(jié)果r1 = 1,r2 = 1不可能。然而,在ARM/POWER存儲器模型中,處理器被允許延遲讀取,直到指令流中稍后的寫入之后,因此y = 1和x = 1在兩次讀取之前執(zhí)行。
盡管ARM和POWER內(nèi)存模型都允許這一結(jié)果,但Maranget等人(2012年)報告說,只能在ARM系統(tǒng)上憑經(jīng)驗重現(xiàn),而不能在POWER上復(fù)制。在這里,模型和真實度之間的差異開始發(fā)揮作用,就像我們在檢查英特爾x86時一樣:硬件實現(xiàn)比技術(shù)保證更強大的模型會鼓勵對更強的行為的依賴,這意味著未來更弱的硬件將破壞程序,無論是否有效。
像TSO系統(tǒng)上一樣,ARM和POWER也有內(nèi)存屏障,我們可以在上面的例子中插入這些內(nèi)存屏障,以強制順序一致的行為。但顯而易見的問題是,沒有內(nèi)存屏障的ARM/POWER是否完全排除了任何行為。任何litmus test的答案是否都是“no,那不可能發(fā)生?” 當(dāng)我們專注于一個單一的內(nèi)存位置時,它可以。
這里有一個litmus test,它可以測試即使在ARM和POWER上也不會發(fā)生的事情:
1 2 3 4 5 6 7 8 9 10 |
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與前一個測試類似,但是現(xiàn)在兩個線程都在寫入單個變量x,而不是兩個不同的變量x和y。線程1和2將沖突的值1和2都寫入x,而線程3和線程4都讀取x兩次。如果線程3看到x = 1被x = 2覆蓋,那么線程4能看到相反的情況嗎?
答案是no的,即使在ARM/POWER上也是如此:系統(tǒng)中的線程必須就寫入單個內(nèi)存位置的總順序達(dá)成一致。也就是說,線程必須同意哪些寫入會覆蓋其他寫入。這個性質(zhì)叫做相干性。如果沒有一致性屬性,處理器要么不同意內(nèi)存的最終結(jié)果,要么報告內(nèi)存位置從一個值翻轉(zhuǎn)到另一個值,然后又回到第一個值。編寫這樣一個系統(tǒng)是非常困難的。
我故意忽略了ARM和POWER弱內(nèi)存模型中的許多微妙之處。更多詳細(xì)信息,請參閱彼得·蘇厄爾關(guān)于該主題的論文。有兩個要點要記住。首先,這里有令人難以置信的微妙之處,這是由有非常持久力、非常聰明的人進(jìn)行了十多年學(xué)術(shù)研究的主題。我自己并不聲稱完全理解。這不是我們應(yīng)該希望向普通程序設(shè)計人員解釋的事情,也不是我們在調(diào)試普通程序時希望能夠堅持的事情。第二,允許和觀察到的結(jié)果之間的差距造成了不幸的未來驚喜。如果當(dāng)前的硬件沒有展現(xiàn)出所有允許的行為——尤其是當(dāng)首先很難推理出什么是允許的時候!—那么不可避免地會編寫一些程序,這些程序會偶然地依賴于實際硬件的更受限制的行為。如果一個新的芯片在行為上受到的限制更少,那么硬件內(nèi)存模型在技術(shù)上允許破壞程序的新行為——也就是說,這個錯誤在技術(shù)上是你的錯——這一事實并不能給你帶來什么安慰。這不是寫程序的方法。
弱排序和無數(shù)據(jù)競爭的順序一致性
到目前為止,我希望您確信硬件細(xì)節(jié)是復(fù)雜而微妙的,而不是您每次編寫程序時都想解決的問題。 相反,它有助于識別“如果你遵循這些簡單的規(guī)則,你的程序只會產(chǎn)生結(jié)果,就像通過一些順序一致的執(zhí)行的那樣。” (我們?nèi)栽谡務(wù)撚布?,所以我們?nèi)栽谡務(wù)摻惶妾毩⒌膮R編指令。)
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.
同步模型是對內(nèi)存訪問的一組約束,這些約束指定了何時以及如何進(jìn)行同步。
硬件相對于同步模型是弱有序的,當(dāng)且僅當(dāng)它在順序上與遵守同步模型的所有軟件一致時。
雖然他們的論文是關(guān)于捕捉當(dāng)時的硬件設(shè)計(不是x86、ARM和POWER),但將討論提升到特定設(shè)計之上的想法使論文與今天的討論依然相關(guān)。
我之前說過“有效的優(yōu)化不會改變有效程序的行為?!边@些規(guī)則定義了什么是有效的手段,然后任何硬件優(yōu)化都必須讓這些程序像在順序一致的機(jī)器上一樣工作。當(dāng)然,有趣的細(xì)節(jié)是規(guī)則本身,定義程序有效的約束。
Adve和Hill提出了一種同步模型,他們稱之為無數(shù)據(jù)競爭(data-race-free,DRF)。該模型假設(shè)硬件具有獨立于普通內(nèi)存讀寫的內(nèi)存同步操作。普通的內(nèi)存讀寫可以在同步操作之間重新排序,但不能在跨它們移動。(也就是說,同步操作也可用來做重新排序的內(nèi)存屏障。)如果對于所有理想化的順序一致的執(zhí)行,從不同線程對同一位置的任何兩個普通存儲器訪問要么都是讀取,要么通過同步操作強制一個在另一個之前發(fā)生而分開執(zhí)行,則程序被稱為無數(shù)據(jù)競爭的。
我們來看一些例子,摘自Adve和Hill的論文(為了演示而重新繪制)。這里有一個線程執(zhí)行變量x的寫操作,然后讀取同一個變量。
垂直箭頭標(biāo)記了單個線程內(nèi)的執(zhí)行順序:先寫后讀。這個程序沒有競爭,因為一切都在一個線程中。
相比之下,在這個雙線程程序中有一個競爭:
這里線程2在不與線程1協(xié)調(diào)的情況下寫入x。線程2的寫入與線程1的寫入和讀取競爭。如果線程2讀x而不是寫x,程序在線程1寫和線程2讀之間只有一個競爭。每個競爭至少涉及一次寫入:兩次不協(xié)調(diào)的讀取不會相互競爭。
為了避免競爭,我們必須添加同步操作,這將在共享一個同步變量的不同線程上的操作之間強制一個特定的順序。如果同步S(a)(在變量a上同步,用虛線箭頭標(biāo)記)迫使線程2的寫操作在線程1完成后發(fā)生,則競爭被消除-
現(xiàn)在線程2的寫操作不能與線程1的操作同時發(fā)生。
如果線程2只是讀取,我們只需要與線程1的寫入同步。兩次讀取仍然可以同時進(jìn)行:
線程可以按同步順序排序,甚至可以使用中間線程。這個程序沒有競爭:
另一方面,同步變量的使用本身并不能消除競爭:錯誤地使用它們是可能的。下面這個程序有一個競爭:
線程2的讀取與其他線程中的寫入完全同步——這肯定發(fā)生在兩者之后——但是這兩個寫入本身并不同步。這個程序并不是data-race-free。
Adve和Hill將弱排序描述為“軟件和硬件之間的契約”,具體來說,如果軟件避免了數(shù)據(jù)競爭,那么硬件就好像是順序一致的,這比我們在前面部分研究的模型更容易推理。但是硬件如何滿足它的契約呢?
Adve和Hill給出了硬件“遵循DRF弱排序”的證明,這意味著它執(zhí)行無數(shù)據(jù)競爭的程序,就好像是按照順序一致的順序一樣,只要它滿足一組特定的最低要求。我不打算詳談細(xì)節(jié),但重點是在Adve和Hill的論文發(fā)表后,硬件設(shè)計師們有了一份由理論支持的手冊:做這些事情,你就可以斷言你的硬件將與data-race-free程序順序一致。事實上,假設(shè)同步操作的適當(dāng)實現(xiàn),大多數(shù)寬松的硬件確實是這樣做的,并且一直在繼續(xù)這樣做。Adve和Hill最初關(guān)注的是VAX,但x86、ARM和POWER肯定也能滿足這些限制。這種系統(tǒng)保證無數(shù)據(jù)競爭程序的順序一致性的觀點通常被縮寫為DRF-SC。
DRF-SC標(biāo)志著硬件內(nèi)存模型的一個轉(zhuǎn)折點,為硬件設(shè)計者和軟件作者提供了一個清晰的策略,至少是那些用匯編語言編寫軟件的人。正如我們將在下一篇文章中看到的,高級編程語言的內(nèi)存模型問題沒有一個整潔的答案。
本文轉(zhuǎn)自:https://colobu.com/2021/06/30/hwmm/
審核編輯:符乾江
-
內(nèi)存
+關(guān)注
關(guān)注
8文章
2981瀏覽量
73824 -
硬件
+關(guān)注
關(guān)注
11文章
3224瀏覽量
66070
發(fā)布評論請先 登錄
相關(guān)推薦
評論