[Caml-list] Coq & Ocaml GC strangeness

[Caml-list] Coq & Ocaml GC strangeness

[Cuihtlauac ALVARADO]

[-- Attachment #1: Type: text/plain, Size: 3871 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 6909 bytes --]