Race condition in Search.ozf

[Harmon Nine]

So the program would look something like this?

==========================
Sobj = {New Search.object script(Space OptProc)}

proc {WillContinue NextSolution} {SObj next(NextSolution)} end
proc {WillStop NextSolution} NextSolution = stopped end

P = {NewCell WillContinue}

Thread 1:
proc {GetNextSolution}
  NextSolution
 in
  {@P NextSolution}

  if NextSolution == stopped then
    skip
  else
    Process NextSolution
    {GetNextSolution}
  end

end

Thread 2:
proc {StopThread}
  P := WillStop
  {Sobj stop}
end
==========================

This is a better solution, i.e. it is deterministic in that the call in
Thread 2 to the StopThread proc is guaranteed to (eventually) stop
calculation.  However there's still a race that has a (very small)
chance of causing the calculations not to stop immediately when the
"stop" method is called on SObj.  An immediate termination would be
necessary on receipt of a user input event, or the expiration of a
soft-real-time timer.

Scenario:
@P has value WillContinue
In Thread 1 (top of GetNextSolution proc), @P is dereferenced and thus
WillContinue is called.
Program execution in Thread 1 is now in the WillContinue proc, but
Thread 1 is pre-empted *before* the {SObj next(NextSolution}} call.

Thread 2 fires up on user input event, changes the value of P to
WillStop and calls the stop method on SObj.
This call to the stop method sets the 'isStopped' flag for the Search
object SObj.
Thread 2 is pre-empted.

Thread 1 resumes execution and, in the WillContinue proc, now calls
{SObj next(NextSolution)}.  With the current Search.oz implementation,
the 'isStopped' flag for SObj is automatically unset, and NextSolution
is bound to the next solution for the space, which will take an
undetermined amount of time.
While this is happening, impatient user drums fingers.


The modification to the Search.oz module still looks like the best
solution.


Regards,
-- Harmon

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

Harmon Nine wrote:
> 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).
> [...]

Well, if you are not interested in more solutions after the external 
event, an alternative is to update the order procedure when calling 
Stop. Assuming that you have defined your order as:

P={NewCell "the actual order proc"}
proc {Order Old New}
    {@P Old New}
end

Stop coud be defined as follows:

proc {Stop}
    P:=proc {$ _ _} fail end
    {Sobj stop}
end

So if Sobj gets "stop" first, {Sobj next(NexSolution)} will return 
immediaelly.

Cheers,
Luis


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