User: Password:
Subscribe / Log in / New account

The kernel lock validator

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.)

(Log in to post comments)

The kernel lock validator

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

... 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.

Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds