Race condition in Search.ozf

[Harmon Nine]

Although the behavior of Search.oz agrees with the documentation, it
still leads to a race condition.  A loop context is most likely where
the "next" method would be called.  That is, its very name implies
repeated calls, most likely within a loop, to get the "next" solution.

A salient factor in this loop is when to stop.  As constraint
calculations can be very time-consuming, when to stop is most likely
going to be based on time, which necessitates a second thread to call
the "stop" method.  This stopping thread could be executed after a
pre-programmed delay, or by an external event, e.g. user input (which is
what our program does).

The current implementation of Search.oz causes an implicit race
condition in this scenario.  We actually tried an approach similar to
that outlined by Yves, i.e. where the "stop" method was called multiple
times (e.g. one call per 500ms) until the stop was confirmed.  However,
such an approach is probabilistic, i.e. the chances that the first
thread hasn't stopped decreases exponentially with each call to "stop"
by the second thread.  This makes it less desirable than a deterministic
approach.

True determinism in this scenario can only be achieved by having the
"stop" method stop any further calculations until an explicit "resume"
method is called.  With such a modification, the documentation would
need to be changed to:

======
stop

             stop

     stops the search engine. Once this method is executed, any call to
next, nextS, nextP, last, lastS, or lastP will return immediately,
binding the argument to the atom 'stopped'.  To resume calculation,
first call the "resume" method, then call next, nextS, nextP, last,
lastS, or lastP.
======

Cheers, :)
-- Harmon

-----Original Message-----
From: hackers-bounces at mozart-oz.org
[mailto:hackers-bounces at mozart-oz.org] On Behalf Of Luis Quesada
Sent: Wednesday, February 01, 2006 9:00 AM
To: hackers at mozart-oz.org
Subject: Re: Race condition in Search.ozf

Harmon Nine wrote:
> 
> If Thread 1 is anywhere else in the loop besides statement (1) when
the 
> 'stop' method is called in Thread 2, the desired behavior is that when

> the loop comes around and executes statement (1), the 'next' method
will 
> return immediately, binding value "stopped" for NextSolution.
> 
I don't think this is a bug. Taking into account the documentation, the 
current behavior is the one that you should expect :

======
stop

             stop

     stops the search engine. The search engine can be restarted by 
next, nextS, nextP, last, lastS, and lastP.
======


I agree with Yves: the idea is to adapt your code so that it is 
consistent with the specification.

Cheers,

Luis

________________________________________________________________________
_________
mozart-hackers mailing list
mozart-hackers at ps.uni-sb.de      
http://www.mozart-oz.org/mailman/listinfo/mozart-hackers