Study

Master Quality of Software (Computer Science) at Radboud University

Master thesis: model checking Qt's Readers-Writers component

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.

You can download my thesis in pdf format.

Research project: interactive floor

Interactive applications are widely used in public relations. A novel way to attract attention. This proposal describes a project to implement an Interactive Floor (IF). IFs consist of a projection on a floor with which users can interact by moving on or over the projection. Together with Mark Blokpoel, we implemented a pong game. Also we implemented another scene that project footsteps behind a walking person, supporting tracking multiple concurrent walking persons.

A little video showing our result:

Bachelor Computer Science at Radboud University

Bachelor thesis: reliability of a read-write lock implementation

Read-write locking is an important mechanism to speed up concurrent access to certain resources within the same program. The correctness of the implementation is important: for example no deadlock should occur and certain properties, like exclusivity for writers, must be guaranteed. To assert the reliability of a read-write lock implementation, it is modelled and checked in UPPAAL. After adjustments to the implementation no bugs were found.