Sharing time between two computations?
 Stephen Brackin
[
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:  20060205 (19:09) 
From:  Stephen Brackin <stephen.brackin@v...> 
Subject:  Sharing time between two computations? 
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.) Steve Brackin