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 ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
