---
tags: concurrency
---
# 透過 Model Checking 學習並行處理
> 資料整理: [jserv](https://wiki.csie.ncku.edu.tw/User/jserv)
你終究要[形式化驗證](https://hackmd.io/@sysprog/formal-verification)的，那為什麼不一開始就驗證？
## 檢驗互斥演算法
[Dekker's Algorithm](http://en.wikipedia.org/wiki/Dekker's_algorithm) 是第一個已知的 mutual exclusion (互斥) 演算法，在 1962 年 (另一說在 1963 年) 提出，在 1965 年由 [Dijkstra](https://en.wikipedia.org/wiki/Edsger_W._Dijkstra) (1972 年的 Turing Award 得主) 提出[數學證明](http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD123.PDF)，因此也稱為 Dekker-Dijkstra's Algorithm。其核心概念是「[孔融讓梨](https://dict.revised.moe.edu.tw/dictView.jsp?ID=79028&word=%E5%AD%94%E8%9E%8D%E8%AE%93%E6%A2%A8)」，任意行程 (或執行緒) 在存取 critical section (以下簡稱 CS) 之前，會先檢查其它行程是否也要存取 CS，之所以說「讓梨」，是考慮以下要素:
1. 若其它行程也要存取 CS，而且
2. 其它行程也擁有執行許可
若這二個要素成立，行程就會等待，直到其它行程存取 CS 完畢。反之，若其它行程無法同時滿足前述二個條件，目前行程就會存取 CS。
我們可將行程的執行過程想像為「在鐵軌上奔跑的二台火車」，如下圖:
標註為 "criticial section" 的區域就是，二台火車都可能涉足到的共享區域，同時至多只能一台火車穿越，否則就會釀成嚴重的交通事故。[Dekker's Algorithm](http://en.wikipedia.org/wiki/Dekker's_algorithm) 在這樣的情境設定中，就相當於引入[轉轍器](https://zh.wikipedia.org/wiki/%E8%BD%89%E8%BD%8D%E5%99%A8) (英語：Point，美語：Switch，用來轉換道岔或鎖閉道岔的方向)，用來告知火車應該在穿越特定區域前，做出變換方向的操作，相互禮讓並搭配必要的等待，從而確保 CS (即重疊的軌道) 最多只有一台火車穿越。
[Dekker's Algorithm](http://en.wikipedia.org/wiki/Dekker's_algorithm) 用 C 程式碼表示如下:
```cpp
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: } | }
```
運用 [model checking](https://en.wikipedia.org/wiki/Model_checking)，對應以下的操作:
* 建構針對上述演算法的有限狀態機 (finite-state machine, FSM) 模型
* 確立可到達狀態 (reachable states) 的集合
* 驗證所有可到達狀態都滿足 mutual exclusion 的要求
* 並非證明程式碼無誤 (bug-free)，而是試圖找出違反期望特質的反例 (counterexample)
* 也可驗證其他性質，如:
* 例如，能否避免發生 starvation: 若一個行程嘗試進入該 CS，儘管可能等待，但最終都要可成功進入 CS
這樣的有限狀態機展現如下:
如上圖解析可見，每個行程有 6 個控制點 (即上圖的 `1`, `12`, `10`, `3`, `4`, `6`)，另外有 3 個全域二元 (boolean) 變數:
* `flag[0]`
* `flag[1]`
* `turn`
由控制點的進出 (2 個狀態) 及 3 個全域變數可得到 $6^2 \times 2^3 = 288$ 可能的狀態，我們要確保在上圖標註 `10` 的區域，也就是在 CS 中，沒有可到達的狀態。
我們可撰寫以下使用 POSIX Thread 的 C 程式來測試 Dekker's Algorithm:
```cpp=
#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](http://spinroot.com/) 來建立對應的模型:
```cpp=
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 來驗證:
```shell
$ 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 的規範和實作匹配。
```graphviz
digraph p_dekker {
size="8,10";
GT [shape=box,style=dotted,label="dekker"];
GT -> S1;
S1 -> S13 [color=black,style=bold,label="flag[i] = 1"];
S13 -> S9 [color=black,style=bold,label="(flag[j])"];
S13 -> S16 [color=black,style=bold,label="else"];
S9 -> S4 [color=black,style=bold,label="
((turn==j))"];
S9 -> S8 [color=black,style=bold,label="else"];
S4 -> S5 [color=black,style=bold,label=" flag[i] = 0"];
S5 -> S6 [color=black,style=bold,label="(!((turn==j)))"];
S6 -> S13 [color=black,style=bold,label=" flag[i] = 1"];
S8 -> S13 [color=black,style=solid,label="(1)"];
S16 -> S19 [color=black,style=solid,label=" cnt = (cnt+1)"];
S19 -> S20 [color=black,style=bold,label=" turn = j"];
S20 -> S1 [color=black,style=bold,label=" flag[i] = 0"];
}
```
:::success
產生上圖的命令:
```shell
$ 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
:::info
$M \models \phi$
> problem of formally verifying, in an automated and exhaustive way, that a given system model M matches a given specification $\phi$, i.e. a set of logical properties.
:::
[model checking](https://en.wikipedia.org/wiki/Model_checking) 的具體作法是狀態空間檢索 (state-space search)，原理就是將程式或通訊協定看作一個分散式系統，局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發。
Model checking 的主流工具包括 SPIN, AsmL, SMV 等等，理論主要是利用時序邏輯 (Temporal Logic) 和有限狀態機 (Finite State Machine)，應用遍及硬體設計、安全分析、自動控制等範疇。
[SPIN](http://spinroot.com/) 是由[貝爾實驗室](https://en.wikipedia.org/wiki/Bell_Labs) [Gerard Holzmann](https://en.wikipedia.org/wiki/Gerard_J._Holzmann) 博士帶領發展的通訊協定與軟體驗證工具。[SPIN](http://spinroot.com/) 使用 Promela 程式语言來建構，整個系統可看作一组同步、可擴展的有限狀態機，支援所有可用的線性時序邏輯，來表示正確性驗證要求。
[SPIN](http://spinroot.com/) 可驗證的性質除了常見的死結 (deadlock)、斷言 (assertion)、未到達狀態 (unreachable state) 等等之外，亦可檢驗線性時間邏輯(Linear-Temporal Logic，LTL) 的性質。[SPIN](http://spinroot.com/) 採用的方法是時間邏輯 (temporal logic) 公式反向後轉換成 [büchi automata](https://en.wikipedia.org/wiki/B%C3%BCchi_automaton)。然後運用自動機學理 (automata theory) 檢測 [büchi automata](https://en.wikipedia.org/wiki/B%C3%BCchi_automaton) 與狀態空間的合成機器是否接受可接受語言為空集合。簡單地說，就是要檢查的性質不會出現在狀態空間中。使用 LTL 性質可對系統模型檢驗安全性質 (safety property) 和活化性質 (liveness property)。
[SPIN](http://spinroot.com/) 亦提供數種模擬的功能，如隨機 (randomly) 路徑模擬、使用者互動 (interactive) 路徑模擬。上述的模擬情境是直接使被模擬的行程運作，直到分支點時，按照隨機或使用者所選擇的路徑繼續執行下去。如果行程的結構使得無 限迴圈產生，使用者可決定要無限的模擬下去或在指定的步數 (steps) 內結束。[SPIN](http://spinroot.com/) 模擬中最重要的功用是追蹤驗證找到的錯誤。當 [SPIN](http://spinroot.com/) 對某個系統進行驗證時，若某個違反性質的錯誤產生，工具程式會產生一個可供追蹤的檔案，且使用者能運用模擬的追蹤功能，找到發生錯誤的所在狀態位置為何。如此可方便使用者觀察及更改設計上的缺失 (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
驗證最主要的目的是對設計進行先期檢驗，然後找出系統設計時違反需求的
錯誤。如此在系統真正被實作時，因為設計本身的問題所造成的錯誤和損失，期待可減到最小。驗證可在系統所有的狀態中證明某一種難以偵測的錯誤不存在，這方面是測試難以達到的。
驗證雖然有許多好處，但狀態爆炸問題依舊是個難題。若驗證和測試分別是正確性確保技術的光譜兩端，那麼模擬可被歸類為中間的方法。模擬雖不能證明錯誤的不存在，但可避免耗掉大量的記憶體來展開狀態空間，而且雖不能實際測試系統每個細節，但卻能在主要的設計上進行探索。比起驗證，模擬具備的優點如:
1. 雖然狀態爆炸的問題還在，但是模擬不需耗掉大量的記憶體，仍可以做到一定程度的正確性確保;
2. 在模擬當中，因為有較為足夠的記憶體，許多系統原有的資訊可以被保留下來以供檢驗。
比起測試，模擬具備的優點如:
1. 不需系統實作後才可以進行，可以直接模擬為系統所設計的模型
2. 模擬可以有系統地選擇欲探索的路徑，但測試卻要找到適當的測試案例(test case) 才能進行。
## 從範例學習 SPIN/Promela
## 待整理
* https://www.students.cs.ubc.ca/~cs-418/2016-2/lecture/03-29/slides.pdf
Sign in with Wallet
Connect another wallet