花了最多時間講 Dijkstra’s Mutual Exclusion Algorithm
屬要證明三個部分:
- well-formedness
- mutual exclusion
- progress
well-formedness 老師說不用甚麼證明,但我對於這個概念還是很模糊,mutual exclusion 用上禮拜的反證法概念。
老師還有特別證明,像是任兩個 process 甚麼情況有可能同時到達 flag(i):= 2 這行,但同一情況不可能一直發生。
對於 Mutual Exclusion 三位大師都有證明:
Dijkstra : 有 starvation 發生
Knuth : (忘記了)
E-M : 最好
上面的演算法,沒有 atomic,以
while turn != i do
if flag(turn)=0 then turn:=i
為例這兩個 turn 支間可以相隔很久,而且第二個 turn 沒有多讀的必要,這是因為 psuedo code 太高階了,課本範例有介紹用 pc counter 來達到 atomic 的寫法。
eq. (此 action 利用 precondition 當 pc counter 等於 set-flag-1 時就執行)
set-flag-1
Precondition:
pc=set-flag-1
Effect:
接下來證明複雜的 Progress...
課本用了很多 lemma 來說明,比較容易的想法是,CS 是空的時,很多人想進去,那最後 turn 一定會進入穩定狀態,而那個拿到 turn 的 process 也就勢如破竹的進入 CS 了。
課本上還用了比較學理的證明,但是那個太邏輯了,老師說沒甚麼必要(跳過)... XD
- Lockout-freedom : 不會餓死 (something good will eventually happened)
- Number of bypass a: 其他人最多執行 a 次 (something bad can not happened)
老師說這兩種狀況要注意,證明的方法很不一樣
接下來介紹 Peterson2P 和 PertersonNP
2P 比較好懂,NP 的證明就比較難,老師舉了想像 N-1 階樓梯,有 N 個老鼠想進去,每個階梯會黏住一個老鼠,所以最後會只有一隻能進去。
這些擰人化的想法只是幫主想像,學理上的證明還是要學院派一點 -= =
最後提到 BurnsMe Algorithm
這個觀念就用長幼有序的方式去想,
尊敬一次後,舉手,在尊敬一次,等後輩執行完後就不客氣了。
舒服!!
沒有留言:
張貼留言