Mutual Exclusion Using Weak Semaphores

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.