Hi all,
We request your comments on the following proposal for a new model and
implementation of by-need synchronization in Mozart. This model is the
one presented in Peter & Seif's book. It is simple, and more
declarative than the previous definition. The previous definition was
making use of futures, and it turned out that those can introduce
unexpected non-determinism in a program. See the example below.
We would appreciate your feedback on the model presented below. If no
objection arises about the model, the implementation will be part of a
future Mozart release (possibly Mozart 1.3.0), as soon as it is
complete and stable.
1. The problem with the current definition of ByNeed
The following example shows how to make an indeterministic choice with
futures. It uses the fact that the unification of two futures F1 and
F2 blocks. In the example, one of the threads will terminate, while
the other one blocks forever without binding X. Depending on the order
of execution of the threads, X will be 1 or 2.
proc {OneOrTwo ?X}
U
F1={ByNeed fun {$} {Wait _} _ end}
F2={ByNeed fun {$} {Wait _} _ end}
in
thread U=F1 X=1 end % thread #1
thread U=F2 X=2 end % thread #2
end
For more details, consult our paper at
http://www.info.ucl.ac.be/~raph/dlcc.ps.gz.
2. The proposed model
We model a by-need computation as a thread waiting for a logic variable
to be needed. When a logic variable is created, it is not needed yet.
The variable becomes needed as soon as a thread suspends on it, or it
gets determined, or it is bound to another needed variable. Once a
variable becomes needed, it stays needed forever. In other words, the
need is monotonic. No future is introduced in this mechanism. In fact
futures become a completely orthogonal concept. So a variable with a
by-need computation is not protected by default. This makes the
by-need synchronization declarative and conform Peter & Seif's book.
We introduce one new primitive, WaitNeed, and describe Wait and !! in
terms of this new model.
- {WaitNeed X} waits until X becomes needed.
- {Wait X} makes X needed (if necessary) and waits until X becomes
determined.
- {WaitQuiet X} waits until X becomes determined, without making X
needed.
- Y=!!X makes Y a future - read-only view - of X. Unification with a
value or another future blocks. When Y becomes needed, X is made
needed too.
The new definition of ByNeed in Peter & Seif's book is given by
proc {ByNeed P X}
thread {WaitNeed X} {P X} end
end
We can program the previous behavior of ByNeed this way:
proc {ByNeed P X}
Y in
thread {WaitNeed Y} {P Y} end
X=!!Y
end
3. Status and plan of the implementation
Thanks to the help provided by Christian and Kostja, we have
implemented and tested the by-need synchronization mechanism of the new
model, and the first results are encouraging. We created the primitive
WaitNeed, and adapted Wait and WaitQuiet. We are now working on the
implementation of futures. Once this is done, we will be able to
replace the former implementation by the new one. (The old
implementation could be kept available under a different name during a
transition phase, if necessary.)
Thanks for your comments,
Raph & Fred.
-
Please send submissions to hackers@mozart-oz.org
and administriva mail to hackers-request@mozart-oz.org.
The Mozart Oz web site is at http://www.mozart-oz.org/.