## Linux 核心專題: Futex 驗證和評估
> 執行人: LindaTing0106
> [專題解說影片](https://youtu.be/wLut9jNjYJ0)
## 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](https://hackmd.io/@sysprog/concurrency/%2F%40sysprog%2Fconcurrency-mutex)
> 紀錄你的認知問題,並重現實驗
:::danger
使用行之有年的翻譯詞彙,務必使用本課程教材規範的術語。
:::
論文提到早期並行程式在運行時,為了避免執行緒在 critical section 發生競爭,當執行緒進入 critical section 時有兩種處理方式,一種為每次都觸發系統呼叫,交給核心檢查是否有競爭發生,但這會造成不必要的成本花費。
另一種方式為使用 spinlock 將不能進入 critical section 的執行緒鎖住,但此舉造成 CPU 資源無法釋放,且在多核系統上需要另做處理。
Futex 的誕生,使得執行緒在使用者空間上就可以檢查是否有競爭發生,如果有競爭發生再透過核心去處理,減少不必要的成本。
在下面將重現幾個此篇教材中出現的例子。
:::danger
本論文著重在 model checking,但為何你不探討?
:::
在此將範例給予的 mutex_lock 和 mutex_unlock 使用 Spin/Promela 進行驗證。
> [commit e5fcc37](https://github.com/LindaTing0106/linux2024_finalproject/commit/e5fcc37698e686d58c8b6bd0e9297f327eb5a50c)
輸入以下命令
```
$ spin -a mutex.pml && gcc -o pan pan.c
$ ./pan -D | dot -Tps | ps2pdf - pan.pdf
```
產生此圖
![image](https://hackmd.io/_uploads/S1vHglVPA.png)
```cmake
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
:::danger
避免父權主義的遺毒,本文將 parent (generation) 翻譯為「親代」,而非「父代」或「母代」,不僅更中性,也符合英文原意。若寫作「父」,則隱含「母」的存在,但以二元樹來說,沒有這樣成對關連性。若用「上代」會造成更多的混淆,在漢語中,「上一代」沒有明確的血緣關係 (例如「[炎黃子孫](https://dict.revised.moe.edu.tw/dictView.jsp?ID=155219)」與其說是血緣關係,不如說是傾向文化認同),但「[親](https://dict.concised.moe.edu.tw/dictView.jsp?ID=25345)」的本意就是指名血緣和姻親關係。
> 延伸閱讀: [「新中國」和「中華民族」—— 梁啟超悔之莫及的發明](https://www.thenewslens.com/article/122516)
:::
在 [main.c](https://github.com/sysprog21/concurrent-programs/blob/master/mutex/example/main.c) 的程式中會先建立 $n_0$ ~ $n_{15}$ ,其中除了 $n_0$ 以外,其餘 $n_i$ 的<s>父代</s> 親代都為 $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](https://github.com/sysprog21/concurrent-programs/blob/master/mutex/perf-test/main.c) 中,使用 common 當作共享變數。並建立 $ctx_0$ ~ $ctx_3$ 。將所有執行緒建立完之前,主執行緒會先將所有的執行緒的 start_mutex 都鎖起來,並等待 ready_count 的數量等於執行緒的數量,防止有的執行緒先往下執行。
在 $ctx_i$ 開始執行前,要先確保 $ctx_{i+1}$ 沒有被鎖住。其行為模式為,將 $ctx_{i+1}$ 上鎖後,對 $ctx_i$ 進行解鎖,因此最先執行的會是 $ctx_3$,且執行順序為 $ctx_3$ -> $ctx_2$ -> $ctx_1$ -> $ctx_0$ -> $ctx_3$ -> ...。 整個過程執行 50 次後會計算整體執行時間。
下圖分別為使用 pthead 與 futex 的執行時間由低排至高,可以看出使用 futex 的執行時間必定小於 pthead。
![Figure_1](https://hackmd.io/_uploads/HJRTIseER.png)
而在此程式碼中,我們可以看到一開始先讀取 mutex->state 中的值,並且將其寫入 state 中,此處檢查 state 是否處在 lock 中,如果其處在 lock 中,則回傳 false 。
如果其不為 lock 則嘗試將 mutex->state 改為 lock ,如果在嘗試的過程中已被其他執行緒鎖住,則也回傳 false ,反之則成功上鎖,並且回傳 true 。
在比較效能時我注意到,其實可以直接嘗試將 mutex->state 改為 lock ,可以不需要在經過讀取此步驟。
```c
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;
}
```
更改過後的程式碼為
```c
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;
}
```
而效能比較圖為
![ex_com_change](https://hackmd.io/_uploads/B1KkZ1dIC.png)
明顯可以看到整體效能更佳。從兩張效能比較圖中可以發現,未經過讀取這一步驟的效能圖中,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](https://docs.kernel.org/locking/pi-futex.html) 所述,在執行緒嘗試鎖定 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](https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2023/SPIN.pdf) 和重現實驗
> 如何以[形式化驗證](https://hackmd.io/@sysprog/formal-verification)確認 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
```pml
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 則是顯示目前正在等待的執行緒數量。
```c
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 。
``` pml
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 不相等,則不會變動執行緒。
```pml
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:
```pml
inline cmpxchg(location, expected, desired, result) { d_step {
result = location; location = (location == expected -> desired : location)
}}
```
先將 location 保留在回傳值中,再來根據 location 等不等於預期值,來決定將其更變為何,如 location 等於預期值,則將其賦予為 desired ,如不等於,則其維持不變。
Atomic fetch-and-increment:
```pml
#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 使用相同的原理撰寫。
```pml
#define dec(a) (a == 0 -> MAX_BYTE_VALUE : a - 1)
inline fetch_dec(location, result) {
d_step {
result = location;
location = dec(location);
}
}
```
:::danger
注意用語:
* atomic 不翻譯為漢語,參見: https://hackmd.io/@sysprog/concurrency-atomics
明明有課程教材不看,捨近求遠看一堆品質低劣的簡體中文材料,這樣只會事倍功半。
:::
這些函式確保能夠在 Promela 中模擬 C/C++ 的 atomic 操作,並處理溢位和下溢情況,從而達成與實際系統行為一致的模擬。
### mutex verification
:::danger
闡述更多關於 mutex 驗證的手法,注意論文的說法。
:::
```pml
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)](https://spinroot.com/spin/Man/active.html) 我們可以瞭解到初始程式會從 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 個執行緒。
:::danger
linear temporal logic (LTL) 是 model checking 的重要概念,理解其作用並回顧上述對 Futex 行為的制約。
:::
### linear temporal logic (LTL)
linear temporal logic 的公式描述了特定條件在不斷執行的行為下都為真的集合,也就是說,如果一個程式碼中的所有行為都在此集合中,則它滿足該性質。
:::danger
使用 LaTeX 符號,參見 [List of logic symbols](https://en.wikipedia.org/wiki/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 將嘗試否定該公式以查找反例。
:::danger
補充 model checking 流程,以及論文如何驗證 Futex 的圖例。
:::
### 錯誤例子 Futex-based Mutex
```cpp
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
```cpp
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 的正確性。
```pml
#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 端相較起來稍微複雜些。
```pml
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
```cpp
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 (?)
```cpp
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 也可以驗證其正確性。
```cpp
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](https://github.com/mc-imperial/modelcheckingfutexes/blob/main/cpp/mutex_harness.cc) ,發現應為錯誤的 [cpp/drepper1.cc](https://github.com/mc-imperial/modelcheckingfutexes/blob/main/cpp/drepper1.cc) 沒有被檢測出來。
cpp/mutex_harness.cc 程式是使用 NTHREADS 個 threads ,每個 threads 應該要執行 ELEMS_PER_THREAD 次 count++; 。
則如果沒有任何的 data racing ,預想的 count 應該要為 NTHREADS * ELEMS_PER_THREAD 。
```cpp
// 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 。
```cmake
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 的狀況發生。
```cmake
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](https://github.com/mc-imperial/modelcheckingfutexes/blob/main/cpp/drepper2.cc) 時則不會出現以上報錯,且 count 值確實為 1000000 。
## TODO: 用 C11 futex 重寫[論文範例程式碼](https://github.com/mc-imperial/modelcheckingfutexes/tree/main/cpp)
> 搭配 ThreadSanitizer 去確認行為符合預期
> 對照 model checking 的驗證
:::danger
在此列出你以 C11 Atomics 重寫過的程式碼,亦即 GitHub repository。
:::
> [commit 6cec9c3](https://github.com/LindaTing0106/linux2024_finalproject/commit/6cec9c3610ffb11601897bea381e33aa84eb3c96)
為了驗證其正確性,將 [cpp/mutex_harness.cc](https://github.com/mc-imperial/modelcheckingfutexes/blob/main/cpp/mutex_harness.cc) 編寫為 C 語言 mutex_harness.c 。
這邊比較特別的是將 atomic 操作從 C++ 轉為 C 的過程。最初 C++ 程式中預設的 memory_order 方式都為 memory_order_seq_cst 。
則繼續沿用 NTHREADS 設為 1000 , ELEMS_PER_THREAD 設為 1000 的配置,運行程式。
```cmake
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 加入進行比較。
![mutex2_com](https://hackmd.io/_uploads/r1d0FW_BA.png)
在此得到結果,可以看到使用 drepper2.h 的 mutex 時,其表現與使用 pthread 差不多,甚至表現較差的案例需要的時間大於 pthread 。
由於作者給出了很多種 mutex 實作,在這邊我將所有檔案都拿來做比較。
![com](https://hackmd.io/_uploads/Sksha4dHA.png)
由於 drepper1 的 mutex 會有 data racing ,故我們可以忽視它,在這邊可以看到除了 drepper2 中較好的實驗結果有優於其他,剩餘的 mutex 其表現都差不多。
為了找出 drepper 和範例中的 mutex 為什麼效能上會有差距,先將 drepper 中速度最快的 drepper_1 與其進行比較。
![d1_futex_com](https://hackmd.io/_uploads/SkMLw3Z8R.png)
可以看到就算是運行最快的 drepper_1 在比較簡單的 case 中效能還是比範例給的差。
在此我將 drepper_1 中使用到的 memory_order 改為更加彈性的 release 和 acquire ,但整體差別還是不大。
:::danger
解釋並使用其他工具 (如 Ftrace) 進行更細緻的分析。
:::
![d1_1_futex_com](https://hackmd.io/_uploads/ByRsdn-U0.png)
推測應該是由於範例中的 mutex 有 try_lock 此步驟,如果今天 lock 在足夠短的時間內被釋放,所以在實驗的時候我再將範例中 mutex 中 lock 改為不經過 trylock 。
![d1_1_futex_without_try_com](https://hackmd.io/_uploads/Hy5r5nZLA.png)
此時即可以看到範例中的 mutex 優勢在於在此程式中,執行緒可以在很快的時間內釋放 lock 導致 mutex 在 trylock 時即可以拿到 lock 。
此時換為 drepper_2 與範例比較,則可以發現調整 memory_order 後的 drepper_2 與沒有 try_lock 的範例程式效能是差不多的。
![d2_1_futex_without_try_com](https://hackmd.io/_uploads/Syc5U6ZLC.png)
於是我將 drepper_2 再加上 trylock 的功能,使得如果其他執行緒能夠在很快速的時間內將 mutex 釋出,則可以直接透過 trylock 的方式存取 lock 。
最後我將實驗次數調整至 10000 ,可以看到調整過後的 drepper_2 和原本的 mutex 的效能是<s>差不多</s> 的。
:::danger
工程人員要避免說「差不多」,務必使用精準詞彙。
:::
![d2_1_with_trylock_futex_com](https://hackmd.io/_uploads/r1KWH5HUR.png)