The kernel lock validator

Posted May 31, 2006 6:59 UTC (Wed) by mingo (subscriber, #31122)
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

The kernel lock validator

Posted May 31, 2006 9:35 UTC (Wed) by nix (subscriber, #2304) [Link] (1 responses)

... and now reiser4 turns up with a tree of locks where each rank may be taken within the rank above safely, but where there are a potentially unbounded number of ranks...

The kernel lock validator

Posted Jun 6, 2006 16:07 UTC (Tue) by nix (subscriber, #2304) [Link]

Hm, on rereading that's not what it does. Sorry.