English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
RE: [Caml-list] Sharing time between two computations?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-02-08 (17:21)
From: Harrison, John R <johnh@i...>
Subject: RE: [Caml-list] Sharing time between two computations?
Hi Steve,
| Xavier Leroy showed me how to set things up so that an OCaml
| 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
| evenly. (I'm writing OCaml code for automatically proving results in
| HOL Light theorem prover, and I have a situation where the code needs
| prove that a value is positive or prove that its negative, but the
| 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
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
nothing, and it doesn't need any timeouts or threading.