四、 The practice
4.3 Eisenburg-McGuire’s mutual exclusion algorithm and its variation
Shared variables:
z turn∈{0,...,n−1}, initially arbitrary, writable by all processes
z for every i , 0≤i≤n−1, flag(i)∈{idle,want−in,in−cs}, initially idle , writable by process i and readable by all processes
Process i :
(private variable j: integer) R: ** Remainder Region **
Eisenburg-McGuire 在 1972 年所提 mutual exclusion algorithm[5] (亦見 Operating System Concepts，5th ed.，Silberschatz & Galvin，p.201)，如 Algorithm 8，除了符合基 本的正確性外又具備n−1 bounded waiting 的特性，主要是依靠 algorithm 中 shared variable turn ，它的值只在 extended CS 中被修改，也就是說任何的瞬間最多就只有一 個 process 能夠更改 turn 值；process 離開 CS 在 exit region 中要作 linear search 找出下一 個 non-idle process 並將turn 值改為此 process 之 index（此動作受到 extended CS 保護）， 而 turn 值所代表的 process 只要是 non-idle就是下一個能優先進入 CS 的 process。在 safety property 的設計仍然保留與 Dijkstra’s[4]一樣的機制，而 progress property 的證明也與 Knuth’s[6]雷同。
Lemma 4.3.1：EM0中，process α 在 exit region 中找到的下一個 non-idle process β 將必然繼 process α 之後進入 CS。
Proof by contradiction：假設有process γ 搶先在 process β 之前繼 process α 之後 進入 CS，可以得到下列事件發生順序的關係，
(1) t(ETβ2)<t(EαE2)，process α 在 exit region 中找到下一個 non-idle process 為 process β。
(2) t(EEα2)<t(EαE3)<t(EEα4)，這是同一個 process 所執行。
(3) t(EEα4)<t(ETγ11)，process γ 繼 process α 之後進入 CS，則 process γ 在 line T11 的 j≥ 測試條件必為 true。 n
(4) 由(2)、(3)得t(EαE3)<t(ETγ11)，process γ 在 line T11 執行時turn=β ，故 i
turn= 的測試必為 false。
(5) t(ETγ11)<t(ETβ2)，因為 process γ 在 line T11 對turn= 的測試為 false，則i idle
turn
flag( )= 的測試必為 true，方可進入 CS。
由(1)、(2)、(3)得t(ETβ2)<t(ETγ11)，與(5)發生矛盾。
Lemma 4.3.1 掌握了 algorithm EM0的 processes 之間溝通交接進 CS 的規律性，不但 可以證明n−1 bounded waiting，也是吾人賴以改進 generic approach 初步結果，增加 focused release 和 fast track 兩項功效的重要基礎。
Claim：EM0具備n−1 bounded waiting 的性質。
Proof by contradiction：欲證n−1 bounded waiting 等價於證明 1 bounded bypass。假 設兩個 non-idle processes α 、β欲進入 CS，在 process β進入 CS 之前，process α 進 入 CS 兩次。在 process α 第一次進入 CS 之後，於 exit region 尋找下一個 non-idle process 時必然找到第三個 non-idle process γ，並將 turn 值改為γ，不失一般性假設α <γ <β， 則在 process γ 進入 CS 之後到 process α 第二次進入 CS 之前，turn 值的變化過程中必 然曾經等於β，但是卻跳過 process β而讓 process α 第二次進入 CS，這與 Lemma 4.3.1 矛盾。
在 EM0上使用 2-dimensional permitted bits 的方式加上 local spin 會與 K1一樣發生 dead lock。在 EM0上使用 generic approach 可輕易地得到初步的 local spin algorithm EM2， 如 Algorithm 9，這過程吾人不必深入瞭解 algorithm EM0之運作細節，頂多只要能認出 trying region 中 P-loop 的 loser path，瞭解 processes 在 P-loop 中互動之方式，找出適當位 置加上 local spin code 即可，其結果已經讓 memory contention 降低很多，且因不更改原 有 program structure，正確性可確保。這種保守的方式適合於初學者。熟悉 concurrent programming 技巧者，若能深入瞭解個別 algorithm 之運作細節，可以進一步更改原有的
program structure 將 local spin 之功效發揮得更好，以 EM2 為實例詳述如何加入 focused release 與 fast track 兩項功效如 4.3.2、4.3.3 節所述。
Shared variables:
z turn∈{0,...,n−1}, initially arbitrary, writable by all processes
z for every i , 10≤i≤n− , flag(i)∈{idle,want−in,in−cs}, initially idle , writable by process i and readable by all processes
z for every i , 0≤i≤n−1, permitted(i)∈{true,false}, writable by all processes and readable by process i
Process i :
(private variable j: integer) R: ** Remainder Region **
4.3.2 Adding focused release to EM
2: Algorithm EM
3以 EM0來說，在其 exit region 有一段 linear search，其主要的目的是為了維持n−1 bounded waiting 的性質，我們做 local spin 時可利用這個 linear search 的動作找到單一 process 來做 release 標的（故稱為 focused release，若依 generic approach 是要 release 所 有其它 local-spinning processes），依據 Lemma 4.3.1，所釋放的單一 process 必然可進入 CS，那麼只需要一次 remote write 叫醒這 process 就夠了，其餘的n−2個 remote writes 只 是讓被叫醒的 processes 白忙而己，終究得再次測知挫敗而進入 local spin。因此，若能
深入瞭解原始 algorithm 運作細節則可用 focused release 大幅度地降低 remote write 次 數；EM3，如 Algorithm 10，最後兩行 code 即充分掌握 focused release 之機會，當 linear search 測到 non-idle process 標的時僅使用一次 remote write 叫醒它；但是，當 linear search 一遍尚未測知 non-idle processes，則系統後續是否已有 non-idle processes 不得而知，
吾人只能保守地使用n−1次 remote writes 將 permitted bits 準備好，以維持後續運作之正 確性。基於 asynchronous atomic read/write shared memory model 之本質，此刻縱使 linear search 做二遍或更多遍尋找下一個 non-idle process 仍然無法克服這“不得而知＂的基 本困難。若能動用功能較強的 read-modify-write model 協助，則很容易測知後續是否已 有 non-idle processes，MCS [10]有這種 algorithms。
Shared variables:
z turn∈{0,...,n−1}, initially arbitrary, writable by all processes
z for every i , 0≤i≤n−1, flag(i)∈{idle,want−in,in−cs}, initially idle , writable by process i and readable by all processes
z for every i , 0≤i≤n−1, permitted(i)∈{true,false}, writable by all processes and readable by process i
Process i :
4.3.3 Adding fast track to EM
3: Algorithm EM
4 Shared variables:z turn∈{0,...,n−1}, initially arbitrary, writable by all processes
z for every i , 0≤i≤n−1, flag(i)∈{idle,want−in,in−cs}, initially idle , writable by process i and readable by all processes
z for every i , 0≤i≤n−1, permitted(i)∈{true,false}, writable by all processes and readable by process i
Process i :
設計 fast track 時則必須謹慎驗證是否會破壞 safety property：有了 fast track 之後，
進入 CS 的 path 會多一個，safety property 正確性之分析變成比較複雜。目前在嘗試加上 fast track 時仍需依 algorithm 之差別而個別推論，仍無一般常規可循，也不是任何 algorithm 都有 fast track 的存在。以 Eisenburg-McGuire’s mutual exclusion algorithm[5]來
說，只要能夠設法留下路徑記錄讓被釋放的 process 能夠辨識出自己是目前唯一可以進 入 CS 的 process，那就有足夠理由可沿 fast track 直接跳到 CS，省下不必要的n−1次 remote memory accesses（S-loop，原本目的在於測知其他 processes 之狀態）。以這樣的 構想，在 fast track 的設計上利用額外的 private variable 由 process 自身記錄執行軌跡，
如 Algorithm 11，EM4中的spin−wake−up。
Claim：EM4維持 safety property。
Proof：當 process β測知自己符合 fast track 的spin−wake−up條件時，若能證明 process β是目前唯一能進 CS 之 process，則β可以免掉檢查n−1個 flag bits 的動作
（line T17、T18），直接進 CS。假設β在 fast track 測知可進 CS 但未進 CS 時停止不動，
則由其過去所走路徑可以推知，必然存在另一 process α 曾在 exit region 以 remote write 叫醒β，兩者之互動符合 Lemma 4.3.1 所述之前提，因此除了β外無其它 process 可以 進 CS。
版本 EM4程式結構精簡，保有原版 EM0具有n−1 bounded waiting 的優點，當系統 處於 heavy loading 時 local spin 的功效特別好。假設 process 在 trying region 的 P-loop 中 使用了 remote access 平均次數為m次就被阻擋而進入 local spin 狀態，在 exit region 找 下一個 non-idle process 所需 remote access 平均次數為k次，則經由 fast track 與 focused release 執行路徑，可計算出 process 進出一次 CS 所需 remote access 平均次數為m+ k+4 次,其中m+2次在 trying region，k+2次在 exit region。當系統 heavy loading 程度越高，
m值與k值越小。
4.4、4.5 節將繼續介紹兩個 one-writer/multiple-reader algorithm 如何加上 local spin 的機制，除了適用 2-dimensional permitted bits 之外，也發現這兩個 algorithm 中的 S-loop 亦可加上 local spin。