HackMD透過 Model Checking 學習並行處理
資料整理: jserv
你終究要形式化驗證的，那為什麼不一開始就驗證？
檢驗互斥演算法
Dekker's Algorithm 是第一個已知的 mutual exclusion (互斥) 演算法，在 1962 年 (另一說在 1963 年) 提出，在 1965 年由 Dijkstra (1972 年的 Turing Award 得主) 提出數學證明，因此也稱為 Dekker-Dijkstra's Algorithm。其核心概念是「孔融讓梨」，任意行程 (或執行緒) 在存取 critical section (以下簡稱 CS) 之前，會先檢查其它行程是否也要存取 CS，之所以說「讓梨」，是考慮以下要素:
- 若其它行程也要存取 CS，而且
- 其它行程也擁有執行許可
若這二個要素成立，行程就會等待，直到其它行程存取 CS 完畢。反之，若其它行程無法同時滿足前述二個條件，目前行程就會存取 CS。
我們可將行程的執行過程想像為「在鐵軌上奔跑的二台火車」，如下圖:
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
標註為 "criticial section" 的區域就是，二台火車都可能涉足到的共享區域，同時至多只能一台火車穿越，否則就會釀成嚴重的交通事故。Dekker's Algorithm 在這樣的情境設定中，就相當於引入轉轍器 (英語：Point，美語：Switch，用來轉換道岔或鎖閉道岔的方向)，用來告知火車應該在穿越特定區域前，做出變換方向的操作，相互禮讓並搭配必要的等待，從而確保 CS (即重疊的軌道) 最多只有一台火車穿越。
Dekker's Algorithm 用 C 程式碼表示如下:
Thread 1 | Thread 2
======== | ========
0: while (true) { | while (true) {
1: /* non-critical code */ | /* non-critical code */
2: flag[0] = true; | flag[1] = true;
3: while (flag[1]) { | while (flag[0]) {
4: if (turn != 0) { | if (turn != 1) {
5: flag[0] = false; | flag[1] = false;
6: while (turn != 0) ; | while (turn != 1) ;
7: flag[0] = true; | flag[1] = true;
8: } | }
9: } | }
10: /* critical section */ | /* critical section */
11: turn = 1; | turn = 0;
12: flag[0] = false; | flag[1] = false;
13: } | }
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
運用 model checking，對應以下的操作:
- 建構針對上述演算法的有限狀態機 (finite-state machine, FSM) 模型
- 確立可到達狀態 (reachable states) 的集合
- 驗證所有可到達狀態都滿足 mutual exclusion 的要求
- 並非證明程式碼無誤 (bug-free)，而是試圖找出違反期望特質的反例 (counterexample)
- 也可驗證其他性質，如:
- 例如，能否避免發生 starvation: 若一個行程嘗試進入該 CS，儘管可能等待，但最終都要可成功進入 CS
這樣的有限狀態機展現如下:
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
如上圖解析可見，每個行程有 6 個控制點 (即上圖的 1, 12, 10, 3, 4, 6)，另外有 3 個全域二元 (boolean) 變數:
flag[0]flag[1]turn
由控制點的進出 (2 個狀態) 及 3 個全域變數可得到 10 的區域，也就是在 CS 中，沒有可到達的狀態。
我們可撰寫以下使用 POSIX Thread 的 C 程式來測試 Dekker's Algorithm:
#include <pthread.h>
#include <stdbool.h>
#include <stdio.h>
#include <unistd.h>
bool flag[2];
int turn;
void in_cs(int num) { usleep(5000); printf("P%d is in CS.\n", num); }
void P0() {
while (true) {
flag[0] = true; /* P0 wants to enter CS */
while (flag[1]) { /* see if P0 wants to enter CS */
if (turn == 1) { /* see if P1 can enter CS */
flag[0] = false; /* Once P1 enters CS, P0 shoud not enter */
while (turn == 1) ; /* see if turn is P1 */
flag[0] = true; /* P0 wants to enter CS */
}
}
in_cs(0); /* critical section */
turn = 1; /* P0 exits from CS, turn should be P1 */
flag[0] = false; /* P0 no longer wants to enter CS */
}
}
void P1() {
while (true) {
flag[1] = true; /* P1 wants to enter CS */
while (flag[0]) { /* see if P0 wants to enter CS */
if (turn == 0) { /* see if P0 can enter CS */
flag[1] = false; /* Once P0 enters CS, P1 should not enter */
while (turn == 0) ; /* see if turn is P0 */
flag[1] = true; /* P1 wants to enter CS */
}
}
in_cs(1); /* critical section */
turn = 0; /* P1 exits from CS, turn should be P0 */
flag[1] = false; /* P1 no longer wants to enter CS */
}
}
int main() {
pthread_t t1, t2;
flag[0] = flag[1] = false;
turn = 0;
if (pthread_create(&t1, NULL, (void *) P0, NULL) != 0)
return 1;
if (pthread_create(&t2, NULL, (void *) P1, NULL) != 0)
return 1;
pthread_join(t1, NULL);
pthread_join(t2, NULL);
return 0;
}
參考的執行輸出為: (省略後續重複的部分)
P0 is in CS.
P0 is in CS.
P1 is in CS.
P1 is in CS.
P0 is in CS.
P0 is in CS.
P1 is in CS.
P1 is in CS.
但若我們將第 17 行 while (turn == 1) ; 予以註解，重新編譯並執行，會得到以下輸出:
P0 is in CS.
P0 is in CS.
P1 is in CS.
P0 is in CS.
P0 is in CS.
P1 is in CS.
P1 is in CS.
乍看之下，P0 和 P1 輪番進入 critical section，但這樣的實作可確保所有狀態都滿足 mutual exclusion 的要求嗎？
我們可透過 SPIN/Promela 來建立對應的模型:
bool turn, flag[2];
active [2] proctype dekker() {
byte cnt = 0;
pid i = _pid, j = 1 - _pid;
again:
flag[i] = true;
do
:: flag[j] ->
if
:: turn == j ->
flag[i] = false;
!(turn == j);
flag[i] = true
:: else -> skip
fi
:: else ->
break
od;
cnt++;
assert(cnt == 1); /* critical section */
cnt--;
turn = j;
flag[i] = false;
goto again
}
其中:
active [2]表示有 2 個執行的實例 (instance)proctype表示 process (行程) 型態_pid是預先定義且唯讀的pid型態變數，紀錄行程的識別數值 (PID)，每個行程的 PID 不重複do和od涵蓋的區域是迴圈 (loop)turn == j是個 guard (先決條件)，->則是先決條件成立時，接著會執行的敘述assert(cnt == 1)表示若cnt不為1，則離開程式，否則繼續執行
透過 SPIN 來驗證:
$ spin -run dekker.pml
會得到以下輸出:
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 32 byte, depth reached 39, errors: 0
這意味著 mutual exclusion 的規範和實作匹配。
產生上圖的命令:
$ spin -a dekker.pml && gcc -o pan pan.c
$ ./pan -D | dot -Tps | ps2pdf - pan.pdf
驗證並行程式
並行機制 (Concurrency) 提供給軟體系統更多的效能和需求。不幸的是，這使的原本就不易檢驗的系統特性變的更加困難。通常關鍵性的系統(critical systems) 可能因為發生系統錯誤而造成無法承受的損失，故檢驗軟體的正確性是對這一類系統是相當重要的。模型檢驗 (model checking) 能幫助我們發現系統 中的錯誤進而修正它。一般來說，並行或分散式的程式由於系統都相當複雜而難以去分析。因此，提供一個有效率且自動化的驗證技術是相當重要的。
以資料庫更新資料為例。更新 (update) 必須先將欲存取資料鎖定 (lock) 且禁止其他可能的讀寫，避免資料競爭 (data race)。之後才進行更新。當資料更新完畢，再解除鎖定 (unlock)。下圖是此資料庫更新的簡化模型。
當資料庫有了 DB_Write 的行為後，行程從狀態 0 經由鎖定 (lock) 行為而到達狀態 1。該筆卻更新的資料也許不只一筆，行程可不斷地經由更新 (update) 行為再回到狀態 1。之後更新結束，行程從狀態 1 經由解除鎖定 (unlock) 行為而到達狀態 2。
軟體驗證所要分析的性質，主分成以下二類：
- 安全性質(Safety Property)
- 程式進行時不會進 入不良的狀態
- 例如，並行互斥(mutual exclusion)指的是一個系統資源不 會同時被兩個以上的行程進行存取，其所代表的就是一種安全性質
- 活化性質(Liveness Property)
- 程式執行時終究會進入某個良好的狀態
- 例如某個行程在系統中要求某種服務，而系統最終將提供此服務給請求的行程，如此將不會產生飢餓的情形 (freedom from starvation)，
以下方的英國式電梯來說，系統包含「G 樓」(Ground floor，也稱「零樓」，對應到我們習慣的「一樓」)，「1 樓」是指地面上一層樓 (也就是我們習慣的「二樓」)，以及「2 樓」(對應到我們習慣的「三樓」):
運用 model checking，我們可檢驗上述提到的二類特性:
- 安全特性: 電梯移動的過程中，門口不會開啟
- 活化特性: 無論任何樓層有人按電梯，中間或許會等待，但最終按電梯的人都可見到電梯移動到指定的樓層
本文探討的活化性質將以 progress property 為主。所謂的 progress property 所聲稱的是，無論如何描述系統，某些特定的行動(specified action)最終(eventually)將會被執行。明顯的 progress 的相反面即為 starvation。 progress property 能簡單並且足夠詳細的描述並行系統中的活化性質。
模型驗證工具目前大多以全域分析為主要架構。但模型驗證目前碰到的最主 要問題為組態爆炸，這樣的結果使的許多以全域分析的驗證工具在還沒有能檢驗 出系統是否違反某些性質時，就因為組態爆炸的產生而導致驗證失敗。
SPIN/Promela
problem of formally verifying, in an automated and exhaustive way, that a given system model M matches a given specification
, i.e. a set of logical properties.
model checking 的具體作法是狀態空間檢索 (state-space search)，原理就是將程式或通訊協定看作一個分散式系統，局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發。
Model checking 的主流工具包括 SPIN, AsmL, SMV 等等，理論主要是利用時序邏輯 (Temporal Logic) 和有限狀態機 (Finite State Machine)，應用遍及硬體設計、安全分析、自動控制等範疇。
SPIN 是由貝爾實驗室 Gerard Holzmann 博士帶領發展的通訊協定與軟體驗證工具。SPIN 使用 Promela 程式语言來建構，整個系統可看作一组同步、可擴展的有限狀態機，支援所有可用的線性時序邏輯，來表示正確性驗證要求。
SPIN 可驗證的性質除了常見的死結 (deadlock)、斷言 (assertion)、未到達狀態 (unreachable state) 等等之外，亦可檢驗線性時間邏輯(Linear-Temporal Logic，LTL) 的性質。SPIN 採用的方法是時間邏輯 (temporal logic) 公式反向後轉換成 büchi automata。然後運用自動機學理 (automata theory) 檢測 büchi automata 與狀態空間的合成機器是否接受可接受語言為空集合。簡單地說，就是要檢查的性質不會出現在狀態空間中。使用 LTL 性質可對系統模型檢驗安全性質 (safety property) 和活化性質 (liveness property)。
SPIN 亦提供數種模擬的功能，如隨機 (randomly) 路徑模擬、使用者互動 (interactive) 路徑模擬。上述的模擬情境是直接使被模擬的行程運作，直到分支點時，按照隨機或使用者所選擇的路徑繼續執行下去。如果行程的結構使得無 限迴圈產生，使用者可決定要無限的模擬下去或在指定的步數 (steps) 內結束。SPIN 模擬中最重要的功用是追蹤驗證找到的錯誤。當 SPIN 對某個系統進行驗證時，若某個違反性質的錯誤產生，工具程式會產生一個可供追蹤的檔案，且使用者能運用模擬的追蹤功能，找到發生錯誤的所在狀態位置為何。如此可方便使用者觀察及更改設計上的缺失 (flaw)。
常見的設計缺失:
- starvation: no access to a resource
- deadlock: complete absence of progress
- race conditions: unprotected critical sections
- constraints violation: buffer overrun, overflows, …
- under-specified model: unexpected behaviours
- over-specified model: dead code / unreachable states
驗證最主要的目的是對設計進行先期檢驗，然後找出系統設計時違反需求的
錯誤。如此在系統真正被實作時，因為設計本身的問題所造成的錯誤和損失，期待可減到最小。驗證可在系統所有的狀態中證明某一種難以偵測的錯誤不存在，這方面是測試難以達到的。
驗證雖然有許多好處，但狀態爆炸問題依舊是個難題。若驗證和測試分別是正確性確保技術的光譜兩端，那麼模擬可被歸類為中間的方法。模擬雖不能證明錯誤的不存在，但可避免耗掉大量的記憶體來展開狀態空間，而且雖不能實際測試系統每個細節，但卻能在主要的設計上進行探索。比起驗證，模擬具備的優點如:
- 雖然狀態爆炸的問題還在，但是模擬不需耗掉大量的記憶體，仍可以做到一定程度的正確性確保;
- 在模擬當中，因為有較為足夠的記憶體，許多系統原有的資訊可以被保留下來以供檢驗。
比起測試，模擬具備的優點如:
- 不需系統實作後才可以進行，可以直接模擬為系統所設計的模型
- 模擬可以有系統地選擇欲探索的路徑，但測試卻要找到適當的測試案例(test case) 才能進行。
