Re: Formal semantics for C

To: matthias@ccs.neu.edu
Subject: Re: Formal semantics for C
From: Dan Grossman <danieljg@cs.cornell.edu>
Date: Thu, 27 Dec 2001 14:18:43 -0500
CC: fjh@cs.mu.oz.au, kfl@it.edu, types@cis.upenn.edu, S.J.Thompson@ukc.ac.uk, Michael.Norrish@cl.cam.ac.uk
References: <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu> <200112231526.fBNFQbM08076@saul.cis.upenn.edu> <20011225143316.GA2616@earth.cs.mu.oz.au> <200112270341.fBR3fnF18423@saul.cis.upenn.edu>


I agree with most everything that has been said.  As I usually summarize the
matter, "If you don't have memory safety as a foundation on which to build,
you're not going to get very far without sacrificing soundness."  

But just to defend those "terrible" C-analyzers and C-optimizers that punt
on these important issues, they can be quite good at defining their (false)
assumptions clearly, simply, and concisely, which semanticists should agree
is a "good thing".

For example, you can define a quite low-level model of the heap and then
define your model's allocater such that:
* objects are never deallocated
* all objects are allocated infinitely far apart from each other

My point here is small, just that the issues can be skirted in a precise
way.  The model remains inaccurate.

--Dan

Matthias Felleisen wrote:
> 
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> Corky has made the most important points.
> 
> My conjecture is that you probably didn't mean "non-deterministic" but
> indeterminate. Perhaps you're trying to say that all unsafe operations
> should be bottom (denotationally speaking), since we have no
> information about them. This, however, would be a bad mistake that was
> made in the early history of the full abstraction problem. When you
> computation is erroneous, there is information. (You may not like it,
> but it is not absence of information, as bottom would make you think.)
> [See the papers that Corky and I wrote on full abstraction for
> sequential higher-order languages.]
> 
> In C's case the real problem is that you don't even know when to
> specify that your semantics is unspecified without going through an
> extreme detour. Just think about how you would specify that an array
> access is out of bounds. When the array is passed to a procedure, you
> typically don't even have access to its bound. If you do, what exactly
> are you going to say?
> 
> -- Matthias

-- 
| Dan Grossman     www.cs.cornell.edu/home/danieljg H:607 256 0724 |
| 5157 Upson Hall  danieljg@cs.cornell.edu          O:607 255 9834 |

References:

Re: Formal semantics for C

From: Fergus Henderson <fjh@cs.mu.oz.au>