Starvation-Free Solutions of Mutual Exclusion Problems Using Semaphores

dc.contributor.authorYue, Kwok-Bun
dc.date.accessioned2019-10-04T19:29:13Z
dc.date.available2019-10-04T19:29:13Z
dc.date.issued1987-10
dc.description.abstractThe 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.
dc.identifier.citationYue, K. and Jacob, R., Starvation-Free Solutions of Mutual Exclusion Problems Using Semaphores. Proceedings of the ACM South Central Regional Conference, October 1987.en_US
dc.identifier.urihttps://hdl.handle.net/10657.1/1494
dc.publisherProceedings of the ACM South Central Regional Conferenceen_US
dc.titleStarvation-Free Solutions of Mutual Exclusion Problems Using Semaphoresen_US
dc.typeArticleen_US

Files

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description: