ThreadSanitizer——跟data race說再見

08-17

來自專欄分散式和存儲的那些事51 人贊了文章

原文因為題圖問題掛了，換一張試試...

人生幾大喜（cuo）事（jue），新鮮出爐的單元測試直接過了。

說到data race，相信各位都已是見得多了。但若不是身經百戰，這傢伙總還會陰魂不散，讓程序或人崩潰。

一般來說，常見的data race並不是很難理解。往往當你意識到它存在的時候，你可以花一些功夫推導出哪裡出問題了。但難就難在，很多時候我們寫代碼時沒有意識到它的存在。

有沒有可能將我們推導的思路進行量化，讓機器幫助我們在運行時檢查可能的data race，並且當它發生時準確地定位出來呢？

ThreadSanitizer（簡稱tsan）是一款可以幫你檢測大多數的data race的工具。不但如此，它還專門發了篇論文[1]介紹了原理（ps 相關理論和工具其實很早就有了）。本質上，這是一次對於Lamport Clock在多線程領域的應用，因此閱讀之前推薦看下Lamport老爺子的[3]，配合丁凱：事件和時間：Time, Clocks, and the Ordering of Events in a Distributed System 讀後感一文食用效果更佳。（也可以直接看 @丁凱的讀後感，總結得很清晰。）

kk，讓我們將data race上升到一個學術高度，一起提高一下姿勢水平，然後跟它說再見。

tsan本質是一個狀態機。在程序執行期間，它會一直觀測各類事件（event），並維護了一個全局的事件隊列。每當一個新的事件發生時，tsan會將其加入到事件隊列中，並更新自己的狀態，然後通過狀態判斷這個事件是否導致了data race。

tsan中的事件可以分為兩大類：內存訪問（memory access）事件和同步（synchronization）事件。

內存操作事件比較簡單，就是讀（Read）和寫（Write）兩種。

而同步事件可以進一步細分成鎖（locking）事件和happens-before（囧rz，實在不會翻譯）事件。鎖事件包括了WriterLock，WriterUnlock，ReaderLock以及ReaderUnlock四種。happens-before事件包括了Signal和Wait兩種。本質上，這對事件對應一個通道（channel）上的Send和Receive操作（[3]）。

為了簡單起見，本文的討論將不細分ReaderLock和WriterLock。因此鎖事件可以被簡化成兩種，Lock和Unlock。下圖是tsan中所有事件類型的一個總結。

tsan中的所有事件類型

概念定義

解決問題的第一步就是要嚴謹的描述問題，讓我們看看tsan都定義了哪些概念。

首先擺上幾個常用的邏輯符號，方便各位猿媛： $land$ 是&&， $lor$ 是||， $eg$ 是!。

Tid（thread ID，T）：線程編號。每個線程Tid唯一。

ID：內存地址，可以理解成指針。當前實現中，一個ID對應內存中的一個byte。

EventType（事件類型）：即上面所列舉到的Read、Write、Lock、Unlock、Signal和Wait。

Event（事件）：一個包含了(EventType, Tid, ID)的tuple，記作 $ext{EventType}_{Tid}(ID)$ 。

事件隊列：事件隊列就是tsan所記錄下來的發生過的事件，記作 $langle e angle$ 。每個事件在隊列中都有唯一的編號，且當前tsan所觀測到的所有事件就是 $langle e angle$ 本身。當一個新的事件發生時，tsan會將其記錄在隊列尾部。註：原文[1]中並沒有此術語的定義。

Lock（鎖，L）：一個出現在鎖事件（包括Lock和Unlock）的內存ID。如果在某一時刻，事件隊列中所包含的 $ext{Lock}_T(L)$ 的數量大於 $ext{Unlock}_T(L)$ 的數量，我們稱該鎖L被線程T持有（held）。原文[1]其實在這裡細分出了write-held和read-held，但簡化後兩者等價。

Lock Set（LS）：某個線程所持有的鎖的集合。同樣，原文又細分了Writer LS和Reader LS，本文中兩者等價。

Event Context（事件上下文）：即stack trace（只用於彙報data race，本文討論中可以忽略）。

Segment（片段）：一個線程內的一段只包含內存操作的事件流。任何一個內存操作事件都只屬於某一個片段。由於片段是屬於某一個線程的，因此每個片段可以通過它所在的線程找到對應的鎖集合。同樣，每個內存操作事件也可以通過它所在的線程找到對應的鎖集合。片段的上下文定義為該片段中第一個事件的上下文。

下面的幾個術語可能會引起頭痛、噁心、嗜睡等癥狀，我會加入一些「人話「和栗子幫助理解。

Happens-before arc（happens-before弧）：對於一對事件 $X= ext{Signal}_{T_X}(A_X)$ 和 $Y= ext{Wait}_{T_Y}(A_Y)$ ，如果 $(A_X = A_Y) land (T_X e T_Y)$ ，並且 $X$ 先被tsan觀測到，那麼稱 $(X, Y)$ 構成一條happens-before弧。

人話：對於一個消息通道（其在內存中的地址為 $A_X$ ），線程 $T_X$ 在該通道上發送了消息，而另一個線程 $T_Y$ 在通道上等待接收消息，那麼 $T_X$ 發送消息一定發生在 $T_Y$ 接收到消息之前。這是邏輯上的因果關係，跟你用的哪個語言，哪種數據結構，怎麼實現的（得是正確的實現...）無關。

Happens-before：一個事件集合上的偏序關係（partial order）。對於兩個事件 $X = ext{EventType}_{T_X}(A_X)$ 和 $Y = ext{EventType}_{T_Y}(A_Y)$ ，稱 $X$ happens-before $Y$ （ $X prec Y$ ），如果 $X$ 先被tsan觀測到，並且以下任意條件成立：

$T_X = T_Y$ 。這很直觀，同一個線程內的事件自然是有序的。
$(X, Y)$ 構成一條happens-before弧。同樣很直觀。
$exists E_1, E_2: X preceq E_1 prec E_2 preceq Y$ 。這還是很直觀：happens-before $prec$ 具有傳遞性（transitivity）

而 $X preceq Y$ 表示 $X prec Y lor X = Y$ ， $X preceq Y$ 表示 $eg (X preceq Y)$ 。

$X preceq Y$ 有兩種可能： $Y prec X$ 或者 $Y preceq X$ 。當 $(X preceq Y) land (Y preceq X)$ 時，我們稱 $X, Y$ 不可比較（incomparable）。

一定要記住， $prec$ 和某次執行時事件隊列的順序是有區別的。如果 $X prec Y$ ，那麼執行時 $X$ 一定先於 $Y$ 發生，也一定在事件隊列之前。但不能因為某一次執行時 $X$ 發生在了 $Y$ 之前就得出 $X prec Y$ 的結論！

Segment Set（SS）：一個片段集合 ${S_1, S_2, dots, S_N}$ ，滿足 $forall i, j: S_i preceq S_j$ 。這裡要注意 $i, j$ 的任意性，即 $S_i preceq S_j$ 和 $S_j preceq S_i$ 要同時成立。這裡的人話我們攢到下面說。

Concurrent（並行）：兩個內存操作事件 $X$ 和 $Y$ 被稱為並行的，如果 $(X preceq Y) land (Y preceq X) land (LS(X) cap LS(Y) = emptyset)$ 。

人話：拋開最後一個鎖集合的條件，前面兩點其實跟片段集合定義相同。它說的是事件 $X$ 和 $Y$ 邏輯上的不可比較（不存在偏序關係）。換句話說，每次程序執行時是 $X$ 先於 $Y$ ，還是 $Y$ 先於 $X$ 發生，這是不確定的，純看compiler、OS等各位爺的心情。正因如此，它們才構成了並行執行的必要不充分條件。

雖然邏輯上不存在順序，我們仍可以用鎖來強制執行時的互斥性（exclusivity）。這也是第三個條件所說的：只有當這兩個事件並沒有被任何鎖同步時，它們才是真正意義上的並行發生的。

互斥性並不意味著邏輯上的有序性。每次執行時獲取鎖的順序仍然是看各位爺的心情。

我們來看看下面這段代碼：

// Thread 1 | // Thread 2mu.Lock(); | mu.Lock();foo = 42; // X = Write_T1(foo) | ++bar; // Y = Write_T2(bar)mu.Unlock(); | mu.Unlock();

拋開鎖操作，這裡的 $X = ext{Write}_{T1}( exttt{foo})$ 和 $Y = ext{Write}_{T2}( exttt{bar})$ 滿足 $X preceq Y land Y preceq X$ ，兩事件是不可比較的。但由於 $LS(X) cap LS(Y) = { exttt{mu} }$ ，兩個線程並沒有辦法並行執行。

而換成這樣的話：

// Thread 1 | // Thread 2mu.Lock(); | foo = 42; // X = Write_T1(foo) | ++bar; // Y = Write_T2(bar)mu.Unlock(); |

$LS(X) cap LS(Y) = { exttt{mu} } cap {} = emptyset$ ，因此兩個線程可以並行執行。

Data Race：data race是指兩個線程並行的操作了同一個內存地址ID，並且至少其中一個內存操作事件是Write（讀-讀操作當然不存在data race）。這就是我們工程中說的data race。

以上就是tsan中全部的術語概念。我們用一個時序圖的栗子來加深下對這些概念，尤其是 $prec$ 關係的理解。

兩個等價的栗子，縱軸代表時間線。

先看左邊的栗子。 $S1 prec S4$ ，因為它們發生在同一個線程中。 $S1 prec S3$ ，因為它們之間存在一條由 $( ext{Signal}, ext{Wait})$ 構成的happens-before弧，再由傳遞性即可得證。而我們無法判斷 $S1, S2$ 的順序，即 $S1 preceq S2 land S2 preceq S1$ ，因此 ${S1, S2}$ 構成一個片段集合。同樣， ${S3, S4}$ 也是一個片段集合。

那麼 $S2, S4$ 呢？看著好像是 $S2$ 發生早於 $S4$ 啊？

讓我們把視線轉向右邊。

每個線程內的事件順序都沒有變，然而 $S2$ 這次晚於 $S4$ 了。事實上， $S2$ 和 $S4$ 之間並不存在邏輯上的因果關係，因此 ${S2, S4}$ 還是一個片段集合。

直觀上這種時序圖很有助於理解，想要嚴謹的童鞋還是要看Lamport老爺子的[3]。

混合狀態機（Hybrid state machine）

tsan的實現包含了全局狀態（global states）和內存ID狀態（per-ID state）。

全局狀態即tsan的事件隊列 $langle e angle$ 。tsan可以通過該隊列推出各線程的鎖集合等信息。

內存ID狀態由兩個片段集合構成：寫片段集合 $SS_{Wr}$ 和讀片段集合 $SS_{Rd}$ 。 $SS_{Wr}$ 由所有Write這一內存ID的事件構成。 $SS_{Rd}$ 則更加複雜一點，它包含了所有1）滿足條件A，且2）Read這一內存ID的事件。

條件A： $forall S_r in SS_{Rd}, S_w in SS_{Wd}: S_r preceq S_w$ 。

翻譯成人話就是，對於 $SS_{Rd}$ 中的任意一個片段 $S_r$ ，它要麼就happens-after $SS_{Wr}$ 中的所有片段，要麼就跟 $SS_{Wr}$ 中的所有片段都不可比較。

此外需要注意的是，內存ID狀態的 $SS_{Wr}$ 和 $SS_{Rd}$ 都需要滿足片段集合本身的不變數。

條件A並不是很直觀，它是怎麼得到的？很抱歉，我並沒有參悟到...個人理解這只是由於演算法本身得出的一個人為約束，歡迎各位大神打臉 ~_~

演算法

講到這裡，我們可以看看演算法了。tsan的偽代碼非常簡略，總共只有半頁。

處理每個內存操作事件的函數

註： $IsWrite$ 指該內存操作事件是否是Write， $Tid$ 是線程， $ID$ 是內存地址， $riangleright$ 是注釋。

這個函數總結成一句話就是：在這個內存事件發生後維護 $SS_{Wr}$ 和 $SS_{Rd}$ ，使其在內存操作事件發生後仍滿足所有不變數約束，然後檢測data race。

我們分析下 $IsWrite = True$ 時的情況，也就是Line 6和Line 7。

先看Line 7： $SS_{Wr} gets { s: s in SS_{Wr} land s preceq Seg }^1 cup { Seg }^2$ 。因為 $Seg$ 包含了Write這個ID的事件，根據定義，它需要在寫片段集合 $SS_{Wr}$ 中，即 $^2$ 。而 $^1$ 則是為了維護 $SS_{Wr}$ 作為片段集合本身的不變數。

還有個問題。執行完Line 7後，雖然 $forall s in SS_{Wr}: s preceq Seg$ ，但是是否存在 $exists s in SS_{Wr}: Seg prec s$ 的可能呢？

通過歸納法，我們發現這是不可能的。記Line 7執行後的寫片段集合為 $SS_{Wr}$ ，執行前的仍為 $SS_{Wr}$ ，我們通過假設 $exists s in SS_{Wr}: Seg prec s$ 推出矛盾。首先如果 $Seg in SS_{Wr}$ ，那麼因為 $SS_{Wr}$ 本身的不變數，矛盾時顯然的。否則當 $Seg otin SS_{Wr}$ 時， $SS_{Wr}$ 中任意一個片段都已經被tsan觀測到了，它們均發生在了 $Seg$ 之前，因此假設矛盾。

Line 6的分析則完全相同。

而 $IsWrite = False$ 時，Line 9對 $SS_{Rd}$ 的更新也與Line 7同理。但在這種情況下， $SS_{Wr}$ 並沒有被更改，因此 $Seg$ 跟 $SS_{Wr}$ 中的所有片段是可能構成happens-after關係的。

如果覺得細節太多，只需要記住 $SS_{Wr}$ 和 $SS_{Rd}$ 的定義和意義：它們記錄了針對某個內存ID的所有讀寫操作。由於每個集合內的片段相互間都不存在順序關係（推論是它們都分布在不同的線程上），這構成了並行執行的必要條件，因此可能造成data race。

再來看檢查data race的演算法。

檢查data race的演算法

其實這個函數完全就是按照文中對data race的定義做的檢查。

Line 3的for循環遍歷 $SS_{Wr}$ 中的每個片段 $W_1 gets SS_{Wr}[i]$ ，其所在線程的鎖集合為 $LS_1$ 。Line 6-12檢查可能和 $W_1$ 產生data race的寫操作，Line 13 - 17檢查讀操作。

我們以稍微複雜點的讀-寫操作檢查為例，分析一下它是如何運行的。

針對當前的寫片段 $W_1$ ，Line 14循環遍歷所有的讀片段 $R in SS_{Rd}$ ，其所在線程的鎖集合為 $LS_R$ 。Line 16的第二個條件 $LS_1 cap LS_R = emptyset$ 我們已經知道了，查兩個操作所在線程持有的鎖是否有重合。那麼第一個條件 $W_1 preceq R$ 呢？

回憶一下條件A：

對於 $SS_{Rd}$ 中的任意片段 $S_r$ ，它要麼就happens-after $SS_{Wr}$ 中的所有片段，要麼就跟 $SS_{Wr}$ 中的所有片段都不可比較。

而兩個事件滿足data race的必要條件就是不可比較，因此第一個條件就是過濾掉那些跟 $W_1$ 可比較（構成happens-after關係）的讀片段。

當這兩個條件都滿足後，我們發現 $(W_1 preceq R) land (R preceq W_1) land (LS(R) cap LS(W_1) = emptyset)$ ，因此這兩個事件會造成data race。

說來真是略坑，[1]到這裡就算把核心理論講完了，然而有個很重要的問題它並沒有提及：如何判斷 $prec$ 關係？

再讀一遍時，我在相關工作的某一行里發現了[2]。讓我們看看[2]是如何講清這件事的。

向量時鐘（Vector Clock）

[2]的一大貢獻就是說明白了如何通過向量時鐘驗證 $prec$ 。

先來介紹下向量時鐘（[4]）的概念：每個線程T都維護一個邏輯時鐘的向量，通過系統中線程的Tid進行索引，因此每個線程的向量時鐘長度都是執行期間的線程總數。記 $V_i(T)$ 為線程T在事件 $e_i$ 發生後的向量時鐘。直觀上的理解是，線程T的向量時鐘里T位置記錄的是T最近一次對T產生影響時的邏輯時間戳。這裡T可以等於T。

此外，當線程T通過通道（內存ID為C）執行一個Signal事件時，我們將線程T當時的向量時鐘賦給這一事件，記為 $V(C)$ 。

向量時鐘是怎麼計算的呢？

$V_0(T)(T) = ig( ext{if } T = T ext{ then } 1 ext{ else } 0ig)$
$V_i(T)(T) = V_{i - 1}(T)(T) + 1, e_{i - 1} = ext{Signal}_T(C)$
$V_i(T)(T) = max(V_{i - 1}(T)(T), V(C)(T)), e_i = ext{Wait}_T(C) land T e T$
$V_i(T)(T) = V_{i - 1}(T)(T), ext{otherwise}$ ，注意這裡 $t$ 可以等於 $t$
$V(C) = V_i(T)$

線程自己肯定是最了解自己的，因此在產生一個可以影響外部的事件（Signal）後，自己的時鐘 $V(T)(T)$ 總是率先增加一格，即規則2。而當某個線程T收到另一個線程T產生的事件時（Wait），T所能知道的T的最新狀態就是T產生該事件的時鐘，因此有了規則3和5。

對於兩個內存操作事件 $e_i, e_j$ ，記其所發生的線程分別為 $T_i, T_j$ ，那麼 $e_i prec e_j$ 的充分必要條件是 $ig((i < j) land (V_j(T_j)(T_i) ge V_i(T_i)(T_i))ig)$ 。

這個稍微想一下還是很好理解的：當事件 $e_j$ 發生在線程 $T_j$ 時，如果線程 $T_j$ 的向量時鐘里 $T_i$ 對應的時刻大於等於線程 $T_i$ 自己在 $e_i$ 發生時的值，那說明在 $e_i$ 到 $e_j$ 期間，線程 $T_j$ 一定收到過 $T_i$ 至少在 $i$ 時或以後發來的消息。因此 $T_j$ 上的某事件一定跟 $T_i$ 上的構成了至少一條happens-before弧，或通過 $prec$ 的傳遞性構成了happens-before關係。

我們再通過圖1的栗子感受一下。這裡我們分析下 $S_1, S_3$ 的關係。

初始化時根據規則1，兩個線程的向量時鐘分別為：

| V(T1) | V(T2) |-----------------------------------| T1 | T2 | T1 | T2 |-----------------------------------| 1 | 0 | 0 | 1 |

設事件 $S1$ 在全局隊列中的編號為 $i$ ，當 $S1$ 發生時，由於並沒有任何條件匹配，根據規則4，兩線程的向量時鐘均沒有變化。這裡注意的是， $S1$ 並不一定是隊列中的第一個事件， $S2$ 也可以。

當線程T1中的Signal事件發生時，兩線程的時鐘向量仍沒有變化。此外，由於它跟 $S1$ 在同一線程，其編號一定大於 $i$ 。而根據5，該事件的向量時鐘為（假設C為Signal事件所用的通道）

| V(C) | # V(C) = V(1)-----------------| T1 | T2 |-----------------| 1 | 0 |

當線程T1中的Signal事件發生後的下一個事件 $e_j$ 發生時，由定義可知， $j > ext{IndexOf(Signal}_{T1}(C)) > i$ 。根據規則2，我們此時需要改變線程T1的向量時鐘：

| V(T1) | V(T2) |-----------------------------------| T1 | T2 | T1 | T2 |-----------------------------------| 2 | 0 | ? | 1 |

需要注意的是：

這裡說的事件 $e_j$ 是在全局隊列中，而非單是線程1的，因此 $e_j$ 可能是 $S4$ ，線程2的Wait事件甚至 $S2$ 。
由於上一點，我們並不能得知線程T2的向量時鐘。但是我們知道 $V_j(T2)(T2)$ 不發生變化（線程T2並沒有任何Signal事件），而 $(V_j(T2)(T1) ge 0) land (V_{j - 1}(T2)(T1) = 0)$ 。
在這之後，線程T1的向量時鐘就不會再改變了（線程T1上不再有Signal或Wait事件了）。

$e_j$ 只可能有兩種情況： $e_j = ext{Wait}_{T2}(C)$ 或者 $e_j e ext{Wait}_{T2}(C)$ （廢話 -_-#）

設 $ext{Wait}_{T2}(C)$ 事件發生在隊列中的第 $k$ 個位置，可知 $k ge j$ 。當其發生時，根據規則3， $V_k(T2)(T1) = max (V_{k - 1}(T2)(T1), V(C)(1)) = max(0, 1) = 1$

| V(T1) | V(T2) |-----------------------------------| T1 | T2 | T1 | T2 |-----------------------------------| 2 | 0 | 1 | 1 |

此後線程T2的向量時鐘也不會再變了。

因為 $(k ge j > i) land ig( V_k(T2)(T1) = V_k(T1)(T1) ig)$ ，所以 $S1 prec S3$ 。

有興趣的童鞋可以選一些其他的事件對驗證 $prec$ （或者 $preceq$ ）。

擴展

tsan的核心思路到這裡就全部結束了，但是它還有一個值得注意的擴展。

[1] Section 4.4.1中擴充了對happens-before弧的定義，並稱之為extended happens-before arc。原文列了三個新的關係，但由於我們對鎖事件的簡化，這三種關係退化成一種。即當事件 $X = ext{Unlock}_{T1}(L)$ 先於 $Y = ext{Lock}_{T2}(L)$ 出現在事件隊列中時， $(X, Y)$ 也構成一條happens-before弧。

因為鎖事件發生的不確定性，一個直接影響就是，data race的檢測結果將取決於執行時事件發生的順序 $langle e angle$ ，參加下圖：

第一次執行（Run1）時，線程1的Unlock和線程2的Lock構成了extended happens-before弧；而第二次執行（Run2）時，線程2的Unlock和線程1的Lock構成了extended happens-before弧

這樣做的優點是降低了data race的誤診率（false positive），代價是增加了data race彙報的不確定性與漏診率——有時候真正的data race，可能會因為某次執行時鎖的順序而被遺漏。

如果這麼說太抽象，我們看一下原文[1]中的一個栗子

// Thread 1 | // Thread 2obj->UpdateMe(); // a | mu.Lock();mu.Lock(); | bool f = flag;flag = true; | mu.Unlock();mu.Unlock(); | if (f) { obj->UpdateMe(); } // b

如果沒有擴展happens-before弧的定義的話，這段代碼每次執行時（不論flag初始值是什麼），tsan都會彙報事件a和b對obj的操作會導致data race。

而擴展了happens-before弧後，我們需要分情況討論了。

假設初始條件為flag = false。如果線程1先拿到了鎖，由於鎖互斥性，事件a會發生在事件b之前；否則線程2先拿到鎖的話，f = false ，事件b並不發生。無論哪種情況，obj都不可能同時被兩個線程修改。因此這種初始情況下，程序並不存在data race。

初始條件：flag = false。左：線程1先拿到鎖；右：線程2先拿到鎖

而tsan會如何處理呢？

可以看出，tsan要麼認為 $a prec b$ （如果線程1先拿到了鎖）；要麼不存在事件b。兩種情況下，tsan都不會報data race。因此tsan的誤診率降低了。

而若初始條件為flag = true呢？仍然按照誰先拿到的鎖分情況討論。如果是線程1，由於互斥性，a一定會發生在b之前。而若是線程2先拿到的話，這次f = true，因此事件a和b有可能並行發生，造成data race。因此在這種初始情況下，程序本身是存在data race的！

初始條件：flag = true。左：線程1先拿到鎖；右：線程2先拿到鎖

然而，tsan在這種情況下只有在線程2先拿到鎖的執行過程中會彙報有data race，因此tsan的不確定性上升了。不僅如此，它在線程1先拿到鎖的執行中還會漏診。

實際應用中，是否選擇啟用擴展的happens-before關係要根據具體情況而定。tsan絕非銀彈。

總結

到這裡，我們自己都可以總結出tsan大致是如何工作的了。

對於tsan中的每一類事件，當其發生時，我們將它添加到事件隊列中。所需記錄的信息有：（事件類型、線程、內存地址），即 $ext{EventType}_{Tid}(ID)$ 。
對於 $ext{Signal}, ext{Wait}$ 事件，我們需要更所在線程的向量時鐘。
對於 $ext{Lock}, ext{Unlock}$ 事件，我們需要更新所在線程的鎖集合。如果擴展了happens-before弧的定義，我們也需要更新所在線程的向量時鐘。
對於 $ext{Read}, ext{Write}$ 事件，每次發生後我們需要通過HandleReadOrWriteEvent()更新其內存ID狀態 $(SS_{Wr}, SS_{Rd})$ ，並檢測data race。為了方便判斷 $prec$ 關係，我們還需要將該事件發生時的 $V(T)(T)$ 記錄下來。

向量時鐘這一概念又是從Lamport老爺子的[3]來的。忽然覺得，如果不是 @丁凱那篇總結得很好，我這篇才應該叫《事件和時間：Lamport Clock讀後感以及一點微小的工作》...

另外，對TLA+有所了解的童鞋應該很容易跟上面各種邏輯關係聯繫起來。

TLA+是誰發明的？Lamport老爺子...

Lamport老爺子在哪？微軟...

所以雲計算哪家強？跟我念：A! z! u! r...

啊不對，Google Cloud...

老闆你冷靜點，你聽我說，先把刀放下...

本文僅代表作者個人觀點。

參考文獻

[1] Serebryany, K. and Iskhodzhanov, T., 2009, December. ThreadSanitizer: data race detection in practice. InProceedings of the Workshop on Binary Instrumentation and Applications(pp. 62-71). ACM.

[2] OCallahan, R. and Choi, J.D., 2003, June. Hybrid dynamic data race detection. InAcm Sigplan Notices(Vol. 38, No. 10, pp. 167-178). ACM.

[3] Lamport, L., 1978. Time, clocks, and the ordering of events in a distributed system.Communications of the ACM,21(7), pp.558-565.

[4] Mattern, F., 1989. Virtual time and global states of distributed systems.Parallel and Distributed Algorithms,1(23), pp.215-226.