Re: [Hol-info] polyml thread support

[Tjark W. <tja...@gm...>]

On Sun, 2008-11-09 at 20:29 +0000, Lu Zhao wrote:
> Can I use the thread support in PolyML to do this task? and how? I'd
> like to run a ML function, which runs a HOL proof, for a certain amount
> of time, say 20 seconds, and if the function hasn't terminated by this
> time limit, I want to kill that thread and run the same function again
> with a different parameter. If the thread terminates before the time
> limit, then it reports to its parent thread so that the parent can stop
> the timer and execute another function.

you can.  One approach is to create a monitor thread that sleeps for
(say) 20 seconds and then interrupts your current (worker) thread, which
is executing the function.  A local variable stores either the result of
the computation, or the interrupt exception.

Thread.self, Thread.fork, Thread.interrupt, OS.Process.sleep should be
relevant.

It gets a bit tricky if you want to handle external interrupts properly.
I'm afraid I don't have a working implementation that I could post, but
maybe someone else does.

Best,
Tjark