Group mutual exclusion

This is joint work with Alex A. Aravind. It concerns a new algorithm for group mutual exclusion, using fetch-and-increment instructions. Group mutual exclusion is a generalization of the readers-writers problem, introduced by Y. Joung in 1998. There is a fixed number of forums available. Our solution satisfies the following conditions.

• Mutual exclusion. If some thread is attending a forum, then no thread is attending a different forum at the same time.
• Deadlock-freedom. When one or more threads have requested forums, one of the requests is eventually answered.
• Individual progress. Every request for a forum is eventually answered; after the answer the requesting thread eventually returns to the noncritical section.
• Simultaneous acceptance. When a thread p opens a new forum f, every thread q that at this moment has completed a request for forum f, enters forum f within a bounded number of steps of p and q.
• No late entry. No thread p is allowed to enter an open forum f if p initiated its request after f was opened.
• Forum first-come first-served. If forum f1 is requested before any request for forum f2 is initiated, then forum f1 is opened before forum f2.

Nonatomic group mutual exclusion

The above algorithm uses shared variables that can be read and written atomically, and also fetch-and-increment registers, which are even stronger. These atomic instructions rely on mutual exclusion at a lower level, as has been argued by Lamport. We (Alex Aravind and I) have therefore developed a group mutual exclusion algorithm based on nonatomic shared variables (safe variables in the sense of Lamport). A paper is in preparation. A proof script for the algorithm with the proof assistant PVS is available.

Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink