Older blog entries for mbp (starting at number 226)

[nevermind]

I reviewed the linux.conf.au papers, and put up a little advogato article regarding it. (This is for people, like me, who only read recentlog.) The standard this year should be excellent.

There are so many things I want to fix in the build system at work and not enough time.

Christian Reis wrote a good paper contrasting XP and open source.

proofs I think some confusion is caused by the two different meanings that "proof" has in English. One is to "establish beyond all doubt", and the other is "mathematical argument".

I was recently saying that software cannot be established beyond doubt to be correct, in part because we cannot really completely define "correct" for practical programs. You can make an argument that nothing can ever be proved absolutely beyond doubt, only contingently.

On the other hand, raph and graydon correctly point out that formal arguments can be useful in trying to establish confidence, and I certainly agree with that.

I think there is less of a gap between quotidien testing techniques and proof than some people on both sides of the gap might suspect.

From: Anonymous-Remailer@See.Comment.Header (Simon Malantrap)
Subject: Who is Stephen Kapp?
Date: 18 Sep 2002 15:37:03 -0000
To: mbp@sourcefrog.net
Comments: This message probably did not originate from the above address.
        It was automatically remailed by one or more anonymous mail services.
        You should NEVER trust ANY address on Usenet ANYWAYS: use PGP !!!
        Get information about complaints from the URL below
X-Remailer-Contact: http://www.privacyresources.org/frogadmin/

 
 Stephen Kapp was the "president" of the UK virus writing team "ARCV"



 
 Here's a quote from "The Risks Digest - Volume 17: Issue 16 Friday 2 June 1995":


 
 "In 1993, another English virus writer, Stephen Kapp, was arrested in connection
with telephone fraud charges. Kapp was known as the "President of ARCV," or
ARCV virus writing group which stood for Association of Really Cruel Viruses."  


 
 Just do a websearh for "Stephen Kapp ARCV virus" and all will be told!



 
 Now you *know* why a bastard like this ripped off your code.



 
 Regards,



 
 A well-wisher...

(The RISKS article mentions another previously prominent virus author, Clinton Haines, who I knew a little in Brisbane. He died of a heroin overdose a while ago.)

Seeing is deceiving. It's eating that's believing. -- James Thurber

I'm surprised by graydon being annoyed at the statement that it is impossible to be completely sure that a program is completely free of bugs.

graydon describes bugs as being states that we do not want to reach, and he suggests that we can do proofs to demonstrate that the program does not reach them. I agree that this is useful, however: (a) proofs alone cannot demonstrate that a program will not reach a bug state, and in fact (b) nothing can demonstrate that beyond doubt.

We always have an imperfect understanding of the way our system will behave in the real world. Therefore we are not able to completely identify ahead of time which states ought to be considered bugs, let alone which bugs are most important.

For distcc, I've tried to make a good effort at both demonstrating ahead of time that the design would work, and also at testing it thoroughly. However, during the course of testing I discovered a kernel bug and an undocumented behaviour in gcc, amongst other things. distcc has a bug because it needs to work around these limits.

These are states which turn out to be bugs but which were initially believed not to be. Unless we make unrealistic assumptions of omniscience, then really I don't see how these could have been discovered other than through testing. (This is even more serious in Samba, where the protocol it's meant to perform is undocumented and very complex.)

Let me try to state it more precisely. Represent our program as a function f(i) => o from input to output -- for interesting programs, the input and output will be large ensembles of values, and so are astronomical in number. Now define a correctness function cf(i), which is true for inputs where f is correct.

The proposition P is that "there are no bugs in program X", which is to say that for every i, cf(i) is true. As I understand it, Popper's point of view is that we cannot ever be sure that we have proved P is universally true. There are too many inputs to examine them all, and if we make a theoretical argument it may be flawed, or it may not correspond to reality. Some people disagree with him.

Rather than trying to gain confidence by piling up evidence in favour of P, Popper says that it is better to try hard to falsify it, either by finding inputs for which is is not true, or by showing that P is internally inconsistent. Considering formal description of f is one good way to find ways in which it is not always correct.

Popper describes science as a stepwise process of formulating theories and then trying to falsify them. This seems broadly like the way people do software. However, perhaps we can do better science by making programs which better support falsification by either tests or proofs. For example being well factored, well documented, and deterministic helps both approaches. Popper's results don't stop us finding scientific theories that are both useful and also almost certainly true. Similarly, never being absolutely sure that a program is bug free ought not to discourage use from developing good software and being appropriate confident in it.

minor bug

Every year in developing countries, a million people die from urban air pollution and twice that number from exposure to stove smoke inside their homes. Another three million unfortunates die prematurely every year from water-related diseases. [The Economist]

Wow. (Yes, I am taking those numbers with a grain of salt, and yes, everybody has to die of *something*, but still.)

giants, shoulders of

graydon, you might like distcc. It's somewhat similar to your doozer program, but perhaps a bit faster (in C, not Perl) and easier to set up (it doesn't need a shared filesystem). (Or perhaps not.)

raph refers to Djikstra's famous quote that "testing can only show the presence of bugs, never their absence."

This rather reminds me of Karl Popper's sensible and insightful arguments that scientific theories can never be proved, only disproved. No number of experiments can prove that F = mg, or that there are no bugs in TeX. However, one (valid) case in which gravity is not proportional to mass demands that the theory be discarded or improved.

This leads at first, to a kind of intellectual nihilism: we can never know anything about the outside physical world absolutely for certain.

However, as Popper pointed out, it is reasonable to gradually gain confidence in a theory as people try and fail to disprove it. People attacking a theory have several possible strategies: they can find experimental conditions under which it fails, or they can demonstrate that the theory is inconsistent with itself or some other theory, or they can perhaps demonstrate that the theory is "unfalsifiable": not amenable to reasonable testing. The proposition that there is an undetectable invisible tiger in my study falls into this category: it may or may not be true, but it is certainly not scientific.

Quantifying the level of confidence is hard, but broadly this method seems to work reasonably well. The more bona-fide attacks that a theory survives, the stronger it appears -- but of course never above reproach.

So Dijkstra and Popper would agree that we can never prove that a program has no bugs. But (from my limited knowledge of them) Popper seems to have some more useful ideas about how as non-omniscient humans, we can rationally gain increased confidence.

Neither empirical methods (e.g. testing) or theoretical methods (e.g. proofs) ought to be privileged. In either case, it is possible that the trial might be carried out incorrectly, or that it may not be as strong an attack as was thought. Both have their place. In addition, the boundary between them is not entirely clear: experiments are formulated from theory, and theory is based on previous experiments. So for example, in software, we can annotate with preconditions and postconditions, as in Eiffel. This stands neatly between empirical measurement and reasoning.

Theoretical proofs have the advantage that they build upon extremely well-established mathematical theorems. But they do perhaps have the disadvantage that they can't test the program fulfills its real-world requirements in the same way that, say, interactive free-form testing can.

Tests, obviously, ought to be designed to prove that the program is *incorrect*. It's too easy to construct experiments which confirm a theory, but Popper would say that they are worthless, particularly if designed by the theory's author.

So it seems to me the crucial question of testing is "how can we economically produce the most excruciating tests?" I think there is a body of knowledge about this which is not really completely captured, by either the XP people or the QA theory people.

One well-known approach is to write test cases for bugs when they're reported and perhaps before they're completely diagnosed. We know that there is some kind of weakness in that area: possibly trying out different tests will discover a related fault.

Another one I have been thinking about recently is "defect injection". Suppose you intentionally temporarily change a line of code to be incorrect -- off-by-1, for example. Do your tests catch the mistake? If not, they're obviously too weak. If you injected 100 mistakes, how many would be caught? That gives some idea of the strength of testing. If you have everything in CVS, and a good "make check", then doing this is actually pretty easy.

Now this is all very well in theory, but in practice humans get attached to their ideas, and don't want to see evidence that contradicts them. This applies to programmers and scientists alike.

Knuth is supposed to have had a comment along the lines of

(* WARNING: I have only proved this code correct, not tested it. *)

gc

raph, Java's bytecode system allows the implementation to use any garbage collection system it wants, from never-free through refcounting through to a mark-and-sweep gc. Various different ones might be appropriate depending on the target: for short-lived tasks, or v0.1 interpreters, being able to use a simpleminded gc is very nice. The "generational gc" that was current last time I looked behaves a lot like Apache pools.

All of this is done with no compile-time knowledge, and with a C API that looks a lot like Python's.

(Perhaps I'm wrong, it is a long time since I looked.)

The Linux kernel map that I did with Rusty and Karim Lakhani is now up on OSDN.

On the one hand, I'm pretty happy with how it turned out, and that its performing pretty well under heavy load. On the other hand, I find it a bit strange that BCG wanted to do it when the map is pretty, but not actually useful as a way to navigate or understand the kernel.

Amongst all the usual garbage on Slashdot there were at least three insightful comments: why is BCG interested in open source hackers?, and here, and here.

In non-geeky news, the Blue Penguins are through into the semi-final of our netball competition. (Well, ok, the name is maybe a bit geeky.) We'll probably get slaughtered, but it's still a big improvement from last year.

I think I indirectly found a kernel bug in 2.2 about FIN_WAIT1 handling with TCP_CORK.

I am rewriting some inner-loop Python code into C to make it faster. The Python C API is really nice; similar to JNI and much easier than Perl.

Some time ago Zaitcev asked how I would map from this C code to exceptions.

int foo() {
    do_something();
    if ((x = bar()) == NULL) goto error_bar;
    if ((y = baz()) == NULL) goto error_baz;
   .......

     // undo_baz();
error_baz:
    undo_bar();
error_bar:
    undo_something();
    return -1;
}

I think this is an excellent example of something better handled using exceptions.

The intention of the code, assuming I'm reading it the way Zaitcev intended, is that we need to either have all operations succeed, or have them all rolled back. I think you can understand exceptions much better if you think about intentions.

That implies that on the failure case, we want to have all the appropriate undo operations called.

I'm going to assume that bar() and baz() raise exceptions rather than returning NULL to indicate errors, because that's generally a better pattern in a language with good exceptions. (C++ is not necessarily included in that class.) You could do it the other way.

One way you might write it is like this:

int foo() {
    Object x = null, y = null;

     do_something();
    
    try { 
	x = bar();
	y = baz();
    } finally {
	/* if we didn't complete, roll back */
	if (y == null)
	    undo_baz();
        if (x == null)
	    undo_bar();
    }
}

I think this fits pretty well with the intended of finally being to do clean up work. (Conversely, catch is for handling errors.) But you could write it either way.

Doing it this way has the advantage that the normal case where no errors occurs appears as straight-line code without being cluttered by error handling. Also, the error is always propagated back correctly, without needing a errno temporary variable to hold it, assuming you want more information than just "-1".

My main point is not that one is better than the other, but rather that they are isomorphic. If you are comfortable with good error-handling idioms in C, then you can quickly learn to use exceptions well.

Zaitcev's friend who said that finally almost always indicates a bug is probably correct; certainly I have found that to be true in some code. However, I think that's not because the language is poorly designed but rather because it's poorly understood. That's what I was hoping to eventually help.

don marti links to wise advice on dealing with Chinese spam.

Busy writing an essay on the DMCA. (Isn't everyone? Yes, but perhaps this will reach a new audience.)

Cold and rainy in Canberra.

One of the nicest things but least obvious things about Python is that the C interface is really straightforward and easy to use. At work I'm moving a frequently-called Python function into C, and it's pretty easy, though it does turn out to be a bit more verbose than a plain C implementation.

I suspect you're bored of me whining about Clearcase, so I'll defer that at least for a couple of days. I do however have something potentially interesting to say on the topic of "a poor workman blames his tools."

joelspolsky recently linked to an entertaining transcript of bruce schneier talking about open source. A few comments:

* slashdot's group mind would get enormously fixated on joel being a fag. oh wow. nothing like slashdot to reacquaint your with the bottom end of the bell curve.

* something about this reminds me of watching performers drinking on stage. there's something about it that reminds me of that arrogant, charming, dissociative, creative frame of mind that a few drinks bring on to a bright person.

* quoting out of context a few paragraphs from a drunk (or conference-speaking) person is in slightly bad taste. it reminds me of watching the Whitlams and worrying that Tim would spill his fifth glass of shiraz on the keyboard. (first child, too responsible, i know.)

* a good conference dinner speech ought to contain roughly equal amounts of flattery, humour, teasing, truth, exageration, rowdiness, ... logic is not particularly needed because you hope your audience will be as deep in their cups as the speaker. i am reminded of the poor bunny at Privacy By Design 2000 who was upstaged by (literally) the Miss Canada contestants filing through the room.

* certainly, in the end free software is futile, lame, derivative, whatever. everything is futile, at least from a certain point of view. everything you think in your life has been thought before (and more clearly, expressed more beautifully); everything you achieve has been done better. the exceptions, if they ever occur, are tainted by the compromises necessary to achieve them. the woman who burns your soul is nothing is nothing compared to Helen of Troy. in the end, that point of view, though objectively true, does not get you anywhere, and there is no point dwelling on it.

* flattering open source people by creating neat Philip Jose Farmer-esque images will get you everywhere

* that certainly applies to you too, Sterling: Gabriel said most of this, and better, before, in his essay on the "slightly bitter quality" of open source. and Gabriel was a pale imitation of Alexander.

* "terrorspace": I hesistated to tie my shoe while walking through SFO customs, and attracted the attention of the security system. i have never before felt more at risk of being shot.

--

And to bjf: relax, and enjoy it. As an unidentified sex therapist said, "if it doesn't feel good, you're not doing it right.". If you think hacking on some free project will help you rediscover why you thought computers were a good idea in the first place then go and do that as a matter of urgency. If going and riding a bike or reading a book or something completely nondigital seems like a good idea then leave strictly at five and do that instead.

One thing I've certainly noticed in my career to date is that the correct answer varies enormously from week to week. Sometimes I just want to hack until 3am. Sometimes I can't stand seeing a computer.

As Richie said, just try to be lucky and everything will work out fine.