Messages in this thread | | | Subject | Static analysis of the Linux kernel | From | Francois-Rene Rideau <> | Date | 01 Aug 1998 19:16:29 +0200 |
| |
Dear Linus and Kernel hackers,
torvalds@transmeta.com (Linus Torvalds) writes: > Well, if we had a static analysis tool we'd obviously be able to track a > lot of things that we can't currently track. You could build a tree of all > calling sequences, and statically verify quite a few rules. You might not > prove correctness, but you could find a lot of things like this. > > Dreaming? Yes.
One valuable tool might be Tom Lord's ctool, a tool for "Application Specific Static Code Checking for C Programs", written in systas Scheme (a near cousin of GUILE). It is available from ftp://ftp2.lanminds.com/lord/twaddle.tar.gz as well perhaps as from ftp://emf.net/users/lord/ It has been used to verify the behavior of the C implementation of systas itself with respect to a few GC invariants, which can be viewed as whole-program (inter-file) mutual exclusion analysis thru generation of critical-section-aware, longjmp-aware, global call graph. So this technology (be it ctool or a similar tool) could probably be used to verify mutual exclusion for the Linux kernel.
One major problem I see is that ctool (and all non-trivial C analysis tools I know) can only handle code that is already preprocessed, because of difficulty of #conditional analysis, of the horrid general-case macro-replacement analysis, and the abominable combination of them (since depending on conditional macro definition, the parse tree may be significantly different, though I believe this should not be the case in cleanly-written code like Linux should be). This means that unless we write a better tool that's CPP-aware (which is not trivial), we can only analyze preprocessed source trees that are valid in a particular configuration.
This may or not be a problem: we'd most likely need separate analysis for UP and SMP, anyway. And other tools working on preprocessed trees only (like the Tempo partial evaluator) have proved quite useful, too. ctool might also require some massaging to work with inline assembly and other extensions used in Linux (initfunc, asmlinkage, etc), but that's rather the easy part. In any way, static analysis of Linux is by no means a trivial task, but if seriously undertook, it may well be worth the work. Any academic research laboratory interested?
[Personal plug: as I see it, the shortcoming is due to the choice of C as a kernel programming language: C is intrinsically non-modular, and disallows any kind of abstraction, except through its very ill-designed string-based preprocessor. Now, Linux is bound to C, at least for version 2 and most certainly for version 3, and it's not clear what other language would fit kernel development. Actually, Modula-3 and ML are interesting alternatives, since they both have been used to build actual OS kernels, (SPIN and FOX respectively). The ML-with-regions extension to ML also allows to combine higher-order functions with static bounds on memory management, which may be very valuable to kernel designers. Now, this means either a different (parallel) OS project, or a tool to translate existing code into the chosen cleaner language, hence lots of work anyway. See TUNES for a project that is kind of both of these]
PS: I know one guy who wanted to do static bounds-checking analysis for the Linux kernel as his PhD thesis, but he had to stop that thesis.
## Faré | VN: Уng-Vû Bân | Join the TUNES project! http://www.tunes.org/ ## ## FR: François-René Rideau | TUNES is a Useful, Not Expedient System ## ## Reflection&Cybernethics | Project for a Free Reflective Computing System ## Greenspun's Tenth Rule of Programming: any sufficiently complicated C or Fortran program contains an ad hoc informally-specified bug-ridden slow implementation of half of Common Lisp.
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.altern.org/andrebalsa/doc/lkml-faq.html
| |