On 1/22/2019 4:00 PM, Fabian Immler wrote:
On 1/22/2019 2:28 PM, Makarius wrote:
On 22/01/2019 20:05, Fabian Immler wrote:
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).

The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:

ML_OPTIONS="--minheap 2000 --maxheap 4000"
Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time,
factor 2.66)
Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time,
factor 1.46) > (I am testing HOL-ODE-ARCH-COMP with
polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take some time...)
HOL-ODE-ARCH-COMP looked fine (2-3 times slower). But I realized that this was the case with your computations, too. Unlike Lorenz_C0:

> x86_64_32-linux -minheap 1500
> Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44)
> x86_64-linux --minheap 3000
> Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52)
Lorenz_C0 had the most significant slowdown, it has the biggest number of parallel computations, so I thought this might be related.

And indeed, if you try the theory at the end:
Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32 whereas the sequential evaluation is only 2 times slower.

All of this reminds me of the discussion we had in November 2017:


theory Scratch

definition "logistic p r x =
normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down p 1 (-x)))"

primrec iter where
  "iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"

definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1)) (nat_of_integer i)"

ML ‹val logistic_chaos = @{code logistic_chaos}›
ML ‹Par_List.map logistic_chaos (replicate 10 100000)›
― ‹x86_64_32: 24s
   x86_64: 2s›
ML ‹map logistic_chaos (replicate 10 100000)›
― ‹x86_64_32: 16s
   x86_64: 8s›


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to