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

Re: Nondeterminism (was: Formal semantics for C)

>[----- 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 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,
>

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