共享記憶體多處理系統上具有優先權的互斥演算法

Abstract

大部分以lock來設計的互斥演算法，並未考慮優先權的問題，這類的演算 法在即時系統上並不適用。Markatos提出兩個具有優先權的lock同步演算 法。第一個方法是Burns的演算法的修改，這個方法在不是所有行程都想 要 lock的情形下，仍必須搜尋整個陣列以找出具有最高優先權的行程。 第二個方法是MCS lock的修改，這個方法在決定具有最高優先權的行程， 至此行程真正獲得lock的中間有較長的時間視窗。在此時間視窗中發出需 求的行程，即使具有更高的優先權，仍然必須等待。本論文中，我們提出 兩個具有優先權的互斥演算法：陣列－基底和串列－基底的優先權lock。 第一個方法修改自Anderson的演算法，只需要搜尋屬於等待行程的陣列元 素。第二個方法也是修改自MCS lock，但是縮短了時間視窗，減少發生優 先權倒置的機率。我們使用斷言的推論來證明MCS lock的正確性。我們的 串列－基底的優先權lock保有MCS lock的正確性。我們也提供斷言式的證 明於陣列－基底的優先權lock。 Most of the lock synchronization algorithms do not take priority into consideration, which makes them unsuitable for the real-time systems. Markatos has presented two priority spin locks. One is a modification of Burns's spin lock. It needs to scan the whole array to find the highest priority process even if not all processes are interested in the lock. The other is a modification of MCS lock. It has a long time-window from the time the highest priority process is decided to the time the highest is actually given privilege. A process that issues a request during the time-window must wait even if it has a higher priority. In this thesis, we propose two priority spin locks: array-based and list-based priority spin locks. The first, a modification of Anderson's spin lock, only scans the array elements of the waiting processes. The other, also a modification of MCS lock, has a shorter time-window. It reduces the possibility of priority inversion. We use assertional reasioning to prove the correctness of MCS lock. Our list-based priority spin lock preserves all the correctness property of MCS lock. An assertional proof is also given for our array- based priority spin lock.