## 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
```
產生此圖
```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。
而在此程式碼中，我們可以看到一開始先讀取 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;
}
```
而效能比較圖為
明顯可以看到整體效能更佳。從兩張效能比較圖中可以發現，未經過讀取這一步驟的效能圖中，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 加入進行比較。
在此得到結果，可以看到使用 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 ，但整體差別還是不大。
:::danger
解釋並使用其他工具 (如 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 的效能是<s>差不多</s> 的。
:::danger
工程人員要避免說「差不多」，務必使用精準詞彙。
:::
Sign in with Wallet
Connect another wallet