Ben Moseley wrote:
> Thanks for all of the replies.
>
> The answer seems to be that it's the fact that unification can raise
> an exception which introduces the nondeterminism. That seems to make
> sense.... but isn't nondeterminism actually creeping in purely from
> the fact that either thread is allowed to bind the same unbound
> variable - whichever thread gets there first?
>
> I'm left feeling slightly uneasy about a couple of things:
> 1) Since it's the unification procedure which we're talking about it
> basically means that it's not possible to use a truly deterministic
> concurrent subset of Oz - (unless we wrote a new unification procedure
> maybe??)
> 2) The failure of the program could occur at any time - there is no
> way in advance I can tell whether one of my threads will in the future
> attempt to do such an invalid unification - in exactly the same way I
> can't necessarily tell whether any threads calculation will terminate.
> What this means is that it could appear that my program was working
> successfully, and giving one particular answer - and at any point I
> would never know whether it was really just due to "luck"
> (non-determinism) that I had arrived at that answer - I would never
> know if my program was just about to fail with an invalid unification
> - which might have succeeded had the luck/non-determinism gone the
> other way. (Obviously the longer I wait the more certain I'll get -
> but I can never be absolutely certain that the program would behave
> the same way if I ran it again...)
>
> I suppose there aren't really any answers to these points.
>
> The reason I've been thinking about these issues is that I've been
> trying to understand what the practical benefits (and limitations) of
> using a model like the declarative concurrent model would be. I
> suppose that in practice the discipline imposed by that model is useful.
>
> --Ben
Dear Ben,
Let me add a few comments to the previous messages.
Unification failures are very conservative warning bells! If one goes
off, then it
is theoretically possible that there is a deep logic error in your
program, so that
previously calculated results are not right. Only the program didn't
notice it at
that time. That's the blessing and the curse of concurrency: things can
happen
out of order and error detection might be delayed.
But usually things are better than that, because most programs don't use
unification
in such a sophisticated way. E.g., if your program is based on streams,
then it is
usually clear what part has been correctly calculated when the
unification failure
occurs, because there is a clear forward flow of data. It's easy to see
when the
program has gotten past a certain point. So you *can* be "absolutely
certain"
that the results before that point are correct.
In any case, an (unintended) unification failure is a programmer error,
like taking the
square root of a negative number or dividing by zero, and means that
your program
should be fixed!
As a final point, if you're not using the full power of unification,
then a little bit of
static typing can guarantee that unification failures will never occur.
E.g., that
only variable-value unifications are done. The work on Alice, a
statically typed
variant of Oz, is an example of this. It's also possible to add a
little static typing to
Oz and keep the language essentially unchanged. Kevin Glynn is working
on this.
Peter
-
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.