第 10 章 記憶體模型：困難的部分

本章描述 OCaml 寬鬆記憶體模型的細節。寬鬆記憶體模型描述當讀取記憶體位置時，OCaml 程式允許觀察到的值。如果您對 OCaml 中的高階平行程式設計感興趣，請參閱平行程式設計章節 9。

本章旨在為希望從實務角度了解 OCaml 記憶體模型細節的專家而撰寫。有關 OCaml 記憶體模型的正式定義、其保證以及編譯為硬體記憶體模型，請參閱 PLDI 2018 年關於在空間和時間上界定資料競爭的論文。本章中介紹的記憶體模型是 PLDI 2018 年論文中介紹的模型的延伸。本章還涵蓋了論文中未涵蓋的記憶體模型的一些實用方面。

1 為什麼要弱一致性記憶體？

我們可以給予程式最簡單的記憶體模型是循序一致性。在循序一致性下，程式觀察到的值可以透過程式中來自不同網域的操作的某些交錯來解釋。例如，考慮以下具有兩個網域 d1 和 d2 並行執行的程式

let d1 a b = let r1 = !a * 2 in let r2 = !b in let r3 = !a * 2 in (r1, r2, r3) let d2 b = b := 0 let main () = let a = ref 1 in let b = ref 1 in let h = Domain.spawn (fun _ -> let r1, r2, r3 = d1 a b in Printf.printf "r1 = %d, r2 = %d, r3 = %d\n" r1 r2 r3) in d2 b; Domain.join h

參考儲存格 a 和 b 最初為 1。如果 d2 中寫入 b 的操作發生在 d1 中讀取 b 之前，使用者可能會觀察到 r1 = 2, r2 = 0, r3 = 2。在此，觀察到的行為可以透過來自不同網域的操作交錯來解釋。

現在讓我們假設 a 和 b 是彼此的別名。

let d1 a b = let r1 = !a * 2 in let r2 = !b in let r3 = !a * 2 in (r1, r2, r3) let d2 b = b := 0 let main () = let ab = ref 1 in let h = Domain.spawn (fun _ -> let r1, r2, r3 = d1 ab ab in assert (not (r1 = 2 && r2 = 0 && r3 = 2))) in d2 ab; Domain.join h

在上述程式中，變數 ab、a 和 b 指的是相同的參考儲存格。人們會預期主函數中的斷言永遠不會失敗。原因是如果 r2 是 0，則 d2 中的寫入發生在 d1 中讀取 b 之前。假設 a 和 b 是別名，則 d1 中第二次讀取 a 也應該傳回 0。

1.1 編譯器最佳化

令人驚訝的是，由於編譯器最佳化，此斷言在 OCaml 中可能會失敗。OCaml 編譯器觀察到 d1 中的常見子表達式 !a * 2，並將程式最佳化為

let d1 a b = let r1 = !a * 2 in let r2 = !b in let r3 = r1 in (* CSE: !a * 2 ==> r1 *) (r1, r2, r3) let d2 b = b := 0 let main () = let ab = ref 1 in let h = Domain.spawn (fun _ -> let r1, r2, r3 = d1 ab ab in assert (not (r1 = 2 && r2 = 0 && r3 = 2))) in d2 ab; Domain.join h

此最佳化稱為常見子表達式消除 (CSE)。此類最佳化對於良好的效能是有效且必要的，並且不會改變程式的循序含義。然而，CSE 會破壞循序推理。

在上面最佳化的程式中，即使 d2 中寫入 b 的操作發生在 d1 中的第一次讀取和第二次讀取之間，程式也會觀察到 r3 的值 2，導致斷言失敗。觀察到的行為無法透過來源程式中來自不同網域的操作交錯來解釋。因此，CSE 最佳化在循序一致性下被認為是無效的。

一種解釋觀察到的行為的方法是，就好像在網域上執行的操作被重新排序一樣。例如，如果從 d1 的第二次和第三次讀取被重新排序，

let d1 a b = let r1 = !a * 2 in let r3 = !a * 2 in let r2 = !b in (r1, r2, r3)

那麼我們可以解釋 d1 傳回的觀察到的行為 (2,0,2)。

1.2 硬體最佳化

另一個重新排序的來源是硬體。現代硬體架構具有複雜的快取階層結構，具有多個快取層級。雖然快取一致性確保讀寫到單一記憶體位置時遵守循序一致性，但對在不同記憶體位置上運作的程式的保證要弱得多。考慮以下程式

let a = ref 0 and b = ref 0 let d1 () = a := 1; !b let d2 () = b := 1; !a let main () = let h = Domain.spawn d2 in let r1 = d1 () in let r2 = Domain.join h in assert (not (r1 = 0 && r2 = 0))

在循序一致性下，我們永遠不會預期斷言會失敗。然而，即使在提供比 ARM 更強大保證的 x86 上，CPU 核心執行的寫入也不會立即發佈到所有其他核心。由於 a 和 b 是不同的記憶體位置，a 和 b 的讀取都可能會觀察到初始值，導致斷言失敗。

如果允許在先前儲存到不同記憶體位置之前重新排序載入，則可以解釋此行為。這種重新排序可能是由於現代處理器上存在核心內儲存緩衝區。每個核心實際上都有一個待處理寫入的 FIFO 緩衝區，以避免在寫入完成時需要封鎖。對 a 和 b 的寫入可能分別在執行網域 d1 和 d2 的核心 c1 和 c2 的儲存緩衝區中。如果寫入尚未從緩衝區傳播到主記憶體，則分別在核心 c1 和 c2 上執行的 b 和 a 的讀取將看不到寫入。

2 資料競爭自由蘊含循序一致性

OCaml 寬鬆記憶體模型的目的是精確地描述 OCaml 程式保留哪些順序。只要編譯器和硬體尊重記憶體模型的排序保證，它們就可以自由地最佳化程式。雖然直接在寬鬆記憶體模型下進行程式設計很困難，但記憶體模型也描述了程式僅會顯示循序一致行為的條件。此保證稱為資料競爭自由蘊含循序一致性 (DRF-SC)。在本節中，我們將描述此保證。為了做到這一點，我們首先需要一些定義。

2.1 記憶體位置

OCaml 將記憶體位置分類為原子和非原子位置。參考儲存格、陣列欄位和可變記錄欄位是非原子記憶體位置。不可變物件是非原子位置，具有初始化的寫入但沒有進一步的更新。原子記憶體位置是使用 Atomic 模組建立的位置。

2.2 發生於之前關係

讓我們想像一下，OCaml 程式是由一個抽象機器執行的，該機器一次執行一個動作，並且在每一步驟中任意選擇一個可用的域。我們將動作分為兩類：跨域和域內。跨域動作是指可以被其他域的動作觀察和影響的動作。跨域動作有以下幾種：

另一方面，域內動作既不能被觀察到，也不能影響其他域的執行。範例包括評估算術表達式、調用函數等。記憶體模型規範會忽略此類域內動作。在後續內容中，我們使用術語「動作」來表示跨域動作。

抽象機器執行的動作的全序列表稱為執行追蹤。由於非確定性，給定程式可能有多個可能的執行追蹤。

對於給定的執行追蹤，我們定義一個非自反的、傳遞的先行發生關係，它捕獲 OCaml 程式中動作之間的因果關係。先行發生關係被定義為滿足以下屬性的最小傳遞關係：

2.3 資料競爭

在給定的追蹤中，如果兩個動作存取相同的非原子位置，且至少有一個是寫入，而且都不是對該位置的初始化寫入，則稱這兩個動作是衝突的。

如果程式的某些執行追蹤中存在兩個衝突的動作，並且在這些衝突的存取之間不存在先行發生關係，則我們說程式存在資料競爭。沒有資料競爭的程式被稱為是正確同步的。

2.4 DRF-SC

DRF-SC 保證：沒有資料競爭的程式只會表現出循序一致的行為。

DRF-SC 為程式設計師提供了強有力的保證。程式設計師可以使用循序推理，也就是透過一個接一個地執行跨域動作進行推理，以識別他們的程式是否有資料競爭。特別是，他們不需要為了確定程式是否有資料競爭而對第10.1節中描述的重新排序進行推理。一旦確定特定程式是沒有資料競爭的，他們就不需要擔心程式碼中的重新排序。

3 使用 DRF-SC 進行推理

在本節中，我們將看看使用 DRF-SC 進行程式推理的範例。在本節中，我們將使用名稱為 dN 的函式來表示與其他域並行執行的域。也就是說，我們假設有一個 main 函式，它會並行執行 dN 函式，如下所示：

let main () =
  let h1 = Domain.spawn d1 in
  let h2 = Domain.spawn d2 in
  ...
  ignore @@ Domain.join h1;
  ignore @@ Domain.join h2

以下是一個簡單的資料競爭範例：

(* 有資料競爭 *) let r = ref 0 let d1 () = r := 1 let d2 () = !r

r 是一個非原子參考。這兩個域競相存取該參考，並且 d1 是一個寫入。由於衝突的存取之間沒有先行發生關係，因此存在資料競爭。

我們在第10.1節中看到的兩個程式都有資料競爭。它們表現出非循序一致的行為並不奇怪。

並行存取不相交的陣列索引和記錄欄位不會造成資料競爭。例如：

(* 沒有資料競爭 *) let a = [| 0; 1 |] let d1 () = a.(0) <- 42 let d2 () = a.(1) <- 42
(* 沒有資料競爭 *) type t = { mutable a : int; mutable b : int } let r = {a = 0; b = 1} let d1 () = r.a <- 42 let d2 () = r.b <- 42

沒有資料競爭。

原子位置上的競爭不會導致資料競爭。

(* 沒有資料競爭 *) let r = Atomic.make 0 let d1 () = Atomic.set r 1 let d2 () = Atomic.get r

訊息傳遞

原子變數可用於實作域之間的非阻塞通訊。

(* 沒有資料競爭 *) let msg = ref 0 let flag = Atomic.make false let d1 () = msg := 42; (* a *) Atomic.set flag true (* b *) let d2 () = if Atomic.get flag (* c *) then !msg (* d *) else 0

請注意，動作 a 和 d 分別寫入和讀取相同的非原子位置 msg，因此是衝突的。我們需要建立 a 和 d 之間存在先行發生關係，才能證明此程式沒有資料競爭。

動作 a 在程式順序中先於 b，因此 a 先行發生於 b。同樣，c 先行發生於 d。如果 d2 觀察到原子變數 flag 為 true，則 b 在先行發生順序中先於 c。由於先行發生是可傳遞的，因此衝突的動作 a 和 d 處於先行發生順序中。如果 d2 觀察到 flag 為 false，則不會執行對 msg 的讀取。因此，此執行追蹤中沒有衝突的存取。因此，此程式沒有資料競爭。

以下修改後的訊息傳遞程式確實有資料競爭。

(* 有資料競爭 *) let msg = ref 0 let flag = Atomic.make false let d1 () = msg := 42; (* a *) Atomic.set flag true (* b *) let d2 () = ignore (Atomic.get flag); (* c *) !msg (* d *)

域 d2 現在無條件讀取非原子參考 msg。請考慮執行追蹤

Atomic.get flag; (* c *)
!msg; (* d *)
msg := 42; (* a *)
Atomic.set flag true (* b *)

在此追蹤中，d 和 a 是衝突的操作。但是它們之間沒有先行發生關係。因此，此程式有資料競爭。

4 局部資料競爭自由

OCaml 記憶體模型甚至對具有資料競爭的程式也提供了強大的保證。它提供了所謂的局部資料競爭自由循序一致性 (LDRF-SC) 保證。此屬性的正式定義超出了本手冊章節的範圍。我們鼓勵感興趣的讀者閱讀 2018 年 PLDI 上關於 在空間和時間中限制資料競爭 的論文。

非正式地說，LDRF-SC 表示程式中沒有資料競爭的部分會保持循序一致性。也就是說，即使程式有資料競爭，那些與有資料競爭的部分不相交的程式部分仍然適用於循序推理。

請考慮以下程式碼片段：

let snippet () = let c = ref 0 in c := 42; let a = !c in (a, c)

請注意，c 是一個新分配的參考。對 c 的讀取可以傳回不是 42 的值嗎？也就是說，a 可以不是 42 嗎？令人驚訝的是，在 C++ 和 Java 記憶體模型中，答案是肯定的。在 C++ 記憶體模型中，如果程式有資料競爭，即使在不相關的部分，其語意也是未定義的。如果此程式碼片段與具有資料競爭的程式庫連結，那麼在 C++ 記憶體模型下，讀取可能會傳回任何值。由於不相關位置上的資料競爭可能會影響程式行為，因此我們說 C++ 記憶體模型在空間上不是有界的。

與 C++ 不同，Java 記憶體模型在空間上是受限的。但 Java 記憶體模型在時間上不受限；未來的資料競爭會影響過去的行為。例如，考慮將此範例翻譯成 Java。我們假設先前定義了 Class c {int x;} 和一個共享的非 volatile 變數 C g。現在，這個程式碼片段可能是一個較大程式中並行執行緒的一部分

(* Thread 1 *)
C c = new C();
c.x = 42;
a = c.x;
g = c;

(* Thread 2 *)
g.x = 7;

在第一個執行緒中，讀取 c.x 和寫入 g 是在不同的記憶體位置上進行的。因此，Java 記憶體模型允許它們重新排序。結果，第二個執行緒中的寫入可能發生在讀取 c.x 之前，因此 c.x 返回 7。

上述 Java 程式碼的 OCaml 等效程式碼是

let g = ref None let snippet () = let c = ref 0 in c := 42; let a = !c in (a, c) let d1 () = let (a,c) = snippet () in g := Some c; a let d2 () = match !g with | None -> () | Some c -> c := 7

請注意，在 g 和 c 上都有資料競爭。僅考慮 snippet 中的前三個指令

let c = ref 0 in
c := 42;
let a = !c in
...

OCaml 記憶體模型在空間和時間上都是受限的。這裡唯一的記憶體位置是 c。僅就這個程式碼片段而言，既沒有空間上的資料競爭（在 g 上的競爭），也沒有時間上的資料競爭（未來在 c 上的競爭）。因此，這個程式碼片段將具有循序一致的行為，並且 !c 返回的值將是 42。

OCaml 記憶體模型保證即使對於有資料競爭的程式，記憶體安全性也會得到保留。雖然有資料競爭的程式可能會觀察到非循序一致的行為，但它們不會崩潰。

5 記憶體模型的運作觀點

在本節中，我們將描述 OCaml 記憶體模型的語意。記憶體模型的運作觀點的正式定義在 PLDI 2018 關於在空間和時間上限制資料競爭的論文第 3 節中提出。本節將借助一個範例，對記憶體模型進行非正式的描述。

給定一個可能包含資料競爭的 OCaml 程式，運作語意會告訴您讀取記憶體位置可能觀察到的值。為了簡單起見，我們將執行緒內部的動作限制為僅對原子和非原子位置的存取，忽略網域的產生和加入操作，以及互斥鎖上的操作。

我們以簡單的小步驟運作方式來描述 OCaml 記憶體模型的語意。也就是說，該語意由一個抽象機器描述，該機器一次執行一個動作，在每一步中任意選擇一個可用的網域。這類似於我們在第 ‍10.2.2節中用於描述「發生在之前」關係的抽象機器。

5.1 非原子位置

在語意中，我們將非原子位置建模為從時間戳記 t 到值 v 的有限映射。我們將時間戳記視為有理數。時間戳記是完全排序的，但稠密的；任何兩個時間戳記之間都有一個時間戳記。

例如，

a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t8 -> 7]

表示三個非原子位置 a、b 和 c 及其歷史記錄。位置 a 在時間戳記 t1 和 t2 有兩次寫入，值分別為 1 和 2。當我們寫入 a: [t1 -> 1; t2 -> 2] 時，我們假設 t1 < t2。我們假設這些位置的初始化歷史記錄在時間戳記 0 有一個單一條目，該條目映射到初始值。

5.2 網域

每個網域都配備了一個邊界，它是從非原子位置到時間戳記的映射。直觀地說，每個網域的邊界都會記錄，對於每個非原子位置，執行緒已知的最新寫入。可能發生了更新的寫入，但不保證是可見的。

例如，

d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t7]

表示兩個網域 d1 和 d2 及其邊界。

5.3 非原子存取

現在讓我們定義非原子讀取和寫入的語意。假設網域 d1 執行 b 的讀取。對於非原子讀取，網域可以讀取該位置歷史記錄的任意元素，只要它不早於網域邊界中的時間戳記即可。在這種情況下，由於 d1 在 b 的邊界處於 t3，因此讀取可能會返回值 3、4 或 5。非原子讀取不會變更目前網域的邊界。

假設網域 d2 將值 10 寫入 c（c := 10）。我們為這個寫入選擇一個新的時間戳記 t9，使其晚於 d2 在 c 的邊界。請注意這裡的細微之處：這個新的時間戳記可能不晚於歷史記錄中的所有其他內容，而僅晚於寫入網域已知的任何其他寫入。因此，t9 可以插入到 c 的歷史記錄中 (a) 在 t7 和 t8 之間，或 (b) 在 t8 之後。為了我們的討論，讓我們選擇前一種選項。由於新的寫入出現在網域 d2 已知的所有位置 c 的寫入之後，因此 d2 在 c 的邊界也會更新。抽象機器的狀態如下：

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7] (* new write at t9 *)

(* Domains *)
d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t9] (* frontier updated at c *)

5.4 原子存取

原子位置不僅攜帶值，還攜帶同步資訊。我們將原子位置建模為該位置持有的值和邊界的一對。邊界建模同步資訊，該資訊與操作該位置的執行緒的邊界合併。通過這種方式，一個執行緒進行的非原子寫入可以通過原子位置進行通信，從而被另一個執行緒所知。

例如，

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

顯示了兩個原子變數 A 和 B，它們的值分別為 10 和 5，並且它們各自的邊界。我們使用大寫變數名稱來表示原子位置。

在原子讀取期間，該位置的邊界會合併到執行讀取的網域的邊界中。例如，假設 d1 讀取 B。讀取返回 5，並且通過將其與 B 的邊界合併來更新 d1 的邊界，並為每個位置選擇較晚的時間戳記。原子讀取之前的抽象機器狀態如下：

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t9]

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

由於原子讀取，抽象機器的狀態更新為：

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t2; b -> t4; c -> t7] (* frontier updated at a and b *)
d2: [a -> t1; b -> t4; c -> t9]

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

在原子寫入期間，原子位置持有的值會被更新。寫入網域的邊界和被寫入位置的邊界都會更新為兩個邊界的合併。例如，如果 d2 在目前的機器狀態下將 20 寫入 A，則機器狀態更新為：

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t2; b -> t4; c -> t7]
d2: [a -> t1; b -> t5; c -> t9] (* frontier updated at b *)

(* Atomic locations *)
A: 20, [a -> t1; b -> t5; c -> t9] (* value updated. frontier updated at c. *)
B: 5,  [a -> t2; b -> t4; c -> t6]

5.5 使用語意進行推理

讓我們重新檢視先前的範例（第 10.1節）。

let a = ref 0 and b = ref 0 let d1 () = a := 1; !b let d2 () = b := 1; !a let main () = let h = Domain.spawn d2 in let r1 = d1 () in let r2 = Domain.join h in assert (not (r1 = 0 && r2 = 0))

這個程式在 a 和 b 上有資料競爭，因此，該程式可能會表現出非循序一致的行為。讓我們使用語意來說明該程式可能會表現出 r1 = 0 && r2 = 0。

抽象機器的初始狀態如下：

(* Non-atomic locations *)
a: [t0 -> 0]
b: [t1 -> 0]

(* Domains *)
d1: [a -> t0; b -> t1]
d2: [a -> t0; b -> t1]

執行這個程式有多個可能的排程。讓我們考慮以下排程

1: a := 1 @ d1
2: b := 1 @ d2
3: !b     @ d1
4: !a     @ d2

在 d1 執行第一個動作 a:=1 之後，機器狀態如下：

(* Non-atomic locations *)
a: [t0 -> 0; t2 -> 1] (* new write at t2 *)
b: [t1 -> 0]

(* Domains *)
d1: [a -> t2; b -> t1] (* frontier updated at a *)
d2: [a -> t0; b -> t1]

在 d2 執行第二個動作 b:=1 之後，機器狀態如下：

(* Non-atomic locations *)
a: [t0 -> 0; t2 -> 1]
b: [t1 -> 0; t3 -> 1] (* new write at t3 *)

(* Domains *)
d1: [a -> t2; b -> t1]
d2: [a -> t0; b -> t3] (* frontier updated at b *)

現在，對於 d1 的第三個動作 !b，請注意 d1 在 b 的邊界處於 t1。因此，讀取可能會返回 0 或 1。讓我們假設它返回 0。非原子讀取不會更新機器狀態。

類似地，對於 d2 執行的第四個動作 !a，d2 在 a 的邊界位於 t0。因此，這次讀取也可能返回 0 或 1。讓我們假設它返回 0。因此，原始程式中的斷言 assert (not (r1 = 0 && r2 = 0))，將會在此特定執行中失敗。

6 不符合記憶體模型的運算

有些運算不符合記憶體模型。

Copyright © 2024 Institut National de Recherche en Informatique et en Automatique