Hi Steve,
 
| Xavier Leroy showed me how to set things up so that an OCaml
computation
| is interrupted after a pre-set time limit to ask the user how long to
| continue. Now I'd like to do the same thing for two parallel
| computations that I'd like to have share the time available
more-or-less
| evenly. (I'm writing OCaml code for automatically proving results in
the
| HOL Light theorem prover, and I have a situation where the code needs
to
| prove that a value is positive or prove that its negative, but the
code
| doesnt know which, if either, it will be able to prove.)
 
How about setting up some kind of iterative deepening and interleaving
the computations, rather than aiming for true parallelism? Assuming that
you can already run a computation with a timeout based on Xavier's
earlier
code, you could do:
 
 Computation A for 1 time unit
 Computation B for 1 time unit
 Computation A for 2 time units
 Computation B for 2 time units
 Computation A for 4 time units
 Computation B for 4 time units
 Computation A for 8 time units
 ...
 
restarting the computations of A and B from scratch each time, until one
succeeds. The repetition of work gives a performance hit but it's easy
to bound it by a moderate constant factor, depending on how fast you
grow the timeslices.
 
The common preference for depth-first search with iterative deepening
over breadth-first search in many AI/search applications is based on the
same philosophy: the moderate increase in overall runtime from
duplicated work can be more than compensated for by the fact that you
don't need to store intermediate state to remember where you've been.
 
Indeed, many of HOL Light's automated proving routines like MESON_TAC
and REAL_SOS (is the latter what you're using to prove positivity and
negativity?) already do some kind of iterative deepening, searching step
by step with successively larger bounds on the search space. It wouldn't
be hard to decouple the outer loop and interleave the steps, e.g.
 
 Step 1 of computation A
 Step 1 of computation B
 Step 2 of computation A
 Step 2 of computation B
 Step 3 of computation A 
 ...
 
This may be more coarse-grained than what you wanted, but it's better
than
nothing, and it doesn't need any timeouts or threading.
 
John.