Sharing time between two computations?

Sharing time between two computations?

[Stephen Brackin]

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

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.)

Steve Brackin


[-- Attachment #2: Type: text/html, Size: 2282 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
------------------------------------------------------------