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

Re: Nondeterminism / formal semantics of C

> > Matthias Felleisen writes:
> > > The question that I have is what does it mean to have a semantics
> > > of C?  In my mind, a semantics is a mathematical model that
> > > predicts the behavior of a program in some programming language.
> >
> > > Unless you nail down the precise hardware, os specs, compiler
> > > specs, I can't see how one can possibly specify the semantics of
> > > C. One could specify a very small kernel of C, but as soon as
> > > you admit arrays you're not going to produce anything that will
> > > predict the behavior in a reliable manner.
> >
> > I apologise if this sounds as if I'm belabouring the point, but the
> > C Standard explicitly defines the notion of a "strictly conforming
> > program", one whose execution is guaranteed to produce the same
> > behaviour on all platforms.
> >
> > Other programs might be guaranteed to work, but because of
> > non-determinism will give different answers in different
> > circumstances.  Other programs are beyond the pale.
> >
> > A formal semantics for C would classify programs according to the
> > above, allowing you to predict, for example, that program X will
> > always run, producing the answer 42; will run, producing a number
> > in the range 10-15; or that it's illegal, and that its behaviour
> > is thus unpredictable, or at least, completely dependent on the
> > vagaries of the implementation.
> >
> > Michael.
>
> Excuse my ignorance, but is the Standard's notion of "conforming
> program" a decidable notion?  If so, is your semantics accompanied by
> an algorithm?
>
> -- Matthias

It seems pretty clear that the standard's notion of a conforming program
is one that cannot get to a particular "undefined" state that is entered
when, for example, an out-of-bounds array pointer is dereferenced. I see
no reason why such an operational semantics cannot be defined. To do so,
we don't, contrary to Matthias's assertion, need to know about details
of the operating system or the heap layout in order to get a semantics
that is sufficiently detailed to capture the behavior of conforming
programs.

Determinism is overrated.  Nondeterminism in the operational semantics
is a good thing because it makes it easy to compile better code. Java
makes evaluation order deterministic, but this doesn't save programmers
from bugs because normally they don't think about evaluation order
anyway. In the places where Java (rather arbitrarily) refines a
computation to just one of the evaluations that would have been possible
in C, it's just as likely that the programmer didn't expect the result
that happens to pop out.

The problem of whether C programs are conforming is clearly
not decidable in general. But this misses the point. We don't
need a decision process; we just need to be able to show that
particular programs that we are interested in are conforming,
or deterministic. This should be the goal of the C semantics
discussed. That the semantics fails to identify all conforming or
deterministic programs as such is not necessarily troubling as long
as it is precise enough that programs of interest can be shown to be
conforming. Because skilled C programmers can write conforming programs,
I am sure that this goal is attainable.

Cheers,

-- Andrew