Nondeterminism (was: Formal semantics for C)

To: Fergus Henderson <fjh@cs.mu.oz.au>
Subject: Nondeterminism (was: Formal semantics for C)
From: Viktor Kuncak <vkuncak@mit.edu>
Date: Tue, 25 Dec 2001 12:00:11 -0500
Cc: types@cis.upenn.edu
In-Reply-To: <200112251446.fBPEk5Q19557@saul.cis.upenn.edu>
References: <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu> <200112231526.fBNFQbM08076@saul.cis.upenn.edu> <200112251446.fBPEk5Q19557@saul.cis.upenn.edu>

Fergus Henderson:

 > A semantics doesn't need to be deterministic.  It can specify a set of
 > possible behaviours.  Indeed for almost all programming languages the
 > semantics is not deterministic.
 > 
 > The semantics for a programming language can also be parameterized
 > (i.e. dependent on certain implementation-defined characteristics).

Hi!

I have a few questions about nondeterminism.

I noticed that nondeterminism can neatly solve the following
problem with languages that have object allocation.

Consider these two pieces of code:

    x = new C
    y = new C
    x.f = y
    y = x

  and

    y = new C
    x = new C
    x.f = y
    y = x

If we model an allocator in a deterministic way
(e.g. incrementing a counter), then these two programs will
not be equivalent even though their states have isomorphic
heaps.  However, if we let allocator nondeterministically
return every possible fresh object identifier, we get that
the two pieces represent two equivalent nondeterministic
programs.

The POPL02 paper by Banerjee and Naumann mentions that some
of the problems can be solved by taking the quotient of the
traces (pp4), but gives no references (and the quotient
solution is not applied in this paper).  What is the right
reference for this technique?  It seems to me that it comes
for free if I use nondeterminism.

@InProceedings{BanerjeeNaumann02RepresentationIndependenceConfinement,
  author =       {Anindya Banerjee and David A. Naumann},
  title =        {Representation Independence, Confinement, 
                  and Access Control},
  booktitle =    POPL02,
  year =         2002,
  obtained = {http://guinness.cs.stevens-tech.edu/~naumann/publications.html}
}

It also seems to me that nondeterminism allows us to use
languages with side effects without fixing an evaluation
model.  I have impression that functional languages try to
avoid such nondeterminism.  Is this because it is general
hard to reason about such semantics?  Having nondeterminism
is nice because it gives us more flexibility in program
refinement.

Thanks,

  Viktor