I have just handed in my master's thesis. Next I will hold a presentation about the subject. It will be at March 11, 14:00 at HG01.057. In the mean time (e.g. if you want to prepare for the presentation), you can download my thesis in PDF format. After my presentation, I will put all the SPIN/Promela files online, along with a small guide to them.
The readers-writers algorithm is a widely used mutual exclusion mechanism in concurrent programming. Several versions of the algorithm exist. This thesis examines the algorithm used by Nokia's Qt framework. The algorithm is checked for deadlock and starvation issues using the Spin model checker. Previous work found a deadlock in the algorithm, and proposed and verified a corrected algorithm. The used model was limited. In this thesis, we reverify the results using a more detailed model. While verifying the algorithm for absence of starvation, no issues were found in the algorithm itself. However, the condition variables used by Qt's implementation have algorithmic starvation issues which makes the readers-writers implementation prone to starvation. A new algorithm for a starvation-free condition variable is presented and verified. This condition variable is constructed out of a starvation-prone condition variable, and is therefore applicable to similar situations were only a starvation-prone condition variable is available.