Friday 16 May 2008
Status
Yesterday I gave a talk at Stanford in Dawson Engler's Advanced Operating Systems class. It was a variation on talks I've given before, but with a bit more about open source project issues and spec design issues. I pushed the meme of the virtuoso spec editor, something I hope will spread. I also talked about the economics of error recovery --- the fact that recovering from malformed input, instead of hard failure, is a competitive advantage for client software so in a competitive market it's sure to develop and you might as well put it in specifications.
Today I've been at the Berkeley OSQ retreat. As usual it's a lot of fun hanging out with Berkeley and Stanford students and faculty, plus people from Microsoft, Intel and IBM, talking about software improvement research. I especially enjoy it because I know this community well from my research background, but I also have a lot to contribute from my experiences in the Mozilla trenches.
One point I keep making is that we are pretty good at finding bugs, but we need to improve the fixing process. One part of that is to work on debugging, hence Chronicle. Another part is to apply software verification techniques to patches --- we do care very much about avoiding regressions, so identifying new bugs that would be introduced by a patch would be extremely useful (more useful than just identifying existing bugs in the tree).
Another interesting observation is that we want to avoid bug fixes that increase complexity, if possible. That often means a bug fix involves restructuring code followed by a small fix, where the goal of the restructuring is to allow the fix to be small. We can factor this into two changes, where the first change should preserve existing behaviour. It would be great if we had good tools for checking the first change ... and that actually seems like a feasible goal, since the problem is quite crisply defined and should often be solvable using local reasoning. It would certainly be nice, as a code reviewer, if cleanup patches came with a proof that they do not change behaviour (or at least a statement that intensive automated analysis had failed to uncover any issues).
Comments
Can I ask how this compares with comments like the following on the ES4 mailing list?
"rejecting syntactically invalid scripts is a feature, not a bug" ( https://mail.mozilla.org/pipermail/es4-discuss/2008-May/002862.html )
Which is in response to a request by Hixie for exactly the kind of tolerance you've yourself recommended?
This works because these RTL languages (eg verilog, vhdl) are very much restricted in what they can express.
How much of that expressiveness would a C++ programmer be willing to give up in order to get better automatic provability tools? If C++ had references but not pointers it would be much easier to analyze, but the resulting language wouldn't be acceptable to most existing C++ programmers.
I agree that patches will tend to be localized and thus the tractability of comparing before/after is much better than comparing two programs written independently from the same specification, so even if a limited prover existed, it could still be useful frequently.
Jim: we don't want to restrict the input language very much, not for general browser development. But there's a new generation of advanced white-box testing tools (I'm thinking primarily of mixed-concrete-symbolic techniques) that are really amazing at finding bugs. Sure, it's not full verification, but they add a lot of confidence.
Steve: My slides may not be all that helpful. The "argument" is very simple. If browser A is more lenient than browser B, i.e. there are pages that B rejects outright that A makes some sense of, then (all other things being equal) authors and users will prefer browser A, granting A a competitive advantage. Therefore if the browser vendors are entirely motivated by short-term market share considerations, error recovery will be a desirable feature. (Although in fact, Mozilla at least is not dominated by short-term market share considerations.)
However, I would like to know your thoughts on the benefits and harms of error recovery, even if tentative.
In languages with brittle semantics, such as most programming languages, error recovery has the risk of making your program mean something you didn't intend, so I think most authors would agree that in those domains error recovery is undesirable. (For example, languages like Hypertalk which attempted to have "soft" user-friendly syntax ended up with difficult-to-understand behaviour and authors didn't like them.)
In langauges like HTML where small changes in the document are usually not a big problem, authors seem to prefer error recovery, and I can see that error recovery could be a reasonable way of reducing the cost of development ... although it would be better to simply have better tools for generating valid HTML.
I'm guess I'm undecided about HTML, but it definitely depends on the situation.
For HTML, I believe that errors should be made obvious (e.g. broken image icons and, indeed, 'broken tag' icons), but that they shouldn't prevent innocent users from seeing what the page contains. This is one reason I don't like XHTML.