From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 1CCF5BBA7 for ; Sun, 5 Feb 2006 23:45:12 +0100 (CET) Received: from moutng.kundenserver.de (moutng.kundenserver.de [212.227.126.190]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k15MjB8Y006766 for ; Sun, 5 Feb 2006 23:45:11 +0100 Received: from [212.227.126.160] (helo=mrelayng.kundenserver.de) by moutng.kundenserver.de with esmtp (Exim 3.35 #1) id 1F5sd2-0006Vc-00; Sun, 05 Feb 2006 23:45:08 +0100 Received: from [84.58.133.90] (helo=gate.lan.gerd-stolpmann.de) by mrelayng.kundenserver.de with asmtp (Exim 3.35 #1) id 1F5sd2-0005JI-00; Sun, 05 Feb 2006 23:45:08 +0100 Received: from flakew.lan.gerd-stolpmann.de (flakew.lan.gerd-stolpmann.de [192.168.0.32]) by gate.lan.gerd-stolpmann.de (Postfix) with ESMTP id 2EF32C178; Sun, 5 Feb 2006 23:45:07 +0100 (CET) Subject: Re: [Caml-list] Sharing time between two computations? From: Gerd Stolpmann To: Stephen Brackin Cc: caml-list@yquem.inria.fr In-Reply-To: <0IU800JUPAJW2PB8@vms042.mailsrvcs.net> References: <0IU800JUPAJW2PB8@vms042.mailsrvcs.net> Content-Type: text/plain; charset=iso-8859-13 Date: Sun, 05 Feb 2006 23:45:06 +0100 Message-Id: <1139179506.3912.9.camel@localhost.localdomain> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: quoted-printable X-Provags-ID: kundenserver.de abuse@kundenserver.de auth:a6865a839c0178d9aa0ce41878507ea2 X-Miltered: at nez-perce with ID 43E67FF7.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 computations:01 gerd:01 stolpmann:01 ocaml:01 computations:01 more-or-less:01 ocaml:01 more-or-less:01 computed:01 o'caml:01 unspecified:01 threads:01 gerd:01 stolpmann:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=FORGED_RCVD_HELO autolearn=disabled version=3.0.3 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=FFd like to do the same thing for two > parallel computations that I=FFd like to have share the time available > more-or-less evenly. (I=FFm writing OCaml code for automatically provin= g > 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=FFs > negative, but the code doesn=FFt know which, if either, it will be able > to prove.) Can this be done? If so, then what=FFs the easiest way to do > it? As a special case of this question, for an expression of the form > =B4let x,y =3D f(args1),g(args2)=A1, how does the system allocate time > between the computation of x and y? (If it=FFs more-or-less equally, > then that solves my problem; if one of x or y is computed first, then > the other, then I=FFve 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.=20 Gerd --=20 ------------------------------------------------------------ Gerd Stolpmann * Viktoriastr. 45 * 64293 Darmstadt * Germany=20 gerd@gerd-stolpmann.de http://www.gerd-stolpmann.de Telefon: 06151/153855 Telefax: 06151/997714 ------------------------------------------------------------