In this article I want to show how we can analyze the OpenBSD kernel with domain-specific knowledge of spl(9) locking primitives, to find programming errors. This work was sponsored by Genua GmbH. Genua uses OpenBSD as a basis of many of their products. They allow developers to have a retreat…