Final

contributed by < LindaTing0106 >

TODO: 閱讀並行程式設計: 實作輕量級的 Mutex Lock 並重現實驗，紀錄問題

前提

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

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

Mutex lock

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

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 中，使用 common 當作共享變數。並創建

c t x_{0}

c t x_{3}

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

在

c t x_{i}

開始執行前，要先確保

c t x_{i + 1}

沒有被鎖住。其行為模式為，將

c t x_{i + 1}

上鎖後，對

c t x_{i}

進行解鎖，因此最先執行的會是

c t x_{3}

，且執行順序為

c t x_{3}

c t x_{2}

c t x_{1}

c t x_{0}

c t x_{3}

-> …。整個過程執行 50 次後會計算整體執行時間。

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

Image Not Showing Possible Reasons

The image was uploaded to a note which you don't have access to
The note which the image was originally uploaded to has been deleted

Learn More →

而在此程式碼中，我們可以看到一開始先讀取 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;
}

而效能比較圖為

Image Not Showing Possible Reasons

The image was uploaded to a note which you don't have access to
The note which the image was originally uploaded to has been deleted

Learn More →

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

pi_test

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

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

Image Not Showing Possible Reasons

The image was uploaded to a note which you don't have access to
The note which the image was originally uploaded to has been deleted

Learn More →

為了解決此問題，如果在 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 的問題。

Image Not Showing Possible Reasons

The image was uploaded to a note which you don't have access to
The note which the image was originally uploaded to has been deleted

Learn More →

修正

在描述 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

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);
    }
}

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

mutex verification

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 個執行緒。

錯誤例子 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 重寫 https://github.com/mc-imperial/modelcheckingfutexes/tree/main/cpp 程式碼

為了驗證其正確性，將 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 。

~~在此推測為其中的 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 的效能是差不多的。

Final

TODO: 閱讀 並行程式設計: 實作輕量級的 Mutex Lock 並重現實驗，紀錄問題

前提

Mutex lock

Example

perf-test

pi_test

修正

TODO: 閱讀 https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2023/SPIN.pdf | https://github.com/mc-imperial/modelcheckingfutexes 重現實驗 (原本用 C++) 並紀錄

摘要

Futex System Call Variants

Atomic Operations

mutex verification

錯誤例子 Futex-based Mutex

正確的 Futex-based Mutex

Bug 1: incorrect simplification

Bug 2: incorrect cmpxchg

CondVar verification

錯誤例子 Futex-based CondVar

正確例子 Futex-based CondVar (?)

正確例子 Futex-based CondVar

使用 Spin 檢查 mutex 正確性

原程式 C++ 實驗結果

TODO: 用 C11 futex 重寫 https://github.com/mc-imperial/modelcheckingfutexes/tree/main/cpp 程式碼

Read more

2024q1 Homework5 (assessment)

2024q1 Homework1 (lab0)

2024q1 Homework6 (integration)

2024q1 Homework4 (quiz3+4)

TODO: 閱讀並行程式設計: 實作輕量級的 Mutex Lock 並重現實驗，紀錄問題