Bakery Algorithm

今天 OS 講到 mutual exclusion。暑假 FLOLAC 的 Deductive Program Verification 課堂上，資管系的蔡益坤老師活靈活現地描述 bakery algorithm 的三段峰迴。很可惜我當時仗著有錄音檔，沒把詳細內容寫在 blog 上，後來發現竟然弄丟了兩天的錄音檔，現在只記得其中兩段 XD。

在另一門課 Model Checking 裡面，王柏堯老師用 Spin 抓到一般實作出來的 bakery algorithm 的 bug。蔡老師於是為 bakery algorithm 辯護，要我們注意 bakery algorithm 的前提：號碼牌必須是 unbounded integers！從這裡就可以繼續發展 bounded integer 的變化版，這是第一段峰迴。接著這個峰迴我忘記是第二段還是第三段了：bakery algorithm 不要求從硬體支援 mutual exclusion，最炫的效果是，別人還在寫自己的號碼牌時我們就去看，以致於看錯了別人的號碼，整個演算法都還是對的！這點 Leslie Lamport 自己是到設計出來、寫完證明之後才發現的。Lamport 說：

I have invented many concurrent algorithms. I feel that I did not invent the bakery algorithm, I discovered it.

可見這個 algorithm 有多神妙。這個演算法出現在〈A New Solution of Dijkstra's Concurrent Programming Problem〉，這篇論文只有三頁。在 Lamport 的個人網頁上有一段說明，即使不看 paper 也應該讀一下那段說明，非常有趣。（剛剛引的句子就是從那段說明引來的。）

--
弄丟這份錄音檔真是一大損失 XD。

---

我在猜我忘記的那段峰迴是 bakery algorithm "[...] allows the system to continue to operate despite the failure of any individual component"，不過不能確定 XD。