Re: [Gnu-arch-users] Managing changes to projects that use autoconf/automake with tla

[Tom Lord]

    > From: Robin Green <address@hidden>

    > On Tue, Apr 06, 2004 at 08:49:03AM -0700, Tom Lord wrote:
    > > What if the problem were solved tomorrow -- if we could, as you put
    > > it, stick some wings on that fish?

    > > One can only speculate.  I speculate that alternative kernels and libc
    > > implementations would be more viable, that the form and function of
    > > the platform distribution business would shift away from
    > > consolidation, that test-based certification would be more important,
    > > that packages would be significantly less interdependent, and on and
    > > on.

    > Here is my perspective:

    > 1. Integration bugs are always bugs, not "user errors", contrary to some
    > hotheads in the GNU/Linux community. If a dependency specification is
    > missing or inaccurate for package P, this is a bug _in_ package P. If
    > a tarball doesn't contain any dependency specifications, it is probably
    > replete with such bugs :)

Part of the problem here is the layers of authorship.   Most often,
_packages_ (including dependency specs) are authored separately from
upstream _projects_.

So what happens here?   Upstream, somebody creates the dependency.
Maybe they write a Makefile rule with a `-lfoo' or maybe they do
something in configure.in.   Downstream, the package author has to
tease that apart and express the same information, again, redudently.
Version-specific dependencies just add to the hair.

Yes, a package with incomplete or inaccurate dependencies is buggy but
it's a kind of bug that the arrangement of authorship and tools makes
easy to create.

Better would be a c/b/i tool that upstream uses instead of Make rules
or auto* lines or whatever --- one in which the easy way to create a
dependency has the side effect of recording that dependency in a way
that package systems can use directly.   E.g., the easiest way to
cause a "-lfoo" in my linkage or "-I/usr/foo/include" on my compile
line should be (a) easy;  (b) abstract enough that the package
dependencies are expressed in that same act.

We could go on to talk about things like "install auditting" -- same
deal.  The easiest way to write a rule that something should be
installed should, as a side effect, produce accurate information about
what the c/b/i process will install.  It's a drag that the GNU
conventions for make targets never required "make
tell-me-what-will-be-installed".


    > 2. Test-based certification is nice, and a useful stopgap, but
    > proof-based certification with formal methods provides a better
    > quality guarantee of correct operation.

    > Obviously, proof-based certification is a large project. :)

Well, yeah.  Test-based certs is the essense of what we have.  It's
best practice.   

I'm saying: change the relationship of the tests and the
organizational boundaries so that tests are not brand-specific but are
instead a public resource.   Share those costs and benefits the same
way we sell development costs and benefits.

You're saying: advance computer science by 20 years.

Slight difference there.

    > I intend to attack the problem with:
    > (a) a new programming language system with a proof verification system
    > built-in, and eventually
    > (b) a user-mode operating system (like User Mode Linux, but not Linux!) 
with
    > full proof traceability down to at least the host OS.

    > (Last time I mentioned this, Tom told me to go back to the 1960s or 
something
    > ;-)

I hope I didn't embarass myself too much.   You can find your
intellectual progenitors back there.

I would agree that to ingrain proof systems into programming, you're
going to get yourself involved in language design.   Some languages
are more ammenable to useful proofs than others.   The literature here
is abundent but _one_ thing I'll recommend, in case you aren't already
familiar with all the material it discusses, is:

    "Denotational Semantics: The Scott-Strachey Approach to
    Programming Language Theory" Joseph E. Stoy, 1977, MIT Press

That may very well be beneath your current state of knowledge but just
for the general benefit of the list I recommend it as providing both
lots of nitty-gritty about Denotational Semantics _and_ some long
sections relating that to other approaches to understanding
programming languages and proving useful things about programs.  At a
quick glance, the bibliography looks like it points at a pretty good
review of history in this area, too.   Poke around for Dijkstra and
cites of him, too.

You won't be the first to attempt a major system with accompanying
proof.  I recall that some of have been created but I won't embarass
myself by trying to give cites in this area that I'm not current on.
My impression is that there is more existing literature already than
you could read in a lifetime (which is good --- that means that things
like citeseer can help you identify the subset worth reading.)

Anecdotally: in the very early days of arch a big issue for me was the
locking protocol for archives.  I wanted to be certain it was robust
under a wide range of conditions.  It uses just very basic filesystem
operations (rename, mkdir, rmdir, etc.) about which I make fairly weak
assumptions (for example, two concurrent mkdir or unlink calls for the
same directory or file can both succeed -- thanks to NFS).

I wanted to prove that the algorithms used by the locking code could
be interrupted at _any_ time (but with some minor contraints -- for
example, any interruption of a `rename' call means that at least one
of the two names exists --- _historically_ a dangerous assumption but
one that is essential to unix filesystems).

I wanted to prove that the algorithms could be run concurrently in
arbitrary ways, with arbitrary interuptions -- yet the locking
invarients would be upheld.

I did spend a couple of weeks working towards a computer-assisted
proof of the locking protocol.   Actually made progress, even.   But
ultimately I timed out and resorted to proving it to myself, less than
completely formally, on a bunch of scratch paper.

Gosh, I hope it's right.  :-)

-t