Re: [Hol-info] polyml thread support
On Sun, 9 Nov 2008, 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 See also the thread "Are timeouts possible in HOL (mosml or poly)?" on this list (August 2008): http://sourceforge.net/mailarchive/message.php?msg_name=E1KOtVj-0008Aq-00%40mta1.cl.cam.ac.uk When working with threads in Poly/M,L I do recommend the latest version 5.2.1. Before there is a problem with GC and internal wait that can produce a deadlock (very rarely). Other examples for working with Poly/ML threads are available here: http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Pure/Concurrent/ Makarius - 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] polyml thread support
On Sun, 2008-11-09 at 20:29 +, 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] polyml thread support
Hey, 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. Thanks a lot. Lu - 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
