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.