[Distributed Algorithms] 第二堂: Mutual exclusion (2)

今天上 chap 10，開始講 modelling 的觀念，進入一堆證明，不過還是屬於 mutual exclusion 的範疇內，沒想到有這麼多種的 mutual exclusion。


花了最多時間講 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

這個觀念就用長幼有序的方式去想，

尊敬一次後，舉手，在尊敬一次，等後輩執行完後就不客氣了。

舒服!!