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. Refinement 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.