From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 0FD46D45F for ; Wed, 2 Nov 2005 11:01:34 +0100 (CET) Received: from mx-a.polytechnique.fr (mx-a.polytechnique.fr [129.104.30.14]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jA2A1XYS021610 for ; Wed, 2 Nov 2005 11:01:33 +0100 Received: from argos.lix.polytechnique.fr (argos.lix.polytechnique.fr [129.104.11.2]) by mx-a.polytechnique.fr (tbp 5.3.1/2.0.6) with ESMTP id jA2A1WMC004525 for ; Wed, 2 Nov 2005 11:01:33 +0100 Received: from [129.104.11.153] (pouilly.polytechnique.fr [129.104.11.153]) by argos.lix.polytechnique.fr (Postfix) with ESMTP id C0A274BA1D for ; Wed, 2 Nov 2005 11:01:32 +0100 (CET) Message-ID: <43688C4C.2080606@inria.fr> Date: Wed, 02 Nov 2005 10:52:12 +0100 From: Julien Narboux User-Agent: Mozilla Thunderbird 1.0.2 (X11/20050322) X-Accept-Language: en-us, en MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: The best way to circumvent the lack of Thread.kill ? Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 43688E7D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; sardes:01 inrialpes:01 aschmitt:01 terminating:01 inherently:01 mutexes:01 deprecated:01 terminate:01 macosx:01 arbitrary:01 theorem:01 theorem:01 imho:01 exception:01 computation:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Hi, I just encountered the Thread.kill "not implemented" exception. A google search gives me this answer from Xavier Leroy on the caml weekly news (http://sardes.inrialpes.fr/~aschmitt/cwn/2003.05.20.html) : "The general solution is to avoid using Thread.kill. Terminating another thread at arbitrary times is an inherently unsafe operation: the killed thread may be holding mutexes, for instance. There's a good explanation of the problems in the Java documentation: http://java.sun.com/j2se/1.4.2/docs/guide/misc/threadPrimitiveDeprecation.html explaining why they "deprecated" their equivalent of Thread.kill." Here is the relevant part of this web page : "Most uses of stop should be replaced by code that simply modifies some variable to indicate that the target thread should stop running. The target thread should check this variable regularly, and return from its run method in an orderly fashion if the variable indicates that it is to stop running. (This is the approach that JavaSoft's Tutorial has always recommended.) To ensure prompt communication of the stop-request, the variable must be volatile (or access to the variable must be synchronized)." My problem is that I don't want to pollute my target thread with checks for a variable. Indeed, I am writing a graphical user interface for an automated theorem prover. I have a function f which decides if a theorem is true or not. It can terminate quickly or take ages, and I want to have an "interrupt" button in the graphical user interface so the user can stop the computation if he wants to. I do not want to have GUI related code in the automated theorem proving part of the program, it would not be clean imho. What is the best solution ? start a new process and use the kill at the operating system level ? (to make things even worse I need something which works on linux, windows and macosx) Kindest regards. Julien Narboux