Re: [9fans] NUMA

[Bakul Shah <bakul@bitblocks.com>]

On Sun, 17 Jul 2011 09:38:47 +0200 tlaronde@polynum.com  wrote:
>
> Furthermore, I don't know for others, but I prefer correctness over
> speed. I mean, if a program is proved to be correct (and very few are),
> complex acrobatics from the compiler, namely in the "optimization" area,
> able to wreak havoc all the code assumptions, is something I don't buy.

C's design has compromises in favor of speed to correctness
(mainly by underspecifying, by leaving more things upto the
implementor). So if you really prefer correctness over speed,
you should be using Scheme, ML or Haskell etc but not C!

But note that for what C is used for, this compromise is fine
(IMHO). But this has made its semantics significantly more
complex.  C doesn't even have a well defined formal semantics
(there have been attempts to define denotational semantics for
C subsets but never the whole language, and even such a subset
specification is significantly larger than, say, Scheme's).

Also note that the ISA implementations these days are quite
complex (perhaps even more than your typical program).  We
don't see this complexty because it is all hidden behind a
relatively simple ISA.  But remember the FOOF bug? Usually the
vendor has a long errata list (typically only available on a
need to know basis and only under NDA!). And usually they
don't formally prove the implementation right; they just run
zillions of test vectors! I bet you would be scandalized if
you knew what they do :-)

> But how can one rely on a binary that is so mangled that the fact
> that you do not see it fail when testing does not prove it will
> yield a correct result? And, furthermore, that the code is so chewed
> that the proofs of correctness on the source level do not guarantee
> anything about the correctness of the compiled result?

Most all complex programs have bugs. gcc does, clang does, and
so does plan9 cc. The difference is in the degree of
bugginess. One uses the best tool available for a given job
and then learns to work around its problems.

The problem with C/C++ optimization is that these languages
are quite complex and it is not always easy to figure out the
correct equivalent operations under all conditions.  Contrast
that with Stalin which does whole program optimization of R4RS
Scheme programs and does it extremely well (but extremely
slowly!).

> My gut feeling is that the whole process is going too far, is too
> complex to be "maintenable" (to be hold in one hand), and that some
> marginal gains in specific cases are obtained by a general ruin if not
> of the certainty, at least of some confidence in correctness.

I seriously think you will be happier with Scheme!