Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
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-05 (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 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