Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

[Fabian Immler]

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_PLATFORM="x86-linux"
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)


And indeed, if you try the theory at the end:


All of this reminds me of the discussion we had in November 2017:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2017-November/thread.html#7643

Fabian


==============================================================
theory Scratch
  imports
    "HOL-Library.Float"
    "HOL-Library.Code_Target_Numeral"
begin

definition "logistic p r x =


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



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›

end

Lorenz_C0 had the most significant slowdown, it has the biggest number of parallel computations, so I thought this might be related. Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32 whereas the sequential evaluation is only 2 times slower. normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down p 1 (-x)))" definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1)) (nat_of_integer i)"

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev