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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 60C38BBA7 for ; Wed, 8 Feb 2006 18:21:31 +0100 (CET) Received: from orsfmr003.jf.intel.com (fmr18.intel.com [134.134.136.17]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k18HLT51020136 for ; Wed, 8 Feb 2006 18:21:30 +0100 Received: from orsfmr101.jf.intel.com (orsfmr101.jf.intel.com [10.7.209.17]) by orsfmr003.jf.intel.com (8.12.10/8.12.10/d: major-outer.mc,v 1.1 2004/09/17 17:50:56 root Exp $) with ESMTP id k18HLQ6p008474; Wed, 8 Feb 2006 17:21:26 GMT Received: from orsmsxvs040.jf.intel.com (orsmsxvs040.jf.intel.com [192.168.65.206]) by orsfmr101.jf.intel.com (8.12.10/8.12.10/d: major-inner.mc,v 1.2 2004/09/17 18:05:01 root Exp $) with SMTP id k18HL7e1012244; Wed, 8 Feb 2006 17:21:26 GMT Received: from orsmsx332.amr.corp.intel.com ([192.168.65.60]) by orsmsxvs040.jf.intel.com (SAVSMTP 3.1.7.47) with SMTP id M2006020809212631442 ; Wed, 08 Feb 2006 09:21:26 -0800 Received: from orsmsx409.amr.corp.intel.com ([192.168.65.58]) by orsmsx332.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.211); Wed, 8 Feb 2006 09:21:26 -0800 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----_=_NextPart_001_01C62CD4.1718D384" Subject: RE: [Caml-list] Sharing time between two computations? Date: Wed, 8 Feb 2006 09:21:24 -0800 Message-ID: <196F1D996F92CD46A542EA519DB8CE470313A191@orsmsx409> X-MS-Has-Attach: X-MS-TNEF-Correlator: Thread-Topic: [Caml-list] Sharing time between two computations? Thread-Index: AcYqh7TmbkQUz8NVTJ+3PUCyR1MpqQCSRkkg From: "Harrison, John R" To: "Stephen Brackin" , Cc: "Harrison, John R" X-OriginalArrivalTime: 08 Feb 2006 17:21:26.0338 (UTC) FILETIME=[175E4220:01C62CD4] X-Scanned-By: MIMEDefang 2.52 on 10.7.209.17 X-Miltered: at concorde with ID 43EA2899.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 computations:01 johnh:01 ocaml:01 computations:01 more-or-less:01 ocaml:01 iterative:01 xavier's:01 depth-first:01 iterative:01 runtime:01 threading:01 more-or-less:01 xavier's: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=HTML_50_60,HTML_MESSAGE autolearn=disabled version=3.0.3 This is a multi-part message in MIME format. ------_=_NextPart_001_01C62CD4.1718D384 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Hi Steve, =20 | 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 its negative, but the code | doesnt know which, if either, it will be able to prove.) =20 How about setting up some kind of iterative deepening and interleaving the computations, rather than aiming for true parallelism? Assuming that you can already run a computation with a timeout based on Xavier's earlier code, you could do: =20 Computation A for 1 time unit Computation B for 1 time unit Computation A for 2 time units Computation B for 2 time units Computation A for 4 time units Computation B for 4 time units Computation A for 8 time units ... =20 restarting the computations of A and B from scratch each time, until one succeeds. The repetition of work gives a performance hit but it's easy to bound it by a moderate constant factor, depending on how fast you grow the timeslices. =20 The common preference for depth-first search with iterative deepening over breadth-first search in many AI/search applications is based on the same philosophy: the moderate increase in overall runtime from duplicated work can be more than compensated for by the fact that you don't need to store intermediate state to remember where you've been. =20 Indeed, many of HOL Light's automated proving routines like MESON_TAC and REAL_SOS (is the latter what you're using to prove positivity and negativity?) already do some kind of iterative deepening, searching step by step with successively larger bounds on the search space. It wouldn't be hard to decouple the outer loop and interleave the steps, e.g. =20 Step 1 of computation A Step 1 of computation B Step 2 of computation A Step 2 of computation B Step 3 of computation A=20 ... =20 This may be more coarse-grained than what you wanted, but it's better than nothing, and it doesn't need any timeouts or threading. =20 John. ------_=_NextPart_001_01C62CD4.1718D384 Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable
Hi=20 Steve,
 
| Xavier Leroy=20 showed me how to set things up so that an OCaml computation
| is = interrupted=20 after a pre-set time limit to ask the user how long to
| continue. = Now I'd=20 like to do the same thing for two parallel
| computations that I'd = like to=20 have share the time available more-or-less
| evenly. (I'm writing = OCaml code=20 for automatically proving results in the
| HOL Light theorem prover, = and I=20 have a situation where the code needs to
| prove that a value is = positive or=20 prove that its negative, but the code
| doesnt know which, if either, = it will=20 be able to prove.)
 
How about setting=20 up some kind of iterative deepening and interleaving
the = computations, rather=20 than aiming for true parallelism? Assuming that
you can already run a = computation with a timeout based on Xavier's earlier
code, you could=20 do:
 
 Computation=20 A for 1 time unit
 Computation B for 1 time = unit
 Computation A=20 for 2 time units
 Computation B for 2 time = units
 Computation A=20 for 4 time units
 Computation B for 4 time = units
 Computation A=20 for 8 time units
 ...
 
restarting the=20 computations of A and B from scratch each time, until one
succeeds. = The=20 repetition of work gives a performance hit but it's easy
to bound it = by a=20 moderate constant factor, depending on how fast you
grow the=20 timeslices.
 
The common=20 preference for depth-first search with iterative deepening
over = breadth-first=20 search in many AI/search applications is based on the
same = philosophy: the=20 moderate increase in overall runtime from
duplicated work can be more = than=20 compensated for by the fact that you
don't need to store intermediate = state=20 to remember where you've been.
 
Indeed, many of=20 HOL Light's automated proving routines like MESON_TAC
and REAL_SOS = (is the=20 latter what you're using to prove positivity and
negativity?) already = do some=20 kind of iterative deepening, searching step
by step with successively = larger=20 bounds on the search space. It wouldn't
be hard to decouple the outer = loop=20 and interleave the steps, e.g.
 
 Step 1 of=20 computation A
 Step 1 of computation B
 Step 2 of = computation=20 A
 Step 2 of computation B
 Step 3 of computation A=20
 ...
 
This may be more=20 coarse-grained than what you wanted, but it's better than
nothing, = and it=20 doesn't need any timeouts or threading.
 
John.
------_=_NextPart_001_01C62CD4.1718D384--