# Final
contributed by < `LindaTing0106` >
## TODO: 閱讀 [並行程式設計: 實作輕量級的 Mutex Lock](https://hackmd.io/@sysprog/concurrency/%2F%40sysprog%2Fconcurrency-mutex) 並重現實驗，紀錄問題
### 前提
早期的並行程式在運行時，為了避免執行緒在 critical section 發生競爭，當執行緒進入 critical section 時有兩種處理方式，一種為每次都呼叫 system call 交給核心檢查是否有競爭發生，但這會造成不必要的成本花費。
另一種方式為使用 spinlock 將不能進入 critical section 的執行緒鎖住，但此舉造成 CPU 資源無法釋放，且在多核系統上需要另做處理。
Futex 的誕生，使得執行緒在 user space 上就可以檢查是否有競爭發生，如果有競爭發生再透過核心去處理，減少不必要的成本。
### Mutex lock
在下面將重現幾個此篇教材中出現的例子。
### Example
在 [main.c](https://github.com/sysprog21/concurrent-programs/blob/master/mutex/example/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` ，並使其他執行緒脫離做事迴圈。
### 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: 閱讀 https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2023/SPIN.pdf | 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);
}
}
```
這些函式確保能夠在 Promela 中模擬 C/C++ 的原子操作，並處理溢位和下溢情況，從而實現與實際系統行為一致的模擬。
### mutex verification
```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 個執行緒。
### 錯誤例子 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 程式碼
為了驗證其正確性，將 [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 。
~~在此推測為其中的 atomic 行為都是 memory_seq_cst 的模式，導致編譯器無法最大化優化其。~~
由於作者給出了很多種 mutex 實作，在這邊我將所有檔案都拿來做比較。
由於 drepper1 的 mutex 會有 data racing ，故我們可以忽視它，在這邊可以看到除了 drepper2 中較好的實驗結果有優於其他，剩餘的 mutex 其表現都差不多。
為了找出 drepper 和範例中的 mutex 為什麼效能上會有差距，先將 drepper 中速度最快的 drepper_1 與其進行比較。
可以看到就算是運行最快的 drepper_1 在比較簡單的 case 中效能還是比範例給的差。
在此我將 drepper_1 中使用到的 memory_order 改為更加彈性的 release 和 acquire ，但整體差別還是不大。
推測應該是由於範例中的 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 的效能是差不多的。
Sign in with Wallet
Connect another wallet