IJbema, M. (2011) Mutual Exclusion Using Weak Semaphores. Master's Thesis / Essay, Computing Science.
|
Text
INFOR_MA_2011_IJbemaM.pdf - Published Version Download (581kB) | Preview |
Abstract
In this thesis we describe two algorithms which implement mutual exclusion without individual starvation, one by Udding[8] and one by Morris[7]. We prove, using the theorem prover PVS, that they both implement mutual exclusion, and are free from both deadlock and individual starvation. Though the algorithms were provided with a proof, they were not mechanically verified as of yet. We conclude by looking at a conjecture by Dijkstra, which was disproved by the existence of the algorithms by Udding and Morris. We weaken it in such a way that it is true, and prove it informally.
| Item Type: | Thesis (Master's Thesis / Essay) |
|---|---|
| Degree programme: | Computing Science |
| Thesis type: | Master's Thesis / Essay |
| Language: | English |
| Date Deposited: | 15 Feb 2018 07:45 |
| Last Modified: | 15 Feb 2018 07:45 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/9519 |
Actions (login required)
 |
View Item |