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.