[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)
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:
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 =
   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›

end

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190122/2f488802/attachment.bin>