[Camllist] Coq & Ocaml GC strangeness
 Cuihtlauac ALVARADO
[
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:   (:) 
From:  Cuihtlauac ALVARADO <cuihtlauac.alvarado@f...> 
Subject:  [Camllist] 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 = 2, then 2 + 2 = 4, then 4 + 4 = 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) ~~>setenv OCAMLRUNPARAM s=64M ~~>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égut 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] := (plus n n). Definition nat_1 := Eval Compute in (S O). Definition nat_2 := Eval Compute in (mult2 nat_1). Definition nat_4 := Eval Compute in (mult2 nat_2). Definition nat_8 := Eval Compute in (mult2 nat_4). Definition nat_16 := Eval Compute in (mult2 nat_8). Definition nat_32 := Eval Compute in (mult2 nat_16). Definition nat_64 := Eval Compute in (mult2 nat_32). Definition nat_128 := Eval Compute in (mult2 nat_64). Definition nat_256 := Eval Compute in (mult2 nat_128). Definition nat_512 := Eval Compute in (mult2 nat_256). Time Definition nat_1k := Eval Compute in (mult2 nat_512). Time Definition nat_2k := Eval Compute in (mult2 nat_1k). Time Definition nat_4k := Eval Compute in (mult2 nat_2k). Time Definition nat_8k := Eval Compute in (mult2 nat_4k). Time Definition nat_16k := Eval Compute in (mult2 nat_8k). Time Definition nat_32k := Eval Compute in (mult2 nat_16k). Time Definition nat_64k := Eval Compute in (mult2 nat_32k). Time Definition nat_128k := Eval Compute in (mult2 nat_64k). Time Definition nat_256k := Eval Compute in (mult2 nat_128k). Time Definition nat_512k := Eval Compute in (mult2 nat_256k). Time Definition nat_1m := 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