[Prev][Next][Index][Thread]

Re: Memory safe implementations of C/C++

Corky Cartwright writes:
 
> >And this is a perfectly reasonable assumption; they don't have to
> >preserve any particular behaviour when a program is undefined, so they
> >need only check that their optimisation satisfies the following
> >property
> >
> >  program P doesn't exhibit undefined behaviour 
> >
> >    ==> 
> >
> >  (behaviour(P) = behaviour(optimised(P)))
> >
> >This is a strong and very useful assumption, but I don't think it
> >constitutes "ducking" the issue.  
 
> I emphatically disagree since the set of "well-behaved programs"
> (those that never perform unsafe operations) is not recursive.  (In
> fact, it is not even recursively enumerable.)  In practice, it is
> impossible to tell if such an optimization is safe for a given C
> program.  This is the point that Matthias Felleisen was implicitly
> making in the message when "he rested his case".

You only need to be able to determine if an optimisation is safe for a
C program that is assumed not to already exhibit undefined behaviour.
This might be hard, but it doesn't have anything to do with the
problem of determining whether or not the program is well-behaved or
not.  This is because the transformation wrought by the optimisation
on undefined programs is irrelevant.
 
> Such optimizations can only be safely applied to programs for which
> there is a proof that no unsafe operations can be performed.
 
No.  We can apply an optimisation if we can prove that it preserves
the behaviour of well-behaved programs.  This may require us to prove
that our new, optimised program is well-behaved, but this is likely to
be relatively easy in the presence of the assumption that the original
program is well-behaved.

In particular, we absolutely don't need to have the much stronger

  behaviour(P) = behaviour(optimised(P))

If an optimisation is safe for a well-behaved program, we can apply
it.  And this license is precisely why the standard requires nothing
of undefined programs; it makes compiler writers' lives easier.  

If we make an ill-behaved program well-behaved with our optimisation,
we will confuse the author of the program, but our optimisation is
still legitimate.  It's up to the author of the program to make sure
that their program is well-behaved.

Michael.
References: