Hi Ben,
On 20 Nov 2003, at 09:10, 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?
Yes, it is, since the thread execution order is nondeterministic.
Writing something to an output stream, (like a screen, or a file)
would make the thread-nondeterminism observable, so these kind of
operations are outside the deterministic subset. The same goes for
checking if a variable is (already) determined (IsDet). As you read on
in the book, you will find out about these things.
> 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??)
Unification is very powerful, and it's presence often contributes
substantially indeed to the nondeterminism of other constructs. If we
would not have unification, the non-deterministic subset might very
well include more constructs. But unification is a central construct in
Oz, as are threads, so we're very happy that you have both in a
"declarative" subset. The assembly of the "nondeterministic" subset in
Oz is of course a bit arbitrary, as I'm sure you could find completely
different subsets that guarantee non-observable nondeterminism. But
this one is chosen for its expressive power, and it wouldn't be Oz if
it where different.
> 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...)
You have to wait until the program reaches a state of partial
termination (no threads that possibly ever have effect on the store are
executable).
>
> 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.
Indeed, as it allows the programmer not to worry about a lot of usual
problems when dealing with concurrency: time-of-check-to-time-of-use
differences, locking and deadlocks, race-conditions, etc.
>
> --Ben
>
> On 20 Nov 2003, at 07:30, Raphael Collet wrote:
>
>> 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.
>
-----------------
Fred Spiessens
Researcher Software Security
Université catholique de Louvain
Louvain-la-Neuve
Belgium
fsp@info.ucl.ac.be
http:www.info.ucl.ac.be/people/fsp/fred.html
-
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.