Re: Certified C compilers for safety-critical embedded systems

["Robert I. Eachus" <rieachus@comcast.net>]

Chad R. Meiners wrote:

> "Georg Bauhaus" <sb463ba@l1-hrz.uni-duisburg.de> wrote in message

>>Are you sure you can say that a program that implements the Halting
>>problem for a bounded Turing machine does not implement the same
>>problem for a Turing machine?
>
> It depends what you mean by implement.  I tend to think of implementations
> as algorithms (which must halt).  Therefore, since there is no algorithm
> that satisfies the Halting problem's specification (it is undecidable),
> there is not an implementation.  If you want to define implementation as
> something else (reasonable or unreasonable), all bets are off of course.

Excatly, or anyother way of making my point.  All physical machines have 
limits even if someone builds a self-replicating von Neuman system that 
keeps growing itself, it would be limited by the available matter in the 
universe.  But in reality, for realistic time frames even the PC on your 
desk is a sufficiently close approximation to an infinite Turing 
machine.  Does it really matter if I give you an implementation of the 
Halting problem for your PC that will always halt within a trillion 
years, instead of one that does not halt for some inputs? (And are you 
sure, if you had both in hand, you could tell which was which?)

Anyone who works on compiler front end and language definitions has to 
be ready to dance with G�del, decidability issues and the whole nine 
yards.  ANY compiler for a reasonable programming language, and even for 
some unreasonable ones runs right straight into G�del's proof.  It 
either does not accept some legal programs, accepts some illegal 
programs, or never halts for some inputs.  (And as many of you know, 
early releases of compilers tend to do all three.) G�del says that any 
Ada, C, C++, Fortran, or whatever compiler must have at least one of 
those three bugs in it. (In the Ada community, we aim for the first 
choice--that there will be some legal Ada programs that will be rejected 
due to implementation limitations.)

I thought it was wonderful about a decade ago when we made a decision to 
require Ada compilers to solve NP-complete problems--and were honest 
about it. Record representation specifications can be only partially 
specified, and we require the compiler to find a legal layout if one 
exists.  This is of course a bin packing problem, and with not much work 
ANY bin packing or knapsack problem can be mapped to an Ada record 
representation clause.

However, for decades there have been requirements in the Reference 
Manual to solve the Halting problem, but we still dance around saying 
that. In Ada you can write expressions which will be evaluated at 
compile time, and the compiler must decide whether to accept or reject a 
program based on the results of those computations. (Did someone say 
G�del numbers?) I once wrote a joke compiler "benchmark" that used a 
series expansion to compute Pi to 50 places. (Our compiler compiled it 
correctly, but took about 20 minutes.)

Actually Dave Emery and Rich Hilliard a few years later came up with an 
even more torturous compiler test.  I think Dave wrote:

type Positive_Integer is range 0..2**Integer'Last-1;

by accident, and the Verdix compiler just kept churning away.  (Of 
course the last expression was intended to be 2**Integer'Size-1 not 
2**4_294_967_296-1.) I think a number of compilers now check for that 
error by bounding the terms if one gets too large.  In this case once 
you get past 2**32 subtracting one can't bring the final result back in 
range, so you can declare an error and give up.

But there are actually programs in the Ada test suite that depend on the 
fact that A*X-B*Y is a small number for some integers A, B, X, and Y > 
1.  With a computer you can hunt up some pretty nasty expressions that 
require several thousand digits in your arbitrary arithmetic package but 
the final result is say, 13.  Why does Ada require this?  Because it 
allows programs to be written using expressions meaningful in the 
problem domain.  This goes back to the issue of making it easier for 
domain experts to validate designs and implementations.

-- 
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture, 
cell by cell, and victory by victory. Our security is assured by our 
perseverance and by our sure belief in the success of liberty." -- 
George W. Bush