Szymanski算法

Szymanski算法是解決多個執行緒並發訪問一個共享資源的互斥問題的一個算法。由Boleslaw Szymanski於1988年提出。^[1]^[2]^[3]該算法具有很多優良性能，如線性等待，解決了由Leslie Lamport提出的開問題。^[4]

算法的類比解釋

該算法可以用等候室(waiting room)做一個直觀地類比。等候室有一個入口門與一個出口門。起初，入口門是打開的。所有想要進入臨界區的執行緒在差不多同一時間由入口進入等候室。最後一個進入的執行緒負責關閉進口門。然後在等候室的執行緒根據優先級高低依次進入臨界區。最後退出臨界區的執行緒負責打開入口門。

算法的實現

每個執行緒有一個flag變量表示該執行緒所處的狀態。規定其含義為：

0: 在外面，未申請訪問臨界區
1: 在入口門外等待
2: 在入口門內等待其它提出申請的進程都進入入口門
3: 正在進入入口門
4: 入口門關閉，在等候室里等待進入臨界區，或正在訪問臨界區

可以把這些flag變量表示為一個數組，共有n個元素。每個進程只寫屬於自己的flag數組元素，只讀取其它執行緒的flag數組元素。這種「單獨寫」策略有助於提高cache性能。入口門的狀態由所有的flag變量共同確定。

算法的偽代碼實現:

#进入临界区的协议：
flag[self] ← 1                    #站在入口门外，申请进入等候室
await_until(all flag[1..N] ∈ {0, 1, 2}) #等待入口门打开。即不存在有进程处于3、4状态，包括正在进门、正在使用临界区
flag[self] ← 3                    #站在入口门处，即正在进入。
if any flag[1..N] = 1:            #如果还有在入口门外等待进入的线程
    flag[self] ← 2                #把自己置为在入口门内，等待所有提出申请的线程都完成进入等候室
    await_until(any flag[1..N] = 4)     #等待最后进门的线程关闭入口门

flag[self] ← 4                    #门处于关闭状态，线程在等候室
await_until(all flag[1..self-1] ∈ {0, 1})   #等待所有具有更高优先级的线程访问完临界区，退出等候室

#这里是临界区
#...

#退出临界区的协议
await_until(all flag[self+1..N] ∈ {0, 1, 4}) #确保所有比自己优先级低的已经通过入口门的线程都进入了等候室
flag[self] ← 0 #离开等候室，如果自己是最后离开的，则入口门被打开

上述偽代碼中的"all"與"any"分別表示"所有"與"存在".

該算法容易直觀理解其正確性。但是其正確性的形式驗證比較難。一些文獻給出了形式驗證^[2]^[5].

參考文獻

[1]
Szymanski, Boleslaw K. A simple solution to Lamport's concurrent programming problem with linear wait. ICS '88: Proceedings of the 2nd international conference on Supercomputing (St. Malo, France: ACM). 1988: 621–626. ISBN 0-89791-272-1. doi:10.1145/55364.55425.
[2]
Manna, Zohar; Pnueli, Amir. An Exercise in Verification of Multi-Process Programs.. Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra. Springer Verlag. 1990: 289–301. ISBN 978-0-387-97299-2.
[3]
Szymanski, Boleslaw. Mutual Exclusion Revisited (PDF). Fifth Jerusalem Conference on Information Technology (Jerusalem, Israel). 1990: 110–117 [2012-09-02]. （原始內容 (PDF)存檔於2012-10-29）.
[4]
Lamport, Leslie. The mutual exclusion problem: partII—statement and solutions. Journal of the ACM (ACM). 1986, 33 (2): 327–348. doi:10.1145/5383.5385.
[5]
de Roever, Willem-Paul; de Boer, Frank; Hannemann, Ulrich; Hooman, Jozef; Lakhnech, Yassine; Poel, Mannes; Zwiers, Job. Concurrency Verification. Number 54 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. November 2002. ISBN 978-0-521-80608-4. doi:10.2277/0521806089.

參見

[Sz88-1] [1]
Szymanski, Boleslaw K. A simple solution to Lamport's concurrent programming problem with linear wait. ICS '88: Proceedings of the 2nd international conference on Supercomputing (St. Malo, France: ACM). 1988: 621–626. ISBN 0-89791-272-1. doi:10.1145/55364.55425.

[ZA91-2] [2]
Manna, Zohar; Pnueli, Amir. An Exercise in Verification of Multi-Process Programs.. Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra. Springer Verlag. 1990: 289–301. ISBN 978-0-387-97299-2.

[Sz90-3] [3]
Szymanski, Boleslaw. Mutual Exclusion Revisited (PDF). Fifth Jerusalem Conference on Information Technology (Jerusalem, Israel). 1990: 110–117 [2012-09-02]. （原始內容 (PDF)存檔於2012-10-29）.

[LL86-4] [4]
Lamport, Leslie. The mutual exclusion problem: partII—statement and solutions. Journal of the ACM (ACM). 1986, 33 (2): 327–348. doi:10.1145/5383.5385.

[5] [5]
de Roever, Willem-Paul; de Boer, Frank; Hannemann, Ulrich; Hooman, Jozef; Lakhnech, Yassine; Poel, Mannes; Zwiers, Job. Concurrency Verification. Number 54 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. November 2002. ISBN 978-0-521-80608-4. doi:10.2277/0521806089.

[1]

[2]

[3]

[4]

[5]