From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id XAA26056; Fri, 26 Jul 2002 23:28:51 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id XAA25994 for caml-list@pauillac.inria.fr; Fri, 26 Jul 2002 23:28:51 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA22047 for ; Thu, 25 Jul 2002 10:06:12 +0200 (MET DST) Received: from parsmtp1.rd.francetelecom.com (parsmtp1.rd.francetelecom.com [194.167.105.13]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g6P86BT21719 for ; Thu, 25 Jul 2002 10:06:11 +0200 (MET DST) Received: from lat4148.rd.francetelecom.fr ([10.193.6.100]) by p-grive.rd.francetelecom.fr with SMTP (Microsoft Exchange Internet Mail Service Version 5.5.2653.13) id PQ0BK39G; Thu, 25 Jul 2002 10:06:05 +0200 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----_=_NextPart_001_01C233B2.1FC51480" Received: by lat4148.rd.francetelecom.fr (Postfix, from userid 1014) id EB3C53CC01C; Thu, 25 Jul 2002 10:05:30 +0200 (CEST) X-MimeOLE: Produced By Microsoft Exchange V6.0.5762.3 content-class: urn:content-classes:message Subject: [Caml-list] Coq & Ocaml GC strangeness Date: Thu, 25 Jul 2002 10:05:30 +0200 Message-ID: <20020725100530.D5361@francetelecom.com> Thread-Topic: Coq & Ocaml GC strangeness Thread-Index: AcIzsiBvkF/J55+bEdaOgACAXzHsRg== From: "Cuihtlauac ALVARADO" To: Cc: Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk This is a multi-part message in MIME format. ------_=_NextPart_001_01C233B2.1FC51480 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Hi everybody, This message is mainly addressed to coq mailing list, anyway i'm crossposting to caml mailing list since GC people might be interested. I'm using coq to compute 1 + 1 =3D 2, then 2 + 2 =3D 4, then 4 + 4 =3D = 8, etc. up to 2^20 (with unary natural numbers). Machine used has a 1.7Ghz i686 and 1Gbyte of RAM. It does not swap during the test (starts swaping at 2^21). Here are the timings i get (i'm using tcsh) : ~~>limit=20 cputime unlimited filesize unlimited datasize unlimited stacksize 8192 kbytes coredumpsize unlimited memoryuse unlimited descriptors 1024=20 memorylocked unlimited maxproc 7168=20 openfiles 1024=20 ~~>coqc -opt Limits.v Finished transaction in 0 secs (0.02u,0s) Finished transaction in 0 secs (0.04u,0s) Finished transaction in 1 secs (0.08u,0s) Finished transaction in 0 secs (0.19u,0s) Finished transaction in 0 secs (0.51u,0.01s) Finished transaction in 2 secs (1.49u,0.02s) Finished transaction in 5 secs (5.02u,0.04s) Finished transaction in 18 secs (18.28u,0.03s) Stack overflow ~~>limit stacksize 128m ~~>coqc -opt Limits.v Finished transaction in 0 secs (0.01u,0s) Finished transaction in 0 secs (0.04u,0s) Finished transaction in 0 secs (0.08u,0s) Finished transaction in 1 secs (0.21u,0s) Finished transaction in 0 secs (0.55u,0.01s) Finished transaction in 2 secs (1.6u,0.01s) Finished transaction in 5 secs (5.2u,0.01s) Finished transaction in 20 secs (19u,0.08s) Finished transaction in 79 secs (71.6u,0.24s) Finished transaction in 305 secs (291.24u,0.68s) Finished transaction in 1154 secs (1117.98u,1.16s) =20 ~~>setenv OCAMLRUNPARAM s=3D64M ~~>coqc -opt Limits.v Finished transaction in 0 secs (0.02u,0s) Finished transaction in 0 secs (0.03u,0s) Finished transaction in 0 secs (0.05u,0s) Finished transaction in 0 secs (0.09u,0.01s) Finished transaction in 0 secs (0.15u,0.05s) Finished transaction in 1 secs (0.34u,0.07s) Finished transaction in 1 secs (0.74u,0.09s) Finished transaction in 1 secs (1.45u,0.01s) Finished transaction in 4 secs (3.37u,0.08s) Finished transaction in 7 secs (7.02u,0.08s) Finished transaction in 20 secs (19.79u,0.3s) Obviously this program spends all its time in the garbage collector (tests made by Pierre Cr=E9gut are pointing towards minor collections) What could be done to achieve optimal ocaml GC performances when making *big* coq computations ? Here is the coq code I'm using : Require Plus. Definition mult2 [n] :=3D (plus n n). Definition nat_1 :=3D Eval Compute in (S O). Definition nat_2 :=3D Eval Compute in (mult2 nat_1). Definition nat_4 :=3D Eval Compute in (mult2 nat_2). Definition nat_8 :=3D Eval Compute in (mult2 nat_4). Definition nat_16 :=3D Eval Compute in (mult2 nat_8). Definition nat_32 :=3D Eval Compute in (mult2 nat_16). Definition nat_64 :=3D Eval Compute in (mult2 nat_32). Definition nat_128 :=3D Eval Compute in (mult2 nat_64). Definition nat_256 :=3D Eval Compute in (mult2 nat_128). Definition nat_512 :=3D Eval Compute in (mult2 nat_256). Time Definition nat_1k :=3D Eval Compute in (mult2 nat_512). Time Definition nat_2k :=3D Eval Compute in (mult2 nat_1k). Time Definition nat_4k :=3D Eval Compute in (mult2 nat_2k). Time Definition nat_8k :=3D Eval Compute in (mult2 nat_4k). Time Definition nat_16k :=3D Eval Compute in (mult2 nat_8k). Time Definition nat_32k :=3D Eval Compute in (mult2 nat_16k). Time Definition nat_64k :=3D Eval Compute in (mult2 nat_32k). Time Definition nat_128k :=3D Eval Compute in (mult2 nat_64k). Time Definition nat_256k :=3D Eval Compute in (mult2 nat_128k). Time Definition nat_512k :=3D Eval Compute in (mult2 nat_256k). Time Definition nat_1m :=3D Eval Compute in (mult2 nat_512k). --=20 Cuihtlauac ALVARADO - France Telecom R&D - DTL/TAL 2, avenue Pierre Marzin - 22307 Lannion - France Tel: +33 2 96 05 32 73 - Mob: +33 6 08 10 80 41 ------_=_NextPart_001_01C233B2.1FC51480 Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Coq & Ocaml GC strangeness

Hi everybody,

This message is mainly addressed to coq mailing list, = anyway i'm
crossposting to caml mailing list since GC people = might be interested.

I'm using coq to compute 1 + 1 =3D 2, then 2 + 2 =3D = 4, then 4 + 4 =3D 8,
etc. up to 2^20 (with unary natural numbers). Machine = used has a
1.7Ghz i686 and 1Gbyte of RAM. It does not swap = during the test
(starts swaping at 2^21).

Here are the timings i get (i'm using tcsh) :

~>limit
cputime         = unlimited
filesize        = unlimited
datasize        = unlimited
stacksize       8192 = kbytes
coredumpsize    unlimited
memoryuse       = unlimited
descriptors     1024
memorylocked    unlimited
maxproc         = 7168
openfiles       1024
~>coqc -opt Limits.v
Finished transaction in 0 secs (0.02u,0s)
Finished transaction in 0 secs (0.04u,0s)
Finished transaction in 1 secs (0.08u,0s)
Finished transaction in 0 secs (0.19u,0s)
Finished transaction in 0 secs (0.51u,0.01s)
Finished transaction in 2 secs (1.49u,0.02s)
Finished transaction in 5 secs (5.02u,0.04s)
Finished transaction in 18 secs (18.28u,0.03s)
Stack overflow
~>limit stacksize 128m
~>coqc -opt Limits.v
Finished transaction in 0 secs (0.01u,0s)
Finished transaction in 0 secs (0.04u,0s)
Finished transaction in 0 secs (0.08u,0s)
Finished transaction in 1 secs (0.21u,0s)
Finished transaction in 0 secs (0.55u,0.01s)
Finished transaction in 2 secs (1.6u,0.01s)
Finished transaction in 5 secs (5.2u,0.01s)
Finished transaction in 20 secs (19u,0.08s)
Finished transaction in 79 secs (71.6u,0.24s)
Finished transaction in 305 secs = (291.24u,0.68s)
Finished transaction in 1154 secs = (1117.98u,1.16s)         &nb= sp;       
~>setenv OCAMLRUNPARAM s=3D64M
~>coqc -opt Limits.v
Finished transaction in 0 secs (0.02u,0s)
Finished transaction in 0 secs (0.03u,0s)
Finished transaction in 0 secs (0.05u,0s)
Finished transaction in 0 secs (0.09u,0.01s)
Finished transaction in 0 secs (0.15u,0.05s)
Finished transaction in 1 secs (0.34u,0.07s)
Finished transaction in 1 secs (0.74u,0.09s)
Finished transaction in 1 secs (1.45u,0.01s)
Finished transaction in 4 secs (3.37u,0.08s)
Finished transaction in 7 secs (7.02u,0.08s)
Finished transaction in 20 secs (19.79u,0.3s)

Obviously this program spends all its time in the = garbage collector
(tests made by Pierre Cr=E9gut are pointing towards = minor collections)
What could be done to achieve optimal ocaml GC = performances when
making *big* coq computations ?

Here is the coq code I'm using :

Require Plus.

Definition mult2 [n] :=3D (plus n n).

Definition nat_1 :=3D Eval Compute in (S O).
Definition nat_2 :=3D Eval Compute in (mult2 = nat_1).

Definition nat_4 :=3D Eval Compute in (mult2 = nat_2).
Definition nat_8 :=3D Eval Compute in (mult2 = nat_4).
Definition nat_16 :=3D Eval Compute in (mult2 = nat_8).
Definition nat_32 :=3D Eval Compute in (mult2 = nat_16).

Definition nat_64 :=3D Eval Compute in (mult2 = nat_32).
Definition nat_128 :=3D Eval Compute in (mult2 = nat_64).
Definition nat_256 :=3D Eval Compute in (mult2 = nat_128).
Definition nat_512 :=3D Eval Compute in (mult2 = nat_256).
Time Definition nat_1k :=3D Eval Compute in (mult2 = nat_512).
Time Definition nat_2k :=3D Eval Compute in (mult2 = nat_1k).
Time Definition nat_4k :=3D Eval Compute in (mult2 = nat_2k).
Time Definition nat_8k :=3D Eval Compute in (mult2 = nat_4k).

Time Definition nat_16k :=3D Eval Compute in (mult2 = nat_8k).
Time Definition nat_32k :=3D Eval Compute in (mult2 = nat_16k).
Time Definition nat_64k :=3D Eval Compute in (mult2 = nat_32k).
Time Definition nat_128k :=3D Eval Compute in (mult2 = nat_64k).

Time Definition nat_256k :=3D Eval Compute in (mult2 = nat_128k).
Time Definition nat_512k :=3D Eval Compute in (mult2 = nat_256k).
Time Definition nat_1m :=3D Eval Compute in (mult2 = nat_512k).

--
Cuihtlauac ALVARADO - France Telecom R&D - = DTL/TAL
2, avenue Pierre Marzin - 22307 Lannion - = France
Tel: +33 2 96 05 32 73 - Mob: +33 6 08 10 80 = 41

------_=_NextPart_001_01C233B2.1FC51480-- ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners