Starvation-Free Solutions of Mutual Exclusion Problems Using Semaphores
Date
1987-10
Authors
Yue, Kwok-Bun
Journal Title
Journal ISSN
Volume Title
Publisher
Proceedings of the ACM South Central Regional Conference
Abstract
The standard implementation of mutual exclusion by means of a semaphore allows starvation of processes. Between 1979 and 1986, three algorithms were proposed that preclude starvation. These algorithms use a special kind of semaphore. We model this so-called buffered semaphore rigorously and provide mechanized proofs of the algorithms. We prove that the algorithms are three implementations of one abstract algorithm in whicheverycompetingprocessisovertakennotmorethanoncebyanyotherprocess.Wealsoconsideraso-called polite semaphore, which is weaker than the buffered one and is strong enough for one of the three algorithms. Reļ¬nement techniques are used to compare the algorithms and the semaphores.
Description
Keywords
Citation
Yue, K. and Jacob, R., Starvation-Free Solutions of Mutual Exclusion Problems Using Semaphores. Proceedings of the ACM South Central Regional Conference, October 1987.