Starvation-Free Solutions of Mutual Exclusion Problems Using Semaphores
dc.contributor.author | Yue, Kwok-Bun | |
dc.date.accessioned | 2019-10-04T19:29:13Z | |
dc.date.available | 2019-10-04T19:29:13Z | |
dc.date.issued | 1987-10 | |
dc.description.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. | |
dc.identifier.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. | en_US |
dc.identifier.uri | https://hdl.handle.net/10657.1/1494 | |
dc.publisher | Proceedings of the ACM South Central Regional Conference | en_US |
dc.title | Starvation-Free Solutions of Mutual Exclusion Problems Using Semaphores | en_US |
dc.type | Article | en_US |
Files
License bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- license.txt
- Size:
- 1.71 KB
- Format:
- Item-specific license agreed upon to submission
- Description: