4 ms·
Not all debug tools are single step debuggers. There are memory verifiers, formal proof techniques and self testing frameworks that Linux uses that are very, ve
by albinofrenchy 11y ago
Not all debug tools are single step debuggers. There are memory verifiers, formal proof techniques and self testing frameworks that Linux uses that are very, very useful
- xjia 11y agoWhat are those tools?
- colin_mccabe 11y agosparse -- adds annotations to kernel code which can be checked by the compiler. It is a little bit like a parallel type system which provides domain-specific knowledge like "this function takes lock A and then lock B" or "this function runs in interrupt context." See https://sparse.wiki.kernel.org/index.php/Main_Page https://sparse.wiki.kernel.org/index.php/Main_Page kmemcheck -- sort of like valgrind, but for the kernel. CONFIG_FAULT_INJECTION -- inject random faults at runtime (such as in memory allocation) to test infrequently encountered error paths. CONFIG_DEBUG_MUTEXES, CONFIG_DEBUG_SPINLOCK -- run expensive mutex validation checks at runtime. coccinelle -- a source code matching and transformation engine. You can use it in some of the same contexts as sed or awk. Unlike those tools, it is aware of the C language so it can do smarter things like add an extra final argument to all occurrences of a call to do_foo_bar_baz(). See http://coccinelle.lip6.fr/ http://coccinelle.lip6.fr/ checkpatch.pl -- Checks a patch to see if it conforms to the kernel style guide. Simple things like enforcing 80-column lines, but also more complicated things as well like variable naming, whitespace, etc. smatch, flawfinder -- static analysis tools that are similar in principle to Coverity. Like Coverity, they are unsound, but often helpful.
- xjia 11y agoThanks for the summary. However, what do we have on the formal proof side?