2011年3月14日 星期一

[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
這個觀念就用長幼有序的方式去想,
尊敬一次後,舉手,在尊敬一次,等後輩執行完後就不客氣了。


舒服!!










    





沒有留言:

張貼留言