[Prev][Next][Index][Thread]
Re: Nondeterminism (was: Formal semantics for C)

To: Viktor Kuncak <vkuncak@mit.edu>

Subject: Re: Nondeterminism (was: Formal semantics for C)

From: Michal Walicki <mwalicki@csc.calpoly.edu>

Date: Thu, 27 Dec 2001 20:16:55 0800

Cc: types@cis.upenn.edu

InReplyTo: <200112270341.fBR3fbL18402@saul.cis.upenn.edu>

References: <200112251446.fBPEk5Q19557@saul.cis.upenn.edu> <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu> <200112231526.fBNFQbM08076@saul.cis.upenn.edu> <200112251446.fBPEk5Q19557@saul.cis.upenn.edu>
>[ The Types Forum, http://www.cis.upenn.edu/~bcpierce/types ]
>
>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 implementationdefined 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.stevenstech.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,
>
Nondeterminism has been used for modeling and solving this (and similar)
kinds of problems in the context of algebraic specifications for about 10
years. I do not have the very first references (which contained the
treatement of the example you mention) but you can check some more recent
items:
@InProceedings{ADT,
author = {Michal Walicki and Sigurd Meldal},
title = {Multialgebras, power algebras and complete calculi
of identities and inclusion},
booktitle = Recent Trends in Data Type Specification,
series = LNCS,
volume = 906,
year = 1995,
}
@Article{CS,
author = {Michal Walicki and Sigurd Meldal},
title = {A complete calculus for the multialgebraic
and functional semantics of nondeterminism},
journal = ACM ToPLaS,
volume = 17
number = 2
year = 1995,
}
An overview of earlier techniques can be found in :
@Article{CS,
author = {Michal Walicki and Sigurd Meldal},
title = {Algebraic Approaches to Nondeterminism
 an Overview},
journal = Computing Surveys,
volume = 21
number = 1
month = March
year = 1997,
}
Regrads
Michal