Analyzing locks in OpenBSD’s Kernel with Domain-Specific Knowledge
by from OpenBSD Journal on (#60W2Z)
Christian Ludwig "wrote a tool to statically analyze spl(9) kernel locking in OpenBSD. It even found some bugs."
His write up is here: https://medium.com/@chrissicool/analyze-openbsds-kernel-with-domain-specific-knowledge-ca665d92eebb
His code for the Lock Balancing Checker referenced in the write up is available under an ISC license and can be obtained here: https://github.com/chrissicool/lbc