lkml.org 
[lkml]   [1998]   [Aug]   [2]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
SubjectStatic analysis of the Linux kernel
From
Date
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

\
 
 \ /
  Last update: 2005-03-22 13:43    [W:0.171 / U:0.704 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site