Linux 核心專題: Futex 驗證和評估

執行人: LindaTing0106
專題解說影片

Reviewed by kevinzxc1217

為什麼 spin/promela 可以確保模型驗證出來一定無誤呢？

其將會檢查模型的所有可能出現的狀態，確保所有可能性都被驗證過。

Reviewed by stevendd543

針對 pthread 和 futex 效能比較中可以發現 futex 雖然速度較快，但是他的變化速率卻是極大的原因是什麼？這樣看起來如果超過一定數字就會突破 pthread 的值。

針對 pthread 和 futex 效能圖比較中，其中 xy 軸並不代表其的變化速率，由左至右 x 軸表達效果較好的實驗，故應該是說在較差的實驗結果中， futex 有機會與 pthread 效能相近。

Reviewed by kkkkk1109

在比較效能時我注意到，其實可以直接嘗試將 mutex->state 改為 lock ，可以不需要 在 經過讀取此步驟。

錯字更正 再

任務簡介

探討 mutex lock 的實作手法、進行驗證，和分析其效能表現。

TODO: 閱讀 並行程式設計: 實作輕量級的 Mutex Lock

紀錄你的認知問題，並重現實驗

使用行之有年的翻譯詞彙，務必使用本課程教材規範的術語。

論文提到早期並行程式在運行時，為了避免執行緒在 critical section 發生競爭，當執行緒進入 critical section 時有兩種處理方式，一種為每次都觸發系統呼叫，交給核心檢查是否有競爭發生，但這會造成不必要的成本花費。
另一種方式為使用 spinlock 將不能進入 critical section 的執行緒鎖住，但此舉造成 CPU 資源無法釋放，且在多核系統上需要另做處理。

Futex 的誕生，使得執行緒在使用者空間上就可以檢查是否有競爭發生，如果有競爭發生再透過核心去處理，減少不必要的成本。

在下面將重現幾個此篇教材中出現的例子。

本論文著重在 model checking，但為何你不探討？

在此將範例給予的 mutex_lock 和 mutex_unlock 使用 Spin/Promela 進行驗證。

commit e5fcc37

輸入以下命令

$ spin -a mutex.pml && gcc -o pan pan.c
$ ./pan -D | dot -Tps | ps2pdf - pan.pdf

產生此圖

spin -DNUM_THREADS=3 -search -ltl safe_cs -m100000 -b mutex.pml
ltl safe_cs: [] ((num_threads_in_cs<=1))
warning: only one claim defined, -N ignored
warning: never claim + accept labels requires -a flag to fully verify

(Spin Version 6.5.2 -- 15 February 2024)
        + Partial Order Reduction

Full statespace search for:
        never claim             + (safe_cs)
        assertion violations    + (if within scope of claim)
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      - (disabled by never claim)

State-vector 48 byte, depth reached 73157, errors: 0
   328077 states, stored
   234728 states, matched
   562805 transitions (= stored+matched)
   348957 atomic steps
hash conflicts:      1007 (resolved)

Stats on memory usage (in Megabytes):
   23.779       equivalent memory usage for states (stored*(State-vector + overhead))
   17.921       actual memory usage for states (compression: 75.37%)
                state-vector as stored = 29 byte + 28 byte overhead
  128.000       memory used for hash table (-w24)
    5.341       memory used for DFS stack (-m100000)
  152.091       total actual memory usage


unreached in proctype Thread
        (0 of 113 states)
unreached in claim safe_cs
        _spin_nvr.tmp:8, state 10, "-end-"
        (1 of 10 states)

pan: elapsed time 0.13 seconds
pan: rate 2523669.2 states/second

Example

避免父權主義的遺毒，本文將 parent (generation) 翻譯為「親代」，而非「父代」或「母代」，不僅更中性，也符合英文原意。若寫作「父」，則隱含「母」的存在，但以二元樹來說，沒有這樣成對關連性。若用「上代」會造成更多的混淆，在漢語中，「上一代」沒有明確的血緣關係 (例如「炎黃子孫」與其說是血緣關係，不如說是傾向文化認同)，但「親」的本意就是指名血緣和姻親關係。

延伸閱讀: 「新中國」和「中華民族」—— 梁啟超悔之莫及的發明

在 main.c 的程式中會先建立

$n_0$ ~

$n_{15}$ ，其中除了

$n_0$ 以外，其餘

$n_i$ 的父代 親代都為

$n_{i-1}$ ，且全部節點都共享資料 clock 。

在建立執行緒時，因為一開始的 clock->tick 為 0 所以所有執行緒會被鎖在 clock_wait(self->clock, 1) 直到主執行緒執行完 clock_tick(&clock) 將 tick 設為 1 。

for (int i = 1; clock_wait(self->clock, i); ++i)

透過 node_wait(self->parent) ，除了

$n_0$ 以外的節點都要等待自己親代的 ready 為 1 才能開始執行操作。

操作分為兩類，每個節點在 i 為基數時，執行 clock_tick(self->clock) ，在偶數時，執行 node_signal(self) ，將自己的 ready 設為 1 。

而最外層的 clock_wait(&clock, 1 << N_NODES) ，控制主執行緒在 tick 等於 1 << N_NODES 之前都持續等待。直到 tick 等於 1 << N_NODES 後， clock_stop 將 tick 設為 -1 ，並使其他執行緒脫離迴圈。

perf-test

在 main.c 中，使用 common 當作共享變數。並建立

$ct{x}_0$ ~

$ct{x}_3$ 。將所有執行緒建立完之前，主執行緒會先將所有的執行緒的 start_mutex 都鎖起來，並等待 ready_count 的數量等於執行緒的數量，防止有的執行緒先往下執行。

在

$ct{x}_i$ 開始執行前，要先確保

$ct{x}_{i+1}$ 沒有被鎖住。其行為模式為，將

$ct{x}_{i+1}$ 上鎖後，對

$ct{x}_i$ 進行解鎖，因此最先執行的會是

$ct{x}_3$，且執行順序為

$ct{x}_3$ ->

$ct{x}_2$ ->

$ct{x}_1$ ->

$ct{x}_0$ ->

$ct{x}_3$ -> …。 整個過程執行 50 次後會計算整體執行時間。

下圖分別為使用 pthead 與 futex 的執行時間由低排至高，可以看出使用 futex 的執行時間必定小於 pthead。

而在此程式碼中，我們可以看到一開始先讀取 mutex->state 中的值，並且將其寫入 state 中，此處檢查 state 是否處在 lock 中，如果其處在 lock 中，則回傳 false 。

如果其不為 lock 則嘗試將 mutex->state 改為 lock ，如果在嘗試的過程中已被其他執行緒鎖住，則也回傳 false ，反之則成功上鎖，並且回傳 true 。

在比較效能時我注意到，其實可以直接嘗試將 mutex->state 改為 lock ，可以不需要在經過讀取此步驟。

static bool mutex_trylock_default(mutex_t *mutex)
{
    int state = load(&mutex->state, relaxed);
    if (state & MUTEX_LOCKED)
        return false;

    state = fetch_or(&mutex->state, MUTEX_LOCKED, relaxed);
    if (state & MUTEX_LOCKED)
        return false;

    thread_fence(&mutex->state, acquire);
    return true;
}

更改過後的程式碼為

static bool mutex_trylock_default(mutex_t *mutex)
{
    int state = fetch_or(&mutex->state, MUTEX_LOCKED, relaxed);
    if (state)
        return false;

    thread_fence(&mutex->state, acquire);
    return true;
}

而效能比較圖為

明顯可以看到整體效能更佳。從兩張效能比較圖中可以發現，未經過讀取這一步驟的效能圖中，futex 在效能排名第 80 的測試中花費時間才開始顯著增加，而在原先的效能圖中，futex 在效能排名第 50 的測試中花費時間就已經開始上升。因此，這樣的改進可以有效提高 mutex->state 在 trylock 成功上鎖的比例。

pi_test

在其中加入了執行緒優先順序的考量，根據給予的程式碼，我們可以發現如果沒有根據執行緒的優先性去對其進行調整的話，很有可能會發生 priority inversion ，在程式碼中，就是因為低優先序的執行緒會先將 lock 鎖住，而中優先序的執行緒則是會將 CPU 霸佔住，而此時高優先序的執行緒則因為低優先序的執行序取得不了 CPU ，無法將 lock 釋放掉，反而不是最先被執行完的執行緒，從而導致 priority inversion 。

原文有提到若使用預設的 mutex 會無法修正此問題，導致高優先序的執行續會在中優先序的後面才完成。因此並不會有 h 印出。

為了解決此問題，如果在 mutex_trylock_pi 中，嘗試取得 lock 失敗的話，便使用 FUTEX_LOCK_PI2 核心操作來處理 priority inversion 問題。

根據 pi-futex 所述，在執行緒嘗試鎖定 mutex 時，會先把 mutex 的值從 0 設定為執行緒的 tid 。如果這個操作失敗，表示互斥鎖已經被其他執行緒持有。

因為在 fast-path 失敗，因此呼叫 FUTEX_LOCK_PI 進入核心處理。核心會檢查這個 mutex 是否已經有等待佇列。沒有的話核心會建立一個。接著核心會尋找目前持有這個 mutex 的執行緒。並為此 mutex 附加一個 rt-mutex ，接著將 mutex 的值設定為 FUTEX_WAITERS | TID 。

接著目前的執行緒會嘗試鎖定 rt-mutex，並且開始等待。如果持有 mutex 的執行緒的優先權低於等待執行緒的優先權，核心會將持有執行緒的優先權提升到等待執行緒的優先權。則此時由於此執行緒的優先權提高，則其可以使用 CPU 並且釋放 Mutex 。當等待執行緒被喚醒，執行緒獲得 rt-mutex 的鎖定。核心會將 mutex 的值更新為目前執行緒的 tid ，表示目前執行緒持有了這個 mutex 。

也因此使用 mutex-pi 後，即可以解決此 priority inversion 的問題。

修正

在描述 futex_requeue 的部分，提到

該操作會喚醒最多 limit 個等待者，但和 wait 不同的地方是，若 futex 中所有的等待者超過 limit 個，則所有的等待者皆會被喚醒並改在 other 這個 futex word 對應的 wait queue 中等待，函式中的 INT_MAX 表示可以從 futex 移到 other 的最大數量。

上述 但和 wait 不同的地方是 應該改為 和 walk 不同的地方是 。

TODO: 閱讀 Model Checking Futexes 和重現實驗

如何以形式化驗證確認 Linux futex 的行為符合預期？model checking 又如何找出真實世界的並行問題？
使用 SPIN/Promela 進行驗證
重現實驗: https://github.com/mc-imperial/modelcheckingfutexes 重現實驗 (原本用 C++)

摘要

futex 旨在找出 semaphores 和 spinlocks 之間的平衡， semaphores 會導致系統就算在沒有競爭的情況下依然需要透過系統呼叫，而 spinlocks 在有競爭的情況下可能導致 CPU 使用率忙碌。

此篇論文中使用 Promela 語言與 Spin 模型檢查來檢驗 futex-based mutex 和 condvar 的正確性。其中使用 Spin 可以產生反例，故我們可以看到是怎麼樣的執行順序導致其產生錯誤。

Futex System Call Variants

typedef Futex {
byte word; // Futex word
bool wait[NUM_THREADS]; // Wait list: array of bool indexed by thread IDs,
// thread T is waiting iff wait[T] is true
byte num_waiting; // Number of threads currently waiting
}

Futex 做為一個全域變數，所有的執行緒都可以使用他。

其中透過 wait[tid] 可以得知每個執行緒是否進入等待狀態。

num_waiting 則是顯示目前正在等待的執行緒數量。

long syscall(SYS_futex,
 uint32_t *addr, // pointer to the futex word
 int futex_op, // operation: FUTEX_WAIT, FUTEX_WAKE, ...
 uint32_t val, // plain value argument
 ...); // extra arguments for other operations

• FUTEX_WAIT ：當 addr 所指向的 futex word 與 val 相同時，將此執行緒進入睡眠。以下操作為不可分割並且固定順序的：讀取 futex word 值、與 val 進行比較、 suspend 執行緒。
• FUTEX_WAKE ：喚醒 addr 所指定的 futex 。

inline futex_wait(futex, val) {
 if
 :: d_step {
 futex.word == val ->
 printf("T%d futex_wait, value match: %d; sleep\n",
 _pid, futex.word);
 assert(!futex.wait[_pid]); // The thread must not be sleeping already
 futex.wait[_pid] = true;
 futex.num_waiting++;
 }
 d_step { !futex.wait[_pid] -> printf("T%d has woken\n", _pid); }
 :: d_step {
 else -> printf("T%d futex_wait, value mismatch: %d vs. %d; do not sleep\n",
 _pid, futex.word, val);
 }
 fi
 }

FUTEX_WAIT 中的實作使用 d_step 的方式而不是 atomic ，這是由於 FUTEX_WAIT 具有確定性，也就是說在初始情況一樣的條件下，每次的輸出必定相同。

其中每一段 d_step 的操作都是不可分割的。

此段程式碼表示當 futex.word 與 val 相等時，將此執行緒設為等待中，如果 !futex.wait[_pid] 則表示其已經脫離等待，而如果 futex.word 和 val 不相等，則不會變動執行緒。

inline futex_wake(futex, num_to_wake) {
 atomic {
 assert(!futex.wait[_pid]); // The waker must not be asleep
 byte num_woken = 0;
 do
 :: num_woken == num_to_wake || futex.num_waiting == 0 ->
 break
 :: else ->
 if
 :: futex.wait[0] -> futex.wait[0] = false; printf("T%d wakes T0\n", _pid)
 :: futex.wait[1] -> futex.wait[1] = false; printf("T%d wakes T1\n", _pid)
 #if NUM_THREADS > 2
 :: futex.wait[2] -> futex.wait[2] = false; printf("T%d wakes T2\n", _pid)
 #endif
 #if NUM_THREADS > 3
 :: futex.wait[3] -> futex.wait[3] = false; printf("T%d wakes T3\n", _pid)
 #endif
 #if NUM_THREADS > 4
 :: futex.wait[4] -> futex.wait[4] = false; printf("T%d wakes T4\n", _pid)
 #endif
 #if NUM_THREADS > 5
 #error "NUM_THREADS > 5, add more if branches in futex_wake"
 #endif
 fi
 futex.num_waiting--;
 num_woken++;
 od
 printf("T%d woke up %d thread(s)\n", _pid, num_woken);
 num_woken = 0; // Reset to avoid state space explosion
 }
}

FUTEX_WAKE 使用 atomic ，是由於此段操作為非確定性，不是每次執行的時候，都可以確定是哪一個執行緒先被釋放。

assert(!futex.wait[_pid]) 說明要做喚醒的動作的執行緒不能是在等待中的。

此段程式碼中使用 num_woken 來計算已經 wake 了幾個執行緒，一直到 num_woken 等於 num_to_wake ，則跳出 FUTEX_WAKE 。

Atomic Operations

Atomic compare-and-exchange：

inline cmpxchg(location, expected, desired, result) { d_step {
result = location; location = (location == expected -> desired : location)
}}

先將 location 保留在回傳值中，再來根據 location 等不等於預期值，來決定將其更變為何，如 location 等於預期值，則將其賦予為 desired ，如不等於，則其維持不變。

Atomic fetch-and-increment：

#define MAX_BYTE_VALUE (NUM_THREADS + 1)
#define inc(a) (a == MAX_BYTE_VALUE -> 0 : a + 1)
inline fetch_inc(location, result) {
    d_step { 
        result = location;
        location = inc(location); 
    }
}

利用 inc(a) 處理溢出。

Atomic fetch-and-decrease：

和 Atomic fetch-and-increment 使用相同的原理撰寫。

#define dec(a) (a == 0 -> MAX_BYTE_VALUE : a - 1)
inline fetch_dec(location, result) {
    d_step {
        result = location;
        location = dec(location);
    }
}

注意用語：

• atomic 不翻譯為漢語，參見: https://hackmd.io/@sysprog/concurrency-atomics

明明有課程教材不看，捨近求遠看一堆品質低劣的簡體中文材料，這樣只會事倍功半。

這些函式確保能夠在 Promela 中模擬 C/C++ 的 atomic 操作，並處理溢位和下溢情況，從而達成與實際系統行為一致的模擬。

mutex verification

闡述更多關於 mutex 驗證的手法，注意論文的說法。

byte num_threads_in_cs; // Number of threads in the critical section (CS)

active [NUM_THREADS] proctype Thread() {
do
:: lock();
num_threads_in_cs++;
num_threads_in_cs--;
unlock();
:: printf("T%d is done\n", _pid) -> break
od
}

ltl safe_cs { [](num_threads_in_cs <= 1) } // Never more than one thread in CS

根據 Promela Reference – active(2) 我們可以瞭解到初始程式會從 active 處開始執行，且每個程式至少需要有一個 active 。

而 [NUM_THREADS] 是宣告有幾個執行緒執行以下程式，如果 NUM_THREADS 的數字大於 255 ，則 Spin 發出警告，並僅建立前 255 個執行緒。

其中每個執行緒都會利用自訂的函式來鎖定 mutex 和解鎖 mutex ，全域變數 num_threads_in_cs 預設為 0，用於記錄執行緒進入和離開臨界區的數量。

利用此種方式我們檢驗兩件事情。

• 不會有執行緒還處在等待佇列期間，程式就被結束掉。此為 Spin 檢查中自帶。
• 利用 ltl safe_cs { [](num_threads_in_cs <= 1) } 來確認 critical section 中是否有超過 1 個執行緒。

linear temporal logic (LTL) 是 model checking 的重要概念，理解其作用並回顧上述對 Futex 行為的制約。

linear temporal logic (LTL)

linear temporal logic 的公式描述了特定條件在不斷執行的行為下都為真的集合，也就是說，如果一個程式碼中的所有行為都在此集合中，則它滿足該性質。

使用 LaTeX 符號，參見 List of logic symbols

其中有一些驗證寫法

• $[]p$ ： 從此一直 p（Henceforth p）
• $<>p$ ： 最終 p（Eventually p）
• p Until q ： q 在未來的某個時刻成立，並且 p 至少持續到第一次 q 成立
• p Awaits q ： p 一直成立，或是 p Until q
• $()p$ ： p 在下一個時間點成立

在論文中我們使用 ltl safe_cs { [](num_threads_in_cs <= 1) } ，則我們這裡的 p 表示為 num_threads_in_cs 的數量不應該超過 1 ，也等同於在 critical section 中執行緒的數量不應該超過 1 ，則 []p 應該表示為在程式運行開始後，就不應該有超過 1 個執行緒存在於 critical section 中。

而模型驗證的方法為 ltl safe_cs { [](num_threads_in_cs <= 1) } 中的 p 被視為模型必須滿足的性質。 Spin 將嘗試否定該公式以查找反例。

補充 model checking 流程，以及論文如何驗證 Futex 的圖例。

錯誤例子 Futex-based Mutex

class Mutex {
public:
Mutex() : futex_word(0) {}
void lock() {
    uint32_t old_value;
    while ((old_value = futex_word.fetch_add(1)) != 0)
        futex_wait(&futex_word, old_value + 1);
}
void unlock() {
    futex_word.store(0);
    futex_wake(&futex_word, 1);
}

private:
atomic<uint32_t> futex_word;
};

若 NUM_THREADS 數量為 3 。

設目前 futex_word 為 0 ， Mutex 還沒被鎖上，則此時

$t_0$ 進到 lock 時， old_value 會先保存 futex_word 原始值，接著 futex_word 會加 1 ，故此時 Mutex 被上鎖。

則現在當 futex_word 為 1 ，另一執行緒

$t_1$ 進入 lock ，則 old_value = 1 ，且 futex_word = 2 ，如果此時沒有其他執行緒進入 lock ，則 old_value + 1 == futex_word 故此執行緒進入 futex_wait 等待呼叫。

若其他執行緒

$t_2$ 進入 lock 則此時其 old_value = 2 ， futex_word = 3 ，則由於 old_value == 1 且 futex_word == 3此時

$t_1$ 無法進入 futex_wait。

則當執行緒無法進入 futex_wait 的情況一直持續發生，將會造成 futex_word 溢出後回到 0 ，而其他執行緒此時以為可以將 Mutex 上鎖的情況發生。

若以上狀況發生，則 critical section 中會有超過一個的執行緒，此時違反 Mutex 的互斥性。

這個例子演示了由於 futex_word 的值在競爭中不斷變化，執行緒之間可能會發生錯誤的同步，導致競爭失敗。且，由於 futex_word 的值在競爭時可能回到 0 ，導致了執行緒錯誤地認為它們可以鎖住 Mutex，而違反了互斥性原則。

T0 locks mutex
T1 lock fail, old_value: 1
T2 lock fail, old_value: 2
T1 futex_wait, value mismatch: 3 vs. 2; do not sleep
T1 lock fail, old_value: 3
T2 futex_wait, value mismatch: 4 vs. 3; do not sleep
T2 lock fail, old_value: 4
T1 futex_wait, value mismatch: 0 vs. 4; do not sleep
T1 locks mutex
assertion num_threads_in_cs <= 1 violated

另個情況為有執行緒不會結束。先假設

$t_0$ 一樣先將 Mutex 上鎖，且

$t_1$ 和

$t_2$ 一樣進入競爭。此時

$t_1$ old_value 為 3 且

$t_2$ old_value 為 4 ，而 futex_word 的值為 0 ，這兩個執行緒的下一步都是執行 futex_wait。

此時

$t_0$ 將 Mutex 解鎖，並使 futex_word 回到 0 。則此時

$t_1$ 呼叫 futex_wait(0, 4) 失敗，並重新嘗試上鎖，成功上鎖後又馬上進行解鎖。此時

$t_2$ 終於呼叫到 futex_wait(0, 0)，此時

$t_2$ 進入等待中，但因為其他執行緒都已經離開，

$t_2$ 部會再有被喚醒的機會。導致了有執行緒不會離開的情況發生。

T0 locks mutex
T1 lock fail, old_value: 1
T2 lock fail, old_value: 2
T1 futex_wait, value mismatch: 3 vs. 2; do not sleep
T1 lock fail, old_value: 3
T2 futex_wait, value mismatch: 4 vs. 3; do not sleep
T2 lock fail, old_value: 4
T0 unlocks mutex, futex_word: 0
T1 futex_wait, value mismatch: 0 vs. 4; do not sleep
T1 locks mutex
T1 unlocks mutex, futex_word: 0
T2 futex_wait, value mismatch: 0 vs. 0; sleep

正確的 Futex-based Mutex

class Mutex {
public:
    Mutex() : futex_word(0) {}
    void lock() {
        uint32_t old_value;
        if ((old_value = cmpxchg(futex_word, 0, 1)) != 0)
        do {
            if (old_value == 2 || cmpxchg(futex_word, 1, 2) != 0)
            futex_wait(&futex_word, 2);
        } while ((old_value = cmpxchg(futex_word, 0, 2)) != 0);
        }
    void unlock() {
        if (futex_word.fetch_sub(1) != 1) {
            futex_word.store(0);
            futex_wake(&futex_word, 1);
        }
    }
private:
    atomic<uint32_t> futex_word;  
};

在此處 futex_word 的值代表了不同的涵義，當其為 0 時，表示他並未被上鎖。
當其為 1 時，表示上鎖了，但沒有其他在等待的執行緒。
當其為 2 ，表示上鎖了，同時也還有其他在等待的執行緒。

上鎖的路徑分為快路徑和慢路徑，如果一個執行緒

$T$ 是透過 if ((old_value = cmpxchg(futex_word, 0, 1)) != 0) 將 Mutex 上鎖，則稱為快路徑。
反之，若在 while ((old_value = cmpxchg(futex_word, 0, 2)) != 0) 上鎖，則為慢路徑。

此處使用 Spin 驗證此模型的正確性。

此外也對模型進行了一些修改，其中有幾個錯誤的案例。

Bug 1: incorrect simplification

if (old_value == 2 || cmpxchg(futex_word, 1, 2) != 0)
    futex_wait(&futex_word, 2);

改為

futex_word.store(2);
futex_wait(&futex_word, 2);

最終會導致等待的執行緒不會被喚醒。
其過程如下

T0 locks mutex on fast path
T1 fails to lock mutex on fast path
T0 decrements futex word from 1 to 0
T0 is done
T1 sets futex.word to 2
T1 futex_wait, value match: 2; sleep

這是因為當

$T_0$ 將 Mutex 解鎖後，會將 futex_word 設回 0 ，若此時

$T_1$ 沒有檢查是否 Mutex 為沒上鎖的情況，則造成了明明在 Mutex 為空閒的情況下卻在等待。並且也沒有其他執行緒能夠將其喚醒。

Bug 2: incorrect cmpxchg

while ((old_value = cmpxchg(futex_word, 0, 2)) != 0)

替換為

while ((old_value = cmpxchg(futex_word, 0, 1)) != 0)

則也出現等待的執行緒沒有被喚醒的情況發生。

T0 locks mutex on fast path
T1 fails to lock mutex on fast path
T1 futex_wait, value match: 2; sleep
T2 fails to lock mutex on fast path
T2 futex_wait, value match: 2; sleep
T0 decrements futex word from 2 to 1
T0 wakes T2
T0 woke up 1 thread(s)
T0 is done
T2 has woken
T2 locks mutex on slow path
T2 decrements futex word from 1 to 0
T2 is done

CondVar verification

使用 Waiter 和 Signaller 來檢查 condvar 的正確性。

#define NUM_WAITERS (NUM_THREADS - 1)
byte num_signals_req; // Number of signals required
byte num_done; // Number of terminated waiter threads

active[NUM_WAITERS] proctype Waiter() {
    do
    :: mutex_lock() ->
        num_signals_req++;
        printf("T%d calls cv_wait()\n", _pid);
        cv_wait();
        printf("T%d returns from cv_wait()\n", _pid);
        mutex_unlock()
    :: break
    od
    num_done++;
}

該程式在執行時會先將 mutex 鎖上避免 data racing ，而後 num_signals_req 增加，表示等待 condvar 的執行緒增加，進到 cv_wait 後，需要等待 cv_wake ，最後才可將 mutex 解鎖。

而 Signaller 端相較起來稍微複雜些。

active proctype Signaller() {
    do
    :: num_signals_req > 0 -> 
        mutex_lock();
        printf("T%d must signal, num_signals_req=%d\n", _pid, num_signals_req);
        cv_signal();
        num_signals_req--;
        mutex_unlock()
    :: else ->
        if
        :: true ->
            mutex_lock();
            printf("T%d signals without need\n", _pid);
            cv_signal();
            num_signals_req = (num_signals_req > 0 -> num_signals_req - 1 : 0);
            mutex_unlock()
        :: true -> printf("T%d won’t signal until needed\n", _pid);
            if
            :: num_signals_req > 0 -> assert(num_done < NUM_WAITERS)
            :: num_done == NUM_WAITERS -> assert(num_signals_req == 0); break
            fi
        fi
    od
}

在 num_signals_req > 0 ，表示需要發送訊號，則鎖定 mutex 、發送訊號、減少 num_signals_req ，然後解鎖 mutex 。

如果沒有執行緒需要被喚醒，則會有兩種可能的情況。

• 一種是此執行緒還是會發送訊號。
• 另一種情況為，此執行緒在需要時才會發送信號，所以其會再次判斷是否有需要喚醒的執行緒。
  • 如果 num_signals_req 大於 0 但是 num_done 等於或大於 NUM_WAITERS，則表示所有等待中執行緒的已經完成，但仍然有訊號需求，這是一個錯誤狀態，因此會報告錯誤。
  • 如果 num_done == NUM_WAITERS 則表示所有執行緒都已經完成，而如果此時 num_signals_req 不為 0 也視為錯誤，如果確定都已經完成後，此執行緒也會結束。

錯誤例子 Futex-based CondVar

class CondVar {
public:
CondVar() : futex_word(0) {}
void cv_wait(mutex &m) {
m.unlock();
futex_wait(&futex_word, 0);
m.lock();
}
void cv_signal() { futex_wake(&futex_word, 1); }

private:
atomic<uint32_t> futex_word;
};

可能造成

T0 locks mutex
T0 call cv_wait(), unlock mutex
T1 call cv_signal(), futex_wake(&futex_word, 1), the signal is lost
T0 futex_wait(&futex_word, 0)
:
T0 never wake up

正確例子 Futex-based CondVar (?)

class CondVar {
public:
CondVar() : futex_word(0) {}
void cv_wait(mutex &m) {
    uint32_t old_value = futex_word;
    m.unlock();
    futex_wait(&futex_word, old_value);
    m.lock();
}
void cv_signal() {
    futex_word.fetch_add(1);
    futex_wake(&futex_word, 1);
}

private:
atomic<uint32_t> futex_word;
};

通過此種方式則可以避免在 wake 之後才成功執行 wait 。
但文中也有提到此種方式仍然有機會發生死結，當

$T_0$ 在執行完 uint32_t old_value = futex_word; 且執行 futex_wait(&futex_word, old_value); 前，若呼叫 2^32 次 cv_signal() ，其中導致 futex_word.fetch_add(1); 將 futex_word 值執行至溢出，則此時 futex_word 即等於 old_value ，故

$T_0$ 仍有機會進入等待，而導致陷入死結。

正確例子 Futex-based CondVar

在 github 中作者有另外提供此版 CondVar 並且使用 spinlock 也可以驗證其正確性。

class CondVar {
public:
  CondVar() : futex_word(0) {}
  void cv_wait(mutex &m) {
    previous.store(futex_word);
    uint32_t val = previous.load();
    m.unlock();
    futex_wait(&futex_word, val);
    m.lock();
  }
  void cv_signal() {
    uint32_t val = 1 + previous.load();
    futex_word.store(val);
    futex_wake(&futex_word, 1);
  }

private:
  atomic<uint32_t> futex_word;
  atomic<uint32_t> previous; // Additional state
};

若同樣當

$T_0$ 在執行完 uint32_t val = previous.load(); 且執行 futex_wait(&futex_word, val); 前，呼叫 2^32 次 cv_signal() ，則由於 previous 都會維持在執行 cv_wait 時 previous 的值，故不管呼叫多少次 cv_signal() 則 futex_word 的值都維持在 1 +previous ，因此不會有溢出的情況發生。

使用 Spin 檢查 mutex 正確性

在檢查 drepper_mutex1.pml 時，我們先將 num_threads 設為 3 ，來檢查是否有達到互斥性。

若經檢查後違反互斥性，則顯示執行步驟詳細情況。

T2 locks mutex
T2 unlocks mutex
T2 woke up 0 thread(s)
T1 locks mutex
T2 lock fail, old_value: 1
T2 futex_wait, value match: 2; sleep
T1 unlocks mutex
T1 wakes T2
...
T2 lock fail, old_value: 2
T0 lock fail, old_value: 3
T2 futex_wait, value mismatch: 4 vs. 3; do not sleep
T2 lock fail, old_value: 4
T0 futex_wait, value mismatch: 0 vs. 4; do not sleep
T0 locks mutex
T2 futex_wait, value mismatch: 1 vs. 0; do not sleep
T2 lock fail, old_value: 1
T1 unlocks mutex
T2 futex_wait, value mismatch: 0 vs. 2; do not sleep
T2 locks mutex

原程式 C++ 實驗結果

執行原程式 cpp/mutex_harness.cc ，發現應為錯誤的 cpp/drepper1.cc 沒有被檢測出來。

cpp/mutex_harness.cc 程式是使用 NTHREADS 個 threads ，每個 threads 應該要執行 ELEMS_PER_THREAD 次 count++; 。

則如果沒有任何的 data racing ，預想的 count 應該要為 NTHREADS * ELEMS_PER_THREAD 。

// cpp/drepper1.cc
class Mutex {
public:
  Mutex() : futex_word(0) {}
  void lock() {
    uint32_t old_value;
    while ((old_value = futex_word.fetch_add(1)) != 0)
      futex_wait(&futex_word, old_value + 1);
  }
  void unlock() {
    futex_word.store(0);
    futex_wake(&futex_word, 1);
  }

private:
  atomic<uint32_t> futex_word;
};

在上面錯誤例子中，提到當 futex_word 發生溢位時，會導致兩個以上的 thread 同時進入 critical sections ， 但在 futex_word 為 uint32_t 的情況下 thread 的數量要非常大才有可能會溢位，因此我將此處的 uint32_t 改為 char 。

在此將 NTHREADS 設為 1000 ， ELEMS_PER_THREAD 設為 1000 。

WARNING: ThreadSanitizer: data race (pid=164059)
  Write of size 4 at 0x7ffe3c269d0c by thread T37:
    #0 main::{lambda()#1}::operator()() const <null> (a.out+0x27c6) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61cde694)
    #1 void std::__invoke_impl<voidJ main::{lambda()#l}>(std::___invoke-Other, main::{lambda()#1}&&) <null> (a.out+0x35bb) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c6
lcde694)
    #2 std::__invoke_result<main::{lambda()#l}>::type std::___invoke<main::{lambda()#l}>(main::{lambda()#1}&&) <null> (a.out+0x3550) (Buildld: 81ea8faaa76185bee6e5dd9
033aa7c6c61cde694)
    #3 void std::thread::_Invoker<std::tuple<main::{lambda()#l}> >::_M_invoke<0ul>(std::_lndex_tuple<0ul>) <null> (a.out+0x34b2) (Buildld: 81ea8faaa76185bee6e5dd9033
aa7c6c61cde694)
    #4 std::thread::_Invoker<std::tuple<main::{lambda()#l}> >::operator()() <null> (a.out+0x3458) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61cde694)
    #5 std::thread::_State_impl<std::thread::_Invoker<std::tuple<main::{lambda()#l}> > >::_M_run() <null> (a.out+0x340e) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61
cde694)
    #6 <null> <null> (libstdc++.so.6+0xeabb3) (Buildld: 40b9b0dl7fdeebfb57331304da2b7f85el396ef2)

  Previous write of size 4 at 0x7ffe3c269d0c by thread T52:
    #0 main::{lambda()#1}::operator()() const <null> (a.out+0x27c6) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61cde694)
    #1 void std::__invoke_impl<voidJ main::{lambda()#l}>(std::___invoke-Other, main::{lambda()#1}&&) <null> (a.out+0x35bb) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c6
lcde694)
    #2 std::__invoke_result<main::{lambda()#l}>::type std::___invoke<main::{lambda()#l}>(main::{lambda()#1}&&) <null> (a.out+0x3550) (Buildld: 81ea8faaa76185bee6e5dd9
033aa7c6c61cde694)
    #3 void std::thread::_Invoker<std::tuple<main::{lambda()#l}> >::_M_invoke<0ul>(std::_lndex_tuple<0ul>) <null> (a.out+0x34b2) (Buildld: 81ea8faaa76185bee6e5dd9033
aa7c6c61cde694)
    #4 std::thread::_Invoker<std::tuple<main::{lambda()#l}> >::operator()() <null> (a.out+0x3458) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61cde694)
    #5 std::thread::_State_impl<std::thread::_Invoker<std::tuple<main::{lambda()#l}> > >::_M_run() <null> (a.out+0x340e) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61
cde694)
    #6 <null> <null> (libstdc++.so.6+0xeabb3) (Buildld: 40b9b0dl7fdeebfb57331304da2b7f85el396ef2)

在 ThreadSanitizer 報錯中，我們可以看出是因為兩個執行緒同時進入 critical section 中，對共享變數進行寫入，而導致 data racing 的狀況發生。

SUMMARY: ThreadSanitizer: data race (/home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/cpp/a.out+0x27c6) (Buildld: 81ea8faaa76185bee6e5dd9033aa7c6c61cde69
4) in main::{lambda()#1}::operator()() const


Final counter value is 833843; expected 1000000
ThreadSanitizer: reported 2 warnings

且 count 值與理想不同。故證實 cpp/drepper1.cc 會出現 data racing 情況。

而在執行 cpp/drepper2.cc 時則不會出現以上報錯，且 count 值確實為 1000000 。

TODO: 用 C11 futex 重寫論文範例程式碼

搭配 ThreadSanitizer 去確認行為符合預期
對照 model checking 的驗證

在此列出你以 C11 Atomics 重寫過的程式碼，亦即 GitHub repository。

commit 6cec9c3

為了驗證其正確性，將 cpp/mutex_harness.cc 編寫為 C 語言 mutex_harness.c 。

這邊比較特別的是將 atomic 操作從 C++ 轉為 C 的過程。最初 C++ 程式中預設的 memory_order 方式都為 memory_order_seq_cst 。

則繼續沿用 NTHREADS 設為 1000 ， ELEMS_PER_THREAD 設為 1000 的配置，運行程式。

WARNING: ThreadSanitizer: data race (pid=544548)

  Read of size 4 at 0x7fffffffbc08 by thread T756:

    #0 threadfunc /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness. c: 64 (mutex_harness+0xl804) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)

  Previous write of size 4 at 0x7fffffffbc08 by thread T661:

    #0 threadfunc /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:64 (mutex_harness+0xl81e) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)
  Location is stack of main thread.

  Location is global '<null>' at 0x000000000000 ([stack]+0xlec08)

  Thread T756 (tid=545323, running) created by main thread at:

    #0 pthreadcreate ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1022 (Iibtsan.so.2+0x5a267) (Buildld: 64cle8de04blla7d960abd7e45f94f3b277b7779)

    #1 main /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:75 (mutex_harness+0xl909) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)

  Thread T661 (tid=545228, running) created by main thread at:

    #0 pthreadcreate ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1022 (Iibtsan.so.2+0x5a267) (Buildld: 64cle8de04blla7d960abd7e45f94f3b277b7779)

    #1 main /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:75 (mutex_harness+0xl909) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)

SUMMARY: ThreadSanitizer: data race /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:64 in threadfunc

WARNING: ThreadSanitizer: data race (pid=544548)

  Write of size 4 at 0x7fffffffbc08 by thread T756:

    #0 threadfunc /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:64 (mutex_harness+0xl81e) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)

  Previous write of size 4 at 0x7fffffffbc08 by thread T291:

    #0 threadfunc /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:64 (mutex_harness+0xl81e) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)
  Location is stack of main thread.

  Location is global '<null>' at 0x000000000000 ([stack]+0xlec08)

  Thread T756 (tid=545323, running) created by main thread at:

    #0 pthreadcreate ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1022 (Iibtsan.so.2+0x5a267) (Buildld: 64cle8de04blla7d960abd7e45f94f3b277b7779)

    #1 main /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:75 (mutex_harness+0xl909) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)

  Thread T291 (tid=544848, running) created by main thread at:

    #0 pthreadcreate ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1022 (Iibtsan.so.2+0x5a267) (Buildld: 64cle8de04blla7d960abd7e45f94f3b277b7779)

    #1 main /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:75 (mutex_harness+0xl909) (Buildld: d2724775ab72a045b39cdl5b97419e575d6dddb6)

SUMMARY: ThreadSanitizer: data race /home/itlab/kevin/linda_linux2024/final/modelcheckingfutexes/c/mutex_harness.c:64 in threadfunc

Final counter value is 998687 ; expected 1000000
ThreadSanitizer: reported 2 warnings

可以看到在 drepper1.h 中還是存在 data racing 的問題。

而在執行 drepper2.h 時則不會出現以上報錯，且 count 值確實為 1000000 。

另外在這裡為了比較其效能，使用了 perf-test 中的檔案，並將 drepper2.h 加入進行比較。

在此得到結果，可以看到使用 drepper2.h 的 mutex 時，其表現與使用 pthread 差不多，甚至表現較差的案例需要的時間大於 pthread 。

由於作者給出了很多種 mutex 實作，在這邊我將所有檔案都拿來做比較。

由於 drepper1 的 mutex 會有 data racing ，故我們可以忽視它，在這邊可以看到除了 drepper2 中較好的實驗結果有優於其他，剩餘的 mutex 其表現都差不多。

為了找出 drepper 和範例中的 mutex 為什麼效能上會有差距，先將 drepper 中速度最快的 drepper_1 與其進行比較。

可以看到就算是運行最快的 drepper_1 在比較簡單的 case 中效能還是比範例給的差。

在此我將 drepper_1 中使用到的 memory_order 改為更加彈性的 release 和 acquire ，但整體差別還是不大。

解釋並使用其他工具 (如 Ftrace) 進行更細緻的分析。

推測應該是由於範例中的 mutex 有 try_lock 此步驟，如果今天 lock 在足夠短的時間內被釋放，所以在實驗的時候我再將範例中 mutex 中 lock 改為不經過 trylock 。

此時即可以看到範例中的 mutex 優勢在於在此程式中，執行緒可以在很快的時間內釋放 lock 導致 mutex 在 trylock 時即可以拿到 lock 。

此時換為 drepper_2 與範例比較，則可以發現調整 memory_order 後的 drepper_2 與沒有 try_lock 的範例程式效能是差不多的。

於是我將 drepper_2 再加上 trylock 的功能，使得如果其他執行緒能夠在很快速的時間內將 mutex 釋出，則可以直接透過 trylock 的方式存取 lock 。

最後我將實驗次數調整至 10000 ，可以看到調整過後的 drepper_2 和原本的 mutex 的效能是差不多 的。

工程人員要避免說「差不多」，務必使用精準詞彙。