Javascript must be enabled for the correct page display

Mutual Exclusion Using Weak Semaphores

IJbema, M. (2011) Mutual Exclusion Using Weak Semaphores. Master's Thesis / Essay, Computing Science.

INFOR_MA_2011_IJbemaM.pdf - Published Version

Download (581kB) | Preview


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

Actions (login required)

View Item View Item