Older blog entries for graydon (starting at number 109)

a few months pass, and many things have happened.

monotone

I switched monotone from a temporal transport model (log replay) to a stateless hashed-index synchronization model. this was an interesting trip into the wilderness of implementing wire protocols. curiously, getting the protocol's shutdown sequence right seemed to be one of the most complicated parts. anyways, now any monotone client is a server, and you don't need to have any shared history with anyone to do a symmetric or asymmetric (push/pull) sync. it seems pretty cool.

I also internationalized it. so now it does localized messages, local filenames, file character set conversions, international branch and tag names, international dns, etc. this was actually kind of fun work; it was especially amusing when it suddenly started returning system error messages to me in german! I can't say I like IDNA much, but it seems to be the consensus. oh well.

free swing

work proceeds reasonably well. we have some other people at work helping on it now, and we have a bunch of widgets working and the ability to make some trivial buttons-and-sliders sort of programs which really work. of course there's still much to do, but things seem to be speeding up. I think we're over the hump.

language wars

as a long time language geek, I can't help but put in a word about the recent threads over language preferences. this is of course a mixture of business and personal thinking, but in the spirit of honesty I figure I ought to lay out my beliefs.

C# and java strike me as a language-war-in-progress between big, old, dangerous proprietary firms. these companies are not blushing virgins; they have a history of fighting dirty fights. we, the free software community in general, should make a conscious policy to stay away from that war. it is one thing to ship cloned toolchains if our customers want them -- how can you say no to a paying customer? -- but we should not write central or critical code in these languages until well after the war is over. that may take decades, it may involve a lot of splintering and pain. it may even involve writing off some huge, tasty programs previously assumed to be "donated" to the community. yes, it sucks. that's the proprietary game and we're all trying to get out of that game. choosing sides won't make it any less painful. we need to abstain.

havoc asks for a compelling high level language platform, and despite my preference for more exotic languages (ocaml, haskell, lisp, ada, eiffel) I have to ultimately rest on the pragmatics I see before me: the high level free software platform in 2004 is C++ and python.

I suspect that high level really means two things these days: lots and lots of libraries, and abstract interfaces which don't involve pointer twiddling. C++ and python meet the bill here. C++ didn't used to, say in 1994, but it's gotten a lot better in 10 years. we have a good compiler for it now (g++ soon-to-be-3.4) and lots of free libraries. if you're careful you can program in it with nary a "*" in your code.

here is my selection; if you haven't read these libraries or used them, honestly, give them a try:

• Boost
• GTKmm
• Netxx
• Botan
• OTL

monotone is self hosting now. I massaged it into playing nice with other network protocols, so now it has this HTTP/CGI server type as well as the netnews one. that's good because people can just set up private depots if they have a web server account, and don't have to bother finding a news server.

I feel like this is a nice milestone. a couple years ago I needed a good free distributed version control tool, and now I have one.

I've been spending the past couple months working on native java2d on cairo. it's kinda fun, a bit of a break from low level stuff. brings back memories of berlin only without the corba and windowing system business, and with a garbage collector. of course, libgcj takes just about as long to link on my modern pentium 4 as berlin did on my "modern" pentium 1, so I guess some things never change.

some things even seem to get worse!

coincidence

lkcl writes that finite group theory can be used to model intelligence and invention; I wasn't aware we had such a simple model for it yet. would you care to share some more of the maths from whence this conclusion (simultineity of invention) "pops out"? perhaps a link to a paper or such?

testing tools

movement asks if free software testing tools are "wild and wooly". I would say some, but not all. I think the unit test things are as good as they need to be; unit testing is more about practise than technology anyways. there's a *Unit library for just about everything now, which is nice.

high-level supervisory and tracking stuff -- say aegis or bugzilla -- is pretty good. maybe if I'm lucky someday I'll be able to say that about monotone too. I think we all know that test cases are the core of the "science" which makes up computer science; the muck you have to slog through to make your software strong against reality.

the mid-level supervisory stuff, however, is weak. dejagnu is Not My Idea of Good (sorry rob) and most people seem content to just cobble together shell or python scripts when they're fed up with expect. testing tools which do automatic breadth or boundary calculations, which estimate and control test-run time, or which do much in the way of environment control and capture, seem disappointingly rare.

one thing which bothers me about test infrastructure is that the posix 1003.3 output format doesn't require (or doesn't often seem to be interpreted as requiring) unique identifiers for each assertion tested. as a result, people wind up measuring not the set of tests passed or failed, but the number. this is wrong in an important way: if I make some fixes and go from 438 failures to 245, it is not at all clear whether I am "193 tests better off" or whether I've fixed 438 and regressed on 245. constructing a QA system on this sort of measurement will be broken by design. it's a bit frustrating. the proper regression relationship is subset, and for that tests need identity.

option processing

I read in innumeracy that people generally mis-perceive coincidence, and that the expected frequency of coincidences (amongst all possible things that may happen to you every day) is pretty high. that may be, but it's still creepy. one day, I'm sitting on a go bus sketching out a design for a C++ option processing library. next day, it gets mentionned here. then I open up gnus and boost announces a formal review period for an option processing library. jeepers. I can feel the axons of the pan-network subcortex creeping into my head just thinking about it.

lexical reproduction

I have an ongoing thesis at the moment which I'm exploring in the programming language literature, which is that programming language features do well (all other things being equal) when they eliminate either distant or dynamic state and replace it with either close or lexical state. the underlying point being that we may favour language features that facilitate copying and modifying small bits of code -- fragments which work in their new context -- as a fundamental programming activity.

exceptions

so along these lines I was thinking about exception handling mechanisms the other day. exceptions are a dynamic control transfer system, or else they are an "error recovery" system, depending on who you ask. I've been browsing around LtU's recent link to crash-only software, the restart system in common lisp, and the checked-vs-unchecked debate in java.

the static checking part really got me curious, because there's a clearly dynamic bit of state that the java designers have tried to patch into the lexical structure of a program, and have mostly failed. nobody likes checked exceptions because the signature of a method needs an exception specification covering the union of all possible dynamic contexts it will find itself in, which is almost always just "Exception". so there's no point.

I think what lexical exception checking -- if you believe in it at all -- ought to do is specify which exceptions will not be thrown from a method. this would at least let the compiler tell you when a particular catch clause is dead code -- probably an error on your part -- and erase it, along with the associated try context setup. that's something, but not much; you may still fail to catch the "right" exception. but at least it works with an open set of possible thrown exceptions, which is the practical fact, most of the time.

but I wonder if this thinking could be combined with crash-only design, so that you have only one throwing-like statement called crash and a conservative type of signature which says whether your method confines crashes (those without the indicator are assumed to propagate crashes). the confining ones can be checked by a compiler; the "confines crashes" bit can be propagated based on static knowledge between caller and callee, so a method which calls only crash-confining methods (and doesn't do any dangerous pointer fiddling or crashable arithmetic) is itself crash-confining; finding the transfer point during a crash is easier; and the call setup would (I think) be a little shorter on crash handling and crash propagating code. you'd still need destructors, of course, and for diagnostic sake you'd still want to collect stack traces and error descriptors. but I think that's a separate issue: using exceptions as cheap debugging vs. using exceptions to help a program keep running in the face of errors are two different things.

unfortunately I don't think you can quite implement this scheme in java or C++ as it stands. they both treat exceptions a little wrong; java will not statically check for handling of unchecked exceptions, hence the name, and C++ ignores (in a horribly fatal way) everything undeclared, unless you declare nothing. both are a bit broken. ah well.

diffs

pfremy writes that diff's output is unintuitive. this may be the case, but his explanation of the two algorithms used is not right.

diff uses a myers LCS method, a careful dynamic programming construct. it is not the fastest known variant, but it is O(ND) time, where D is the size of the minimal edit script, and it finds that edit script. it also has a very important property that you can implement a version which eats only linear space.

python's difflib uses a "junk-sensitive" recursive greedy matcher (documented here) which is apparantly similar in spirit to the Ratcliff-Oberhelp "gestalt pattern matching" algorithm, but with more desirable running time (R-O is quite awful). it does not find minimal edit scripts, and it might -- or might not -- run at competitive speed and space with myers stuff. I can't find any clear analysis.

anyways, there is a lot of literature on string matching. it's one of the huge problems you can lose the rest of your life in. it is certainly possible to improve diff -- I don't want to put you off the cause -- but be sure to do some large tests and background reading before discounting the decisions made in implementing diff.

a couple years back I complained about the state of version control systems. well, about a year ago some friends and I started sketching out ideas for a new one. this week I released a preliminary copy of it. we'll see if it does well. it's a little different, but I think it's got potential.

meanwhile, it's spring! go outside for a walk!

concurrency abstractions

multi-threading seems awkward (and often is) because it makes very pessimistic assumptions about concurrency needs, eg:

• any co-routine might need any/all global resources
• any co-routine's state == an entire stack segment
• any instruction is an equally likely preemption point

while making very optimistic assumptions about concurrency uses, eg:

• threads always co-operate correctly on global resources they share (memory, signals, fds)
• the sharing mechanisms (say, mutexes) are cheap
• threads always re-schedule optimally, at zero cost

when people imply that "state machines are better than threads", they are broadly saying that if you analyze real-world concurrency needs and uses, you will more likely find that:

• a small set of global resources need sharing
• a small set of values makes up a co-routine's state
• a small set of instructions are reasonable preemption points

therefore in these cases the mechanism of "full" multi-threading can be seen to be redundant distraction, providing little advantage over managing some small sets of values by hand. but moreover:

• threads often co-operate incorrectly, due to programmer error, and worse: non-deterministically
• lock contention and context switching is expensive, especially with increasing cache-dependence
• a general thread scheduler doesn't always choose a very good schedule for your threads; your application may well know better

so it can be easy to see threads as worse than merely irrelevant, but in fact truly harmful to your program.

this is not to suggest that multi-threading cannot ever be put to good use. but rather that its default assumptions lead to strangely mismatched programs, which have too many unexpected failure cases associated with the optimistic assumptions, and too many ways to make simple tasks complex in order to meet the pessimistic assumptions.

there have, however, been some interesting systems developed which mix some sort of threads with stronger-than-default assumptions (either in language extensions or programming frameworks) to yield good results. see for example:

• Polyphonic C#, join calculus with a clever syntax, in C#
• JoCaml, join calculus in Ocaml
• Seda, a new Java concurrency toolkit
• ACE, the granddaddy of concurrency toolkits, for C++

technical mutterings

I've heard a lot of people muttering about end-to-end as a design principle of the internet. And they're right: it is important for the internet's protocols to be transparent and use-agnostic. But I seldom see people doing anything about it; we treat the shameful protocols we have as untouchable, and just bolt stuff on without revisiting the design. Network effects seem to ensure that beyond a certain adoption threshold, you simply can't change poor protocols.

I am therefore happy to see two new-ish, and pleasantly simple and transparent protocols being muttered about, in areas which aren't yet completely pinned down: internet backplane protocol and factotum.

chalst

first: I had not previously read hehner's "beautifying godel" paper, but now that you mention it I must say that I disagree with you that it is the "work of an incompetent". I believe the paper illustrates the concept, and does so in a way which is reasonably terse and accessible to a computer programmer, and pleasantly free of the advanced latex, infinite sequent trees, ambiguous notations and ridiculous term encoding which plagued the "logicians presentation" I received in stephen cook's class. I seem to recall him even saying as much during lecture: that a interpretation-oriented presentation, over ascii strings, would probably be much easier to follow. what makes you think of it as incompetence?

second: I certainly do not like working in TCL, since it is so unsafe and more than a little awkward at times; all I'm arguing here is that string manipulation is effectively as powerful as sexp-splicing. I don't see any refutation of this in bawden's paper, merely a preference for the simplicity and "synergy" of the lisp combination. by all means, use a lisp. it's a good system, definitely. personally I prefer something even tighter: camlp4 statically typechecks my metaprograms too. are there any free lisps which do this? I haven't found them. seriously, I'd like such a thing, I just don't have one.

third: yes, camlp4 is a little "fixated" on "source vs. object code"; more accurately you could say that it's "fixated" on pre-run-time static verifications, since you can certainly ship source-only ocaml programs that compile at load-time. lisp's approach doesn't confuse me, it just isn't terribly safe. I happen to like static verifications, and am happy to trade runtime metaprogramming, a feature I do not often want, and freqently want to prohibit, for statically checked compile-time metaprogramming. if you could point me to a good, free, portable lisp with a native code compiler which does typechecking of its metaprograms and their results, and permits custom lexers for the metaprogram input, I'd be happy to investigate it. imho that is ocaml.

tapioca

jdybnis suggests that tests are worse than proofs; by failing to terminate they may make themselves hard to verify since their traces are infinite. I dispute this, since a test is often written within a testing framework which sets a timer and aborts the test after some time. I think tests, test-traces, and proofs are all finite formal objects, simply of varying scope.

mbp raises interesting points. first, that gcc and linux do not always fit common "specifications" of a C compiler and a POSIX kernel. this is worth complaining about, but is not a flaw in a proof of some formal properties of your distcc program, which treats the functions of kernel and compiler as axioms. as mslicker aptly quotes chuck moore: internal consistency can be proved, but compatibility can only be tested.

axiom testing is a different sort of "test" than I was talking about. surely one needs to test that the assumptions going into a proof hold in a particular environment, and those tests should indeed follow the scientific method of attempted falsification.

but I maintain that it's poor use of time to test a program in order to verify some static property you have a good formal theory of. consider gcc: running its larger testsuites takes hours-to-days. in all combinations of host * target arch, with all combinations of configuration flags, it would not finish before you die. and yet verifying the formal property that gcc is a syntactically valid C program, or that it is type-sound, or that every symbol used by a compilation unit has a definition in another, takes only a small factor more time than the i/o required to read it off disk. why is this?

it is because, unlike the (formal) property of "correct translation from C to machine code for architecture X", we have spent time and effort on some of the simpler properties (does-parse, is-typesound, uses-are-defined), and in the process developed the tools to state and verify them statically. applying gcc to other inputs ad nauseum, as a "test" that gcc is a syntactically legal C program, is a total waste of time. you check the static formal property once when the program text changes, and that's it. any more would only tell you that an assumption from the environment is wrong (disk i/o error?), not that the properties have changed.

davidw states that your competition will always outrun you if you bother to stop for proofs. this depends on how ambitious your proofs are; as I suggest above I think there are lots of properties we already prove, and many more waiting behind the scenes which we will have the opportunity to prove in the near future. will we reach a day when we can prove everything interesting about programs? certainly not. such a statement probably has no meaning. but it is instructive, from a business perspective, to consider how much time you spend running tech support, tracking bugs, debugging, issuing errata, etc. and compare it to the investment in various proof techniques. on several fronts, notably with customers who have deep pockets and long memories, I think the economics may favour "more proofs".

finally, mbp encourages me to try distcc, which is a very good suggestion; it's saved my life several times (though it only speeds up verification of formal properties, not the testsuites). fwiw, I'm your anonymous happy customer from june 4th :)