RE: [Caml-list] Sharing time between two computations?

RE: [Caml-list] Sharing time between two computations?

[Harrison, John R]

[-- Attachment #1: Type: text/plain, Size: 2324 bytes --]

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.


[-- Attachment #2: Type: text/html, Size: 4996 bytes --]

Re: [Caml-list] Sharing time between two computations?

[Gerd Stolpmann]

Am Sonntag, den 05.02.2006, 14:09 -0500 schrieb Stephen Brackin:
> 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 it’s
> negative, but the code doesn’t know which, if either, it will be able
> to prove.) Can this be done? If so, then what’s the easiest way to do
> it? As a special case of this question, for an expression of the form
> “let x,y = f(args1),g(args2)”, how does the system allocate time
> between the computation of x and y? (If it’s more-or-less equally,
> then that solves my problem; if one of x or y is computed first, then
> the other, then I’ve still got a problem.)

Yes, you have. O'Caml does not parallelize computations, it does just
one thing after the other (here in an unspecified order).

If your computations do not mutate any global value (i.e. are really
side-effect free), you can spawn two threads and let the operating
system schedule how the CPU is shared by the computations. However: I
said REALLY side-effect free, and that has to be valid not only for your
own code but also for all functions you call (e.g. consider functions
with hidden caches that pretend they are pure but actually aren't).

Otherwise I do not see any practical solution for your problem. 

Gerd

-- 
------------------------------------------------------------
Gerd Stolpmann * Viktoriastr. 45 * 64293 Darmstadt * Germany 
gerd@gerd-stolpmann.de          http://www.gerd-stolpmann.de
Telefon: 06151/153855                  Telefax: 06151/997714
------------------------------------------------------------