This project grew out of the master project of my former master student Mark IJbema. It resulted in the paper: W.H. Hesselink, M. IJbema: Starvation-free mutual exclusion with semaphores. Formal Aspects of Computing 25, issue 6 (2013) 947-969. DOI: 10.1007/s00165-011-0219-y. The paper discusses three related algorithms for starvation-free mutual exclusion with semaphores: the algorithms of Morris, Udding, and Martin and Burch. It also discusses PVS proofs of these algorithms. Available are the PVS dump files for Morris' algorithm, Udding's algorithm, and the algorithm of Martin and Burch. The details for Udding's algorithm are not contained in the paper mentioned above, but are put in a technical report.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink