第四章 成效評估
4.1. Dining Philosopher
Dining Philosopher 是我們熟知的死結問題。它描述在一個系統中，多個行程 共享某些資源，若一個行程佔有資源時，其他行程若要使用則必須等候，直到該
資源被釋放。
Figure 19.Dining philosopher problem.
若每一個哲學家可以拿他位置上左邊和右邊的筷子吃飯，那麼在某個可能的
順序當中，哲學家們會在都拿了一邊的筷子而等候別人放下另一邊的筷子的狀態
中。我們用 PROMELA 將 dining philosopher 問題建構為一個系統模型。以三個
哲學家為例（模型如 Figure 20），我們有三個哲學家行程（phi0、phi1、phi2）共
享三個 channel，每一個 channel 由一個筷子行程（chop0、chop1、chop2）控管。
首先筷子行程會透過 channel 讓哲學家知道可以拿取筷子，而哲學家拿取左邊的
筷子（channel 陣列中數字較小的）後，會再檢視是否可以拿取右邊的筷子。
Figure 20. The 3 dining philosopher problem model.
將建構好的模型轉換成 CFG 及 CCS，我們可以得到 Figure 21 的示意圖。在
哲學家的模型當中，我們若使用 simulator 來拜訪它的狀態空間，在某一個路徑
中一定會遇到 deadlock。比如在 Figure 21 中，若拜訪的路徑同時到達：cho0、
cho1、cho2、phi0、phi2、phi3 分別在 state 1 時，這個系統就會進入 deadlock。
每一次進入 deadlock 並不一定是一樣的拜訪深度，也許某個哲學家要經過數百次
01 mtype = { take, release };
02 chan q[3] = [0] of { mtype };
03 04
05 proctype phi0 () 06 {
07 do
08 :: q[0]?take;
09 q[1]?take;
10
11 q[0]!release;
12 q[1]!release;
13 od 14 } 15
16 proctype phi1 () 17 {
18 do
19 :: q[1]?take;
20 q[2]?take;
21
22 q[1]!release;
23 q[2]!release;
24 od 25 } 26
27 proctype phi2 () 28 {
29 do
30 :: q[2]?take;
31 q[0]?take;
32
33 q[2]!release;
34 q[0]!release;
35 od 36 }
37 proctype chop0 () 38 {
39 do
40 :: q[0]!take;
41 q[0]?release;
42 od 43 } 44
45 proctype chop1 () 46 {
47 do
48 :: q[1]!take;
49 q[1]?release;
50 od 51 } 52
53 proctype chop2 () 54 {
55 do
56 :: q[2]!take;
57 q[2]?release;
58 od
59 }
拿起、放下筷子的過程，才會遇到 deadlock。
Figure 21. The CCS of 3 dining philosopher problem model.
我們分別將 10 次模擬 dining philosopher problem model 中每一次拜訪遇到死結的
深度記錄下來，並取得其平均值。Table 4 中我們得到在 3 個哲學家的問題當中，
平均要拜訪 22.8 次會遇到死結。
1st 2nd 3rd 4th 5th 6th 7th 8th 9th 10th Depth 38 6 14 54 6 14 46 22 14 14
Avg. 22.8
Table 4. The depth record after simulation.
phi0
cho1 cho0
cho2
phi2 phi1
接下來，我們結合局部性分析，除了 ph0 之外，將剩下的 cho0、cho1、cho2、
phi1、phi2 合併與最小化。dining philosopher problem 的例子當中，我們可以知 道被合併的行程其內部行為應該都會隱藏起來，只留下和外部溝通的行為。因此
我們在 cho0、cho1、cho2、phi1、phi2 合併與最小化後可以得如 Figure 22 的界
面行程。這個界面行程有 5 個 states 及 8 個 transitions。我們同樣將局部性分析
後的 dining philosopher problem 進行 10 的模擬，可以得到 Table 5。平均走進死
結的深度是 2.5 次。
Figure 22. The interface process of cho0, cho1, cho2, phi2 and phi3.
1st 2nd 3rd 4th 5th 6th 7th 8th 9th 10th Depth 3 3 2 10 15 20 2 2 16 17
Avg. 9
Table 5. The depth record after simulation with compositional analysis
在 4.3 節中，我們會大量擴展 dining philosopher problem 的行程數目，透過
4.2 節的評估方法，檢視模擬結合局部性分析的效果。
4.2. 評估方法
我們的實驗目的，是透過實驗證明模擬結合局部性分析的確可以減少拜訪的
路徑而達到拜訪整個系統的效果。以 4.1 的三個哲學家為例，我們合併其中兩個
哲學家的行程，並取得介面行程後再與另一個哲學家行程一同進行模擬。在大量
次數的模擬當中，取出其拜訪深度的平均值。以同樣的次數模擬原始系統，將其
平均值與前者比較。
在這個實驗當中，我們考慮兩個變因：
1. 局部性分析在整個系統中所佔的程度對拜訪深度的影響；
2. 若局部性分析在整個系統中所佔的比例一致，系統行程的數量對拜訪 深度的影響。
變因的第一項，很明顯的可以呈現出局部性分析對模擬的好處。第二項是為
了得知對愈大的系統進行模擬結合局部性分析是不是會愈好，而並不是只有小系
統適用。
最後，我們隨機模擬不同的路徑，取得找到 deadlock 的深度。在 100 次的拜
訪中，計算深度的平均值做為實驗結果數據。
4.3. 評估數據比較
在 Figure 23 中是以 100 個哲學家為實驗本體。X 軸所表示的是局部性分析
的程度，當刻度為 1 時表示沒有任何局部性分析的行程，當刻度為 2 時表示有
10%經過局部性分析合併的介面行程，刻度 3 表示有 20%，以此類推。Y 軸所表 示的是模擬系統時遇見 deadlock 所走的深度。在 Figure 23 裡可以看到，若局部
性分析的程度愈大，相對於模擬所需走入的深度就愈少。
The Chart of Depths by the Degree of Compositional Analysis
0 100 200 300 400 500 600 700 800 900
1 2 3 4 5 6 7 8 9 10
The Degree of Compositional Analysis
The No. of Depths
Depths
Figure 23. The chart of depths by the degree of compositional analysis.
在 Figure 24 中一樣是以沒有經過局部性分析的 10、20、…、100 個哲學家
為實驗組，而對照組是分別進行分析 10、20、…、100 個哲學家的一半後再分列
比較。X 軸所表示的是系統中哲學家的個數，當刻度為 1 時表示 10 個哲學家，
當刻度為 2 時表示有 2 個哲學家，以此類推。Y 軸所表示的是模擬系統時遇見
deadlock 所走的深度。在 Figure 24 中可以約略看到成長的比率大約是呈直線，
並不會因為哲學家數目愈多而有所變化。
The Compared Chart for the Primitive System and the 50% Analyzed System
0 100 200 300 400 500 600 700 800 900
1 2 3 4 5 6 7 8 9 10
The No. of Philosopher (10 times)
The No. of Depths
The Depths of Primitive System
The Depths of Analyzed System
Figure 24. The compared chart for the primitive system and the 50% analyzed system.
從上列的圖表數據中可以得到很簡單的結論：在哲學家問題的例子中，模擬
若結合局部性分析的確可以有效地減少拜訪的深度；局部性分析的程度愈高對模
擬進行愈有幫助，並且此法則不僅適用於少量哲學家行程的系統，大量哲學家行
程的系統亦可運用。
