Sharing time between two computations?

Stephen Brackin
 Gerd Stolpmann
[
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:  Gerd Stolpmann <info@g...> 
Subject:  Re: [Camllist] Sharing time between two computations? 
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 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 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 moreorless 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 sideeffect free), you can spawn two threads and let the operating system schedule how the CPU is shared by the computations. However: I said REALLY sideeffect 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@gerdstolpmann.de http://www.gerdstolpmann.de Telefon: 06151/153855 Telefax: 06151/997714 