RE: [Camllist] Sharing time between two computations?
 Harrison, John R
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Harrison, John R <johnh@i...> 
Subject:  RE: [Camllist] Sharing time between two computations? 
Hi Steve,  Xavier Leroy showed me how to set things up so that an OCaml computation  is interrupted after a preset 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 moreorless  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 depthfirst search with iterative deepening over breadthfirst 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 coarsegrained than what you wanted, but it's better than nothing, and it doesn't need any timeouts or threading. John.