2007/11/21

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。

Labels:

<< 回到主頁