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

[Makarius]

On 22/01/2019 23:08, Fabian Immler wrote:
> 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

Back in Nov-2017, I made the following workaround that is still active:
http://isabelle.in.tum.de/repos/isabelle/rev/5da20135f560

Looking at the profiles of the included Float_Test.thy I now see a lot
of IntInf.divMod, but it is qualitatively similar to former IntInf.pow.

Maybe David can revisit both of these operations, so that we can  get
rid of the workarounds.


Note that I have produced the profiles as follows:

  isabelle build -o profiling=time ...

with a suitable test session that includes the above test theory, e.g.
see the included ROOT.

Then with "isabelle profiling_report" on the resulting log files, e.g.

  isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/Float_Test.gz


	Makarius
-------------- next part --------------
theory Float_Test
  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 \<open>val logistic_chaos = @{code logistic_chaos}\<close>
ML \<open>Par_List.map logistic_chaos (replicate 10 100000)\<close>
\<comment> \<open>x86_64_32: 24s
   x86_64: 2s\<close>

(*
ML \<open>map logistic_chaos (replicate 10 100000)\<close>
\<comment> \<open>x86_64_32: 16s
   x86_64: 8s\<close>
*)

end
-------------- next part --------------
session Float_Test = "HOL-Library" +
  theories
    Float_Test
-------------- next part --------------
A non-text attachment was scrubbed...
Name: x86.log
Type: text/x-log
Size: 3224 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190123/842377a9/attachment-0006.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: x86_64_32.log
Type: text/x-log
Size: 3398 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190123/842377a9/attachment-0007.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: x86_64.log
Type: text/x-log
Size: 3888 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190123/842377a9/attachment-0008.bin>