The kernel lock validator
Posted May 31, 2006 6:59 UTC (Wed) by mingo
Parent article: The kernel lock validator
Small additional thought to subtype paragraph: while subtypes do fix false positives, their role isnt just to get around exceptions - their role is to correctly map recursive locking semantics.
That means that the "special rules" added for the sake of lockdep (via the use of spin_lock_nested() APIs, etc.) act as a formal specification of the locking rules, and the validator checks those rules against actual behavior.
To stay with the partitions example: if for example some kernel code locks a component partition before a container partition then the validator will detect this deadlock scenario.
So subtypes are not a watering down of the "proof of correctness", they are more like a mechanism to "program by specification" and to let the validator check against that specification. For non-recursive locking, the validator can build the specification automatically.
(besides subtypes, explicit type keys are another way to specify locking semantics. This all gets us one step closer to a more formal programming model and to a more correct kernel.)
to post comments)