Oz and Mozart Users Mailing List

Re: Observable Non Determinism in the declarative concurrent model? (CTM)


From: Christian Schulte (schulte@imit.kth.se)
Date: Thu Nov 20 2003 - 17:24:33 CET


Raphael,

careful here, what you say is not correct: The store always maintains the
invariant that it is consistent. That is one of the most fundamental
invariants in how Oz is constructed. Many papers on Oz iterate the point
over and over again. And, of course, there is no such notion as they entire
computation fails (as we are talking toplevel computations).

Ben is absolutely right in noticing that programs using unification and
concurrency are non-deterministic. And everybody else has been absolutely
right in pointing out that as long as a program satisfies the invariant
(which Raphael rightly identifies to be most often the case) that if the
program attempts only at most one binding to an unbound variable, this
cannot happen.

But I also have to congratulate Ben to his very sharp insight that testing
concurrent programs is very hard and that failure can occur indeed at any
time!

Cheers
Christian

"Raphael Collet" <raph@info.ucl.ac.be> wrote in message
news:200311200730.hAK7Uw68016261@sampo.info.ucl.ac.be...
> Hi Ben,
>
> > A question has occurred to me whilst reading the Concepts Techniques
> > and Models book...
>
> (snip snip)
>
> > But isn't there observable nondeterminism in the declarative concurrent
> > subset of Oz by exactly the same argument:
> >
> > declare C
> > thread
> > C=1
> > end
> > thread
> > C=2
> > end
> >
> > ... with this example you cannot tell in advance which value C will be
> > bound to. Certainly the other binding attempt will fail, but isn't this
> > observable nondeterminism nonetheless?
> >
> > I expect there's a flaw in my argument somewhere - but I can't see it...
>
> The flaw is that you assume that your program terminates normally. But
> the binding that fails makes the whole computation fail! All you can
> observe is a failure, actually. The final store contains no consistent
> information.
>
> In the stateful case, your program successfully terminates. The final
> store of your program mentions a cell that contains 1 or 2.
>
>
> Cheers,
>
> raph
> -
> Please send submissions to users@mozart-oz.org
> and administriva mail to users-request@mozart-oz.org.
> The Mozart Oz web site is at http://www.mozart-oz.org/.
> Please send bug reports to bugs@mozart-oz.org.

-
Please send submissions to users@mozart-oz.org
and administriva mail to users-request@mozart-oz.org.
The Mozart Oz web site is at http://www.mozart-oz.org/.
Please send bug reports to bugs@mozart-oz.org.



This archive was generated by hypermail 2b29.