[Prev][Next][Index][Thread]
Re: More on C semantics / nondeterminism
Greg Morrisett writes:
> Also, as someone else has pointed out, it is possible to
> produce a "memory-safe" implementation of C (see for instance
> Necula's CCured or the previous Safe-C work out of Wisconsin.)
Right! Indeed, the ANSI Standard for C is carefully written to ensure
that such implementations adhere to the standard. The difference
between ML and C is that ML requires implementations to be memory
safe, while C only permits implementations to be memory safe. This
aspect of C is too little appreciated in our community. I only
realized it because I used to work around the corner from Dennis
Ritchie.
Necula, McPeak, and Weimemer's CCured is the first work I've seen that
leaves C nearly unchanged but incurs costs of less than an order of
magnitude (their costs range from 20% to 200%). The sticker is the
"nearly unchanged" -- they do require some source changes, but this
seems to have more to do with convenience of writing the compiler than
with performance or ensuring memory safety. (Someone please correct
me if I have this wrong!) I hope they'll explore a compiler that
accepts all strictly conforming ANSI C -- that may have a much bigger
impact than a compiler that accepts "nearly" all C programs.
Cheers, -- P
-----------------------------------------------------------------------
Philip Wadler wadler@avaya.com
Avaya Labs http://www.research.avayalabs.com/user/wadler/
233 Mount Airy Road, room 2C05 office: +1 908 696 5137
Basking Ridge, NJ 07920 fax: +1 908 696 5402
USA home: +1 908 626 9252
cell: +1 908 872 4436
-----------------------------------------------------------------------
"When a Mathematical Reasoning can be had it's as great a folly to make
use of any other, as to grope for a thing in the dark, when you have a
Candle standing by you." -- John Arbuthnot, 1692
-----------------------------------------------------------------------