The best way to circumvent the lack of Thread.kill ?

[Julien Narboux <Julien.Narboux@inria.fr>]

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