Hi all,
I've been working on-and-off on applying various forms of static checking to
the Xen tree. All the stuff I'm doing is based on open source - the
Linux "sparse" checker, "splint", the Linux coding style checker, etc. The
motivation for this work is that the available Free code checkers are
becoming rather powerful; sparse in particular is quite a pragmatic solution
written by Torvalds for checking the Linux source tree and has regularly
found real bugs since its introduction. Using static checkers is perhaps not
as low-effort as switching on compiler warnings but has the potential to
detect rather higher-level errors such as locking bugs, incorrect address
space accesses, unchecked pointer usage, etc.
Eventually I hope this to be useful in rooting out unknown bugs and corner
cases in the Xen tree itself; for now I think a more useful and realistic
goal would be to enhance the process of patch review, both for maintainers
and for code originators, by making certain classes of problems quicker and
easier to spot.
I'm posting here to make people aware of the work that is going on and invite
interested parties to make comments and suggestions or to set up some kind of
collaborative work - patches and suggestions are very welcome at this point
and anybody who is interested in being involved at any level should get in
touch with me at their leisure.
A short digression: another avenue we might want to persue is submitting the
Xen codebase is to look at the www.coverity.com product, to which open source
projects may be submitted for analysis. I'd be happy to try to take this
forward if the core developers are interested. However, I still think it's
worth having an open suite of basic static checking tools that anyone can run
against their patches for immediate feedback.
My public mq tree is at: http://xenbits.xensource.com/maw/xen-checker-queue.hg
I started out doing this in an ordinary Mercurial repository but have since
switched to using the Mercurial Queues extension
(http://www.selenic.com/mercurial/wiki/index.cgi/MqExtension) so you'll want
this extension enabled if you try to clone.
This tree contains a patch queue of various code quality work I've been doing.
Some of it is a bit gross ;-) Current features in the patchqueue include:
* checking of the Xen tree via sparse (splint support should be forthcoming
but it may not work for the moment)
* checking of XenLinux using sparse from the toplevel Xen makefile
(integrating with wider checking under Xen; easily done since linux already
has sparse support. We should sparse check our patches for upstream, too.)
* basic Xen coding style description
* Xen coding style patch checker
* automated test harness to read a load of patches, apply them to a Xen tree
and perform static analysis and coding style conformance testing to each one
in turn (cumulatively) then produce a test report
Features that aren't far off include:
* testing of the tools code, using sparse / splint on the C parts and pylint
(and maybe pychecker) on the Python
* better report summary output
* more versatile commandline controls for the testing harness
* test all the incoming / outgoing changesets relative to a remote hg tree
(use to check a developer tree before requesting a pull)
Potential features that are further off but I'm thinking about:
* an analysis daemon that automatically grabs patches from the mailing lists,
checks them, then either posts back the test reports or sticks them online
somewhere
* hg hooks to auto-run analysis
* add some Xen-related smarts to sparse (or some optional code annotations to
Xen).
Anyhow, any comments welcome, send them to the list, or to me privately, or to
both - whatever makes you happy!
Cheers,
Mark
--
Push Me Pull You - Distributed SCM tool (http://www.cl.cam.ac.uk/~maw48/pmpu/)
_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxxxxxxxx
http://lists.xensource.com/xen-devel
|
Home