Applying Stateless Model Checking to Work-Stealing libraries

Sammanfattning: Software verification by testing does not always detect concurrency errors. Software verification by Stateless Model Checking searches the state space more systematically than testing and can therefore detect concurrency errors which may not be found by testing alone. Dynamic Partial Order Reduction is a common SMC approach whichhas been implemented in the Nidhugg bug finding tool. This thesis evaluates the feasibility of applying Nidhugg to a real-world codebase in practice by detailing the various modifications which had to be made to the Wool work stealing library in order to successfully verify it using Nidhugg. In order to verify our modified version of Wool, we developed and analyzed a small Wool test suite. In the process, we found and reported a bug in Wool. Additionally, we found and reported a bug in Nidhugg. We also measured Nidhugg's performance when verifying this particular test suite.