Re: [isabelle-dev] Slow builds due to excessive heap images

[Florian Haftmann]

> They are just identifiers and I don't think they are computed with.
> However, I don't intend to change formalization beyond a global
> implementation of int by some fixed size integers, if that can be done
> easily. Otherwise we live with the increase in runtime from 7:20 to 8:20.

Hence a suitable theory would follow Code_Numeral and provide
code_printing declarations to map integer to a fixed-width
overflow-guarding implementation.

But I am also not sure whether this is worth the effort.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Tobias Nipkow]

On 16/11/2017 12:43, Florian Haftmann wrote:

Dear all,


The idea above is to provide an option for the HOL codegen that is used
specifically for applications like Flyspeck-Tame. It is mainly a
question to codegen experts, if that can be done easily.


streamlining execution of Flyspeck-Tame without risking its integrity is
a struggle now carrying on twelve years.

The key question to me is whether the integers in the archives (the ML
files) are actually used for numeric calculation (+, *, …) or are just
mere identifiers (=, maybe <).  In the latter case there are a couple of
possibilities not explored so far.


They are just identifiers and I don't think they are computed with. However, I 
don't intend to change formalization beyond a global implementation of int by 
some fixed size integers, if that can be done easily. Otherwise we live with the 
increase in runtime from 7:20 to 8:20.


Tobias


Cheers,
Florian





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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Florian Haftmann]

Dear all,

> The idea above is to provide an option for the HOL codegen that is used
> specifically for applications like Flyspeck-Tame. It is mainly a
> question to codegen experts, if that can be done easily.

streamlining execution of Flyspeck-Tame without risking its integrity is
a struggle now carrying on twelve years.

The key question to me is whether the integers in the archives (the ML
files) are actually used for numeric calculation (+, *, …) or are just
mere identifiers (=, maybe <).  In the latter case there are a couple of
possibilities not explored so far.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Manuel Eberl]

If there are fixed-size integers in ML that raise an exception on
overflow, it should be possible to just do appropriate code_printing
setup similar to what Code_Target_Numeral does. We already have to
somehow magically map Isabelle's "int" type to ML's "IntInf" type, so
all we have to do is to locally map it to ML's fixed size "int" instead,
I think.

Manuel


On 2017-11-08 15:36, Tobias Nipkow wrote:
>
>
> On 08/11/2017 14:13, Makarius wrote:
>> On 08/11/17 12:35, Tobias Nipkow wrote:
>>>
>>> On 07/11/2017 23:13, Makarius wrote:
 For Flyspeck-Tame a small performance loss remains. It might be worth
 trying to configure the Isabelle/HOL codegen to use FixedInt
 instead of
 regular (unbounded) Int. Thus it could become faster with Poly/ML
 5.7.1
 than with 5.6.
>>>
>>> Just as for Isabelle itself, I don't want generated code to abort with
>>> overflow or even worse to overflow silently.
>>
>> I also don't want to see FixedInt used routinely instead of proper
>> mathematical Int.
>>
>> The idea above is to provide an option for the HOL codegen that is used
>> specifically for applications like Flyspeck-Tame. It is mainly a
>> question to codegen experts, if that can be done easily.
>
> Then I misunderstood. An optional use of FixedInt for languages where
> overflow raises an exception is fine with me.
>
>> If the answer is "no", I personally don't mind. Flyspeck-Tame runs
>> de-facto only in background builds: 1-2h more or less does not matter so
>> much. Its classic runtime was actually 10h total, now we are at 7h.
>
> In which case I would say that providing such an option should be
> balanced with the complexity it requires or introduces.
>
> Tobias
>
>>
>> Makarius
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Tobias Nipkow]

On 08/11/2017 14:13, Makarius wrote:

On 08/11/17 12:35, Tobias Nipkow wrote:


On 07/11/2017 23:13, Makarius wrote:

For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.


Just as for Isabelle itself, I don't want generated code to abort with
overflow or even worse to overflow silently.


I also don't want to see FixedInt used routinely instead of proper
mathematical Int.

The idea above is to provide an option for the HOL codegen that is used
specifically for applications like Flyspeck-Tame. It is mainly a
question to codegen experts, if that can be done easily.


Then I misunderstood. An optional use of FixedInt for languages where overflow 
raises an exception is fine with me.



If the answer is "no", I personally don't mind. Flyspeck-Tame runs
de-facto only in background builds: 1-2h more or less does not matter so
much. Its classic runtime was actually 10h total, now we are at 7h.


In which case I would say that providing such an option should be balanced with 
the complexity it requires or introduces.


Tobias



Makarius





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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Andreas Lochbihler]

Hi Makarius,

On 08/11/17 14:13, Makarius wrote:

On 08/11/17 12:35, Tobias Nipkow wrote:


On 07/11/2017 23:13, Makarius wrote:

For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.


Just as for Isabelle itself, I don't want generated code to abort with
overflow or even worse to overflow silently.


I also don't want to see FixedInt used routinely instead of proper
mathematical Int.

The idea above is to provide an option for the HOL codegen that is used
specifically for applications like Flyspeck-Tame. It is mainly a
question to codegen experts, if that can be done easily.


My AFP entry Native_Word basically provides the setup for unsigned fixed-size integers, 
but as a separate type uintXX. The same could be done for signed fixed-size integers. The 
problem is how to get from int to uintXX. There are basically two options:


1. Just axiomatize that int are implemented with uintXX. This is potentially 
unsound.

2. Prove that actually no overflow occurs in the computations. The AFP entry 
Berlekamp-Zassenhaus does that for factoring polynomials over finite fields. The basic 
setup is there, but applying it to a particular instance requires quite some work.


FixedInt has the additional challenge that the width is implementation dependent, so this 
requires a few tricks similar to the formalisation of uint in the AFP entry.


In summary: In principle it could be possible to use FixedInt in Flyspec-Tame in a sound 
way, but it would be quite a bit of work.


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 08/11/17 12:35, Tobias Nipkow wrote:
> 
> On 07/11/2017 23:13, Makarius wrote:
>> For Flyspeck-Tame a small performance loss remains. It might be worth
>> trying to configure the Isabelle/HOL codegen to use FixedInt instead of
>> regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
>> than with 5.6.
> 
> Just as for Isabelle itself, I don't want generated code to abort with
> overflow or even worse to overflow silently.

I also don't want to see FixedInt used routinely instead of proper
mathematical Int.

The idea above is to provide an option for the HOL codegen that is used
specifically for applications like Flyspeck-Tame. It is mainly a
question to codegen experts, if that can be done easily.

If the answer is "no", I personally don't mind. Flyspeck-Tame runs
de-facto only in background builds: 1-2h more or less does not matter so
much. Its classic runtime was actually 10h total, now we are at 7h.


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Tobias Nipkow]

On 07/11/2017 23:13, Makarius wrote:

For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.


Just as for Isabelle itself, I don't want generated code to abort with overflow 
or even worse to overflow silently.


Tobias



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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 02/11/17 18:00, Makarius wrote:
> On 02/11/17 16:11, Lars Hupel wrote:
>>
>> Tobias and me have discovered an interesting discrepancy between your
>> AFP slow setup and our AFP slow setup. They run on identical hardware
>> with the only difference of 6 vs 8 threads. On 6 threads, it runs
>> significantly faster. For example, Flyspeck-Tame requires 9:44:16
>> (elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).
> 
> It was merely my intuition about the virtual hardware that using less
> resources than allocated might help. But I did not make any measurements
> with 8 vs. 6 threads, so that guess might be still wrong.
> 
> The main observation so far: it works quite well and measurements are
> reasonably stable.

Here are current and more detailed results (see dump.csv), from the
following database query:

SELECT log_name, pull_date, timing_elapsed, timing_cpu, timing_factor,
ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
threads, "ML_SYSTEM", "ML_PLATFORM", "ML_OPTIONS"
FROM isabelle_build_log
WHERE session_name = 'Flyspeck-Tame' AND (build_host = 'lrzcloud1' OR
build_engine = 'jenkins') AND pull_date > now() - INTERVAL '20 days'
ORDER BY log_name

An SQLite snapshot of that data is here:
http://isabelle.in.tum.de/devel/build_log.db -- note that SQLite lacks
advanced date functions like INTERVAL above.

Charts are here: http://isabelle.in.tum.de/devel/build_status


David Matthews has already done a great job in tuning current the
performance of Poly/ML 5.7.1 test versions, so most AFP slow sessions
have become significantly faster. Current polyml-test-fb4f42af00fa from
Isabelle/ce6454669360 looks like a very good release candidate.

For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.


Makarius
"log_name","pull_date","timing_elapsed","timing_cpu","timing_factor","ml_timing_elapsed","ml_timing_cpu","ml_timing_gc","ml_timing_factor","threads","ML_SYSTEM","ML_PLATFORM","ML_OPTIONS"
"build_history_2017-10-21.03100_lrzcloud1_x86_64-linux_M6_AFP","2017-10-21 00:20:50+02","24042000","36668000","1.5251642958156559","24035576","36661704","1462036","1.5861379814654741","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-22.03072_lrzcloud1_x86_64-linux_M6_AFP","2017-10-22 00:20:52+02","24108000","36556000","1.5163431226148996","24101313","36549752","1518640","1.5795152737114364","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-23.02973_lrzcloud1_x86_64-linux_M6_AFP","2017-10-23 00:18:22+02","24086000","36661000","1.5220875197209998","24078255","36653260","1501780","1.5846264606799787","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-24.02940_lrzcloud1_x86_64-linux_M6_AFP","2017-10-24 00:18:23+02","24175000","36795000","1.5220268872802483","24168253","36787892","1518016","1.5849680156857016","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-25.02865_lrzcloud1_x86_64-linux_M6_AFP","2017-10-25 00:18:22+02","24161000","36915000","1.5278755018418111","24154064","36907792","1504136","1.5902884086090028","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-26.02857_lrzcloud1_x86_64-linux_M6_AFP","2017-10-26 00:18:24+02","2449","37288000","1.5225806451612902","24482894","37281088","1507308","1.5843060056543969","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-27.02997_lrzcloud1_x86_64-linux_M6_AFP","2017-10-27 00:18:26+02","32431000","49188000","1.5166969874502791","32418714","49176900","1702004","1.5694300520372277","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-28.03072_lrzcloud1_x86_64-linux_M6_AFP","2017-10-28 00:18:26+02","31511000","47528000","1.5082986893465773","31500015","47517580","1154496","1.5451445340581584","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-29.02979_lrzcloud1_x86_64-linux_M6_AFP","2017-10-29 00:18:24+02","31847000","47974000","1.5063899268376928","31835385","47963260","1190340","1.5439926358672904","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-30.02870_lrzcloud1_x86_64-linux_M6_AFP","2017-10-30 00:18:27+01","31692000","48172000","1.5200050485927048","31690809","48170808","1516876","1.5678894155084524","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 3 --gcthreads 6"
"build_history_2017-10-31.02960_lrzcloud1_x86_64-linux_M6_AFP","2017-10-31 

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 04/11/17 19:30, David Matthews wrote:
> 
> I've had a look at this and pushed a change to IntInf.pow to Poly/ML
> master (c2a2961).  It now uses Word.andb rather than IntInf.andb which
> avoids a call into the run-time system (RTS).
> 
> However, this code hadn't changed since 5.6 and when I tested it using
> List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly
> not the massive differences you found with Par_List.map.  The only thing
> I can think of is that there were so many calls into the RTS that there
> was some contention on a mutex and that was causing problems.
> 
> Anyway, try the new version and let me know the results.

I have briefly tested the subsequent version Poly/ML 31b5de8ee56 and it
works well with Isabelle/978c584609de + ch-pow and AFP/9ad8f3af760f:

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/wenzelm/lib/polyml/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

lxcisa0> isabelle build -d '$AFP' -o threads=8 Lorenz_C0
Building Pure ...
Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95)
Building HOL ...
Finished HOL (0:03:21 elapsed time, 0:11:15 cpu time, factor 3.35)
Building HOL-Analysis ...
Finished HOL-Analysis (0:05:09 elapsed time, 0:27:51 cpu time, factor 5.40)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:55 elapsed time, 0:08:18
cpu time, factor 4.33)
Building HOL-ODE ...
Finished HOL-ODE (0:00:01 elapsed time)
Building HOL-ODE-Refinement ...
Finished HOL-ODE-Refinement (0:03:17 elapsed time, 0:20:01 cpu time,
factor 6.10)
Building HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:18:23 elapsed time, 0:43:51 cpu time,
factor 2.39)
Building Lorenz_Approximation ...
Finished Lorenz_Approximation (0:03:51 elapsed time, 0:08:15 cpu time,
factor 2.14)
Running Lorenz_C0 ...
Finished Lorenz_C0 (0:13:14 elapsed time, 1:39:57 cpu time, factor 7.55)
0:49:55 elapsed time, 3:39:48 cpu time, factor 4.40


Here are also the earlier results with the workaround
(Isabelle/17eb23e43630):

On 03/11/17 20:07, Makarius wrote:
> $ isabelle build -d '$AFP' -o threads=8 Lorenz_C0
> Building Pure ...
> Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.95)
> Building HOL ...
> Finished HOL (0:03:19 elapsed time, 0:10:54 cpu time, factor 3.28)
> Building HOL-Analysis ...
> Finished HOL-Analysis (0:05:16 elapsed time, 0:28:08 cpu time, factor
5.33)
> Building Ordinary_Differential_Equations ...
> Finished Ordinary_Differential_Equations (0:01:59 elapsed time, 0:08:10
> cpu time, factor 4.10)
> Building HOL-ODE ...
> Finished HOL-ODE (0:00:01 elapsed time)
> Building HOL-ODE-Refinement ...
> Finished HOL-ODE-Refinement (0:03:29 elapsed time, 0:20:08 cpu time,
> factor 5.76)
> Building HOL-ODE-Numerics ...
> Finished HOL-ODE-Numerics (0:18:06 elapsed time, 0:41:23 cpu time,
> factor 2.28)
> Building Lorenz_Approximation ...
> Finished Lorenz_Approximation (0:03:43 elapsed time, 0:07:53 cpu time,
> factor 2.12)
> Running Lorenz_C0 ...
> Finished Lorenz_C0 (0:14:21 elapsed time, 1:49:04 cpu time, factor 7.60)
> 0:51:01 elapsed time, 3:45:59 cpu time, factor 4.43


So the uniform use of IntInf.pow might come out slightly faster.

I will make a proper polyml-test component soon and then apply ch-pow
permanently, but it needs a few more days: there is still
NewTestRegisterSave (Isabelle/c70c47dcf63e) in the queue for official
testing and timing -- my impression is that it will be only a few
percent faster.


Makarius
# HG changeset patch
# User wenzelm
# Date 1509824436 -3600
#  Sat Nov 04 20:40:36 2017 +0100
# Node ID 415a6bba9344b53576477a6e03d6ea5f6219ad1d
# Parent  978c584609ded0d1a36246b83aeb8630d14034f9
test

diff -r 978c584609de -r 415a6bba9344 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML   Sat Nov 04 19:44:28 2017 +0100
+++ b/src/Pure/General/integer.ML   Sat Nov 04 20:40:36 2017 +0100
@@ -40,20 +40,7 @@
 
 fun square x = x * x;
 
-fun pow k l =
-  let
-fun pw 0 _ = 1
-  | pw 1 l = l
-  | pw k l =
-  let
-val (k', r) = div_mod k 2;
-val l' = pw k' (l * l);
-  in if r = 0 then l' else l' * l end;
-  in
-if k < 0
-then IntInf.pow (l, k)
-else pw k l
-  end;
+fun pow k l = IntInf.pow (l, k);
 
 fun gcd x y = PolyML.IntInf.gcd (x, y);
 fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
@@ -65,10 +52,3 @@
   | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
 
 end;
-
-(* FIXME workaround for Poly/ML 5.7.1 testing *)
-structure IntInf =
-struct
-  open IntInf;
-  fun pow (i, n) = Integer.pow n i;
-end
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[David Matthews]

On 03/11/2017 19:07, Makarius wrote:

On 03/11/17 19:26, Fabian Immler wrote:

I looked at it once more: profiling told me that IntInf.pow (in combination 
with Par_List.map) seems to be the culprit.

The following snippet shows similar behavior:
ML ‹
fun powers [] = []
  | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
›

polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, 
factor 5.70
polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
time
polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu 
time, 42.602s GC time


I have discovered the same and have now pushed a workaround:
http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630

Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit
wasteful, maybe during the bit vector operation instead of our
IntInf.divMod (_, 2) used here: see
http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43


I've had a look at this and pushed a change to IntInf.pow to Poly/ML 
master (c2a2961).  It now uses Word.andb rather than IntInf.andb which 
avoids a call into the run-time system (RTS).


However, this code hadn't changed since 5.6 and when I tested it using 
List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly 
not the massive differences you found with Par_List.map.  The only thing 
I can think of is that there were so many calls into the RTS that there 
was some contention on a mutex and that was causing problems.


Anyway, try the new version and let me know the results.

David

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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 03/11/17 16:36, Fabian Immler wrote:
> 
> 
> I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
> 1600 --maxheap 4000" if that is relevant).
> Invoked with "isabelle build -d . -othreads=8" for the theory below.
> 
> polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu 
> time, factor 6.94)
> polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 
> 4.70)
> 
> Both are in isabelle/123670d1cff3
> 
> theory Check
> imports Pure
> begin
> 
> ML_file \check.sml\
> ML \timeap Check.check (0 upto 7)\
> 
> end

Just for the record, here are my test results for this setup: lxcisa0,
x86_64-linux, threads=6.

log1.gz: polyml-5.6-1
Finished Check (0:00:56 elapsed time, 0:03:01 cpu time, factor 3.21)

log2.gz: polyml-test-e8d82343b692
Finished Check (0:02:50 elapsed time, 0:13:25 cpu time, factor 4.72)

log3.gz: polyml-NewTestRegisterSave
Finished Check (0:02:53 elapsed time, 0:13:36 cpu time, factor 4.72)

log4.gz: polyml-test-e8d82343b692
ML \
structure IntInf =
struct
  open IntInf
  fun pow (i, n) = Integer.pow n i;
end
\
Finished Check (0:00:39 elapsed time, 0:02:01 cpu time, factor 3.06)


The logs contain profiling information at the bottom. Here is are the
relevant bits of log2.gz vs. log4.gz (produced with "isabelle
profiling_report):

   229 IntInf.divMod
   256 Check.approx_floatarith
   261 IntSet.mergeLists
   281 Check.map
   306 GARBAGE COLLECTION (total)
   352 Check.divide_inta
   468 Check.float_plus_down
  3155 Check.log2
 33415 IntInf.pow

   234 Check.approx_floatarith
   245 IntSet.mergeLists
   276 Check.divide_inta
   307 GARBAGE COLLECTION (total)
   321 Integer.pow
   323 Check.float_plus_down
  1514 IntInf.divMod
  2946 Check.log2

The problem is de-facto solved by the workaround in Isabelle/17eb23e43630.


Makarius




log1.gz
Description: application/gzip


log2.gz
Description: application/gzip


log3.gz
Description: application/gzip


log4.gz
Description: application/gzip
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 03/11/17 19:26, Fabian Immler wrote:
> I looked at it once more: profiling told me that IntInf.pow (in combination 
> with Par_List.map) seems to be the culprit.
> 
> The following snippet shows similar behavior:
> ML ‹
> fun powers [] = []
>  | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
> Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
> ›
> 
> polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
> polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu 
> time, factor 5.70
> polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
> time
> polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu 
> time, 42.602s GC time

I have discovered the same and have now pushed a workaround:
http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630

Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit
wasteful, maybe during the bit vector operation instead of our
IntInf.divMod (_, 2) used here: see
http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43

With that little change, I get the following very good timings on lxcisa0:

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

$ isabelle build -d '$AFP' -o threads=8 Lorenz_C0
Building Pure ...
Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.95)
Building HOL ...
Finished HOL (0:03:19 elapsed time, 0:10:54 cpu time, factor 3.28)
Building HOL-Analysis ...
Finished HOL-Analysis (0:05:16 elapsed time, 0:28:08 cpu time, factor 5.33)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:59 elapsed time, 0:08:10
cpu time, factor 4.10)
Building HOL-ODE ...
Finished HOL-ODE (0:00:01 elapsed time)
Building HOL-ODE-Refinement ...
Finished HOL-ODE-Refinement (0:03:29 elapsed time, 0:20:08 cpu time,
factor 5.76)
Building HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:18:06 elapsed time, 0:41:23 cpu time,
factor 2.28)
Building Lorenz_Approximation ...
Finished Lorenz_Approximation (0:03:43 elapsed time, 0:07:53 cpu time,
factor 2.12)
Running Lorenz_C0 ...
Finished Lorenz_C0 (0:14:21 elapsed time, 1:49:04 cpu time, factor 7.60)
0:51:01 elapsed time, 3:45:59 cpu time, factor 4.43


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Fabian Immler]

I looked at it once more: profiling told me that IntInf.pow (in combination 
with Par_List.map) seems to be the culprit.

The following snippet shows similar behavior:
ML ‹
fun powers [] = []
 | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
›

polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, 
factor 5.70
polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
time
polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu 
time, 42.602s GC time


> Am 03.11.2017 um 16:36 schrieb Fabian Immler :
> 
> 
> 
>> Am 03.11.2017 um 14:56 schrieb Fabian Immler :
>> 
>> 
>>> Am 02.11.2017 um 18:00 schrieb Makarius :
>>> 
>>> I am more worried about the factor 5 performance loss of Lorenz_C0: now
>>> (3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
>>> the problem is related to Flyspeck-Tame. I did not approach it yet,
>>> because the HOL-ODE tower is really huge.
>>> 
>>> It would greatly help to see the problem in isolated spots. I usually
>>> send David specimens produced by code_runtime_trace.
>> At least on my Mac, there seems to be a problem with (or induced by) 
>> parallelism:
>> The attached check.sml is the code extracted from Lorenz_C0.
>> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in 
>> the computation for individual elements.
>> 
>> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, 
>> something goes very wrong: a slowdown by a factor of more than 50, compared 
>> to Isabelle2017 .
>> 
>> This seems to be related to parallelism:
>> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. 
>> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.
>> 
>> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this 
>> behaves for both parallel and sequential computations like Isabelle2017.
>> 
>> Unfortunately, I failed to reproduce this behavior on Linux.
> 
> I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
> 1600 --maxheap 4000" if that is relevant).
> Invoked with "isabelle build -d . -othreads=8" for the theory below.
> 
> polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu 
> time, factor 6.94)
> polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 
> 4.70)
> 
> Both are in isabelle/123670d1cff3
> 
> --
> 
> theory Check
> imports Pure
> begin
> 
> ML_file \check.sml\
> ML \timeap Check.check (0 upto 7)\
> 
> end
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Fabian Immler]

> Am 03.11.2017 um 14:56 schrieb Fabian Immler :
> 
> 
>> Am 02.11.2017 um 18:00 schrieb Makarius :
>> 
>> I am more worried about the factor 5 performance loss of Lorenz_C0: now
>> (3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
>> the problem is related to Flyspeck-Tame. I did not approach it yet,
>> because the HOL-ODE tower is really huge.
>> 
>> It would greatly help to see the problem in isolated spots. I usually
>> send David specimens produced by code_runtime_trace.
> At least on my Mac, there seems to be a problem with (or induced by) 
> parallelism:
> The attached check.sml is the code extracted from Lorenz_C0.
> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in 
> the computation for individual elements.
> 
> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, 
> something goes very wrong: a slowdown by a factor of more than 50, compared 
> to Isabelle2017 .
> 
> This seems to be related to parallelism:
> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. 
> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.
> 
> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this 
> behaves for both parallel and sequential computations like Isabelle2017.
> 
> Unfortunately, I failed to reproduce this behavior on Linux.

I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
1600 --maxheap 4000" if that is relevant).
Invoked with "isabelle build -d . -othreads=8" for the theory below.

polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu time, 
factor 6.94)
polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 4.70)

Both are in isabelle/123670d1cff3

--

theory Check
imports Pure
begin

ML_file \check.sml\
ML \timeap Check.check (0 upto 7)\

end




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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 02/11/17 16:11, Lars Hupel wrote:
> 
> Tobias and me have discovered an interesting discrepancy between your
> AFP slow setup and our AFP slow setup. They run on identical hardware
> with the only difference of 6 vs 8 threads. On 6 threads, it runs
> significantly faster. For example, Flyspeck-Tame requires 9:44:16
> (elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

It was merely my intuition about the virtual hardware that using less
resources than allocated might help. But I did not make any measurements
with 8 vs. 6 threads, so that guess might be still wrong.

The main observation so far: it works quite well and measurements are
reasonably stable.


> That difference aside, what I also find alarming is that the total
> runtime of Flyspeck-Tame increased by more than 20% after the switch to
> Poly/ML 5.7.

I've had some private email exchange with David Matthews about it. It is
a consequence of a bias towards FixedInt instead of IntInf (= Int) in
the ML code generator. There is some chance that Flyspeck-Tame actually
works with FixedInt, but I did not try it yet.

Which Isabelle codegen options are required to use FixedInt instead of
mathematical Int?

Here is also an experiment to make the present setup
(polyml-test-e8d82343b692) a bit faster:
https://github.com/polyml/polyml/tree/NewTestRegisterSave -- I have some
tests with that still running.


I am more worried about the factor 5 performance loss of Lorenz_C0: now
(3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
the problem is related to Flyspeck-Tame. I did not approach it yet,
because the HOL-ODE tower is really huge.

It would greatly help to see the problem in isolated spots. I usually
send David specimens produced by code_runtime_trace.


> This now means that the slow sessions rapidly approach 24 hours
> in build time, which makes it less feasible to run them every day.

That is already an old AFP tradition :-) Applications are constantly
pushing towards the end of it all, but so far the technology has managed
to keep up.

For the non-slow tests, I have already split AFP into two structually
quite stable parts:
http://isabelle.in.tum.de/repos/isabelle/file/fc87d3becd69/src/Pure/Admin/afp.scala#l86

In the worst case, we could split the slow sessions manually by extra
group tags.


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Lars Hupel]

> We are presently testing Poly/ML 5.7.1 by default (see
> Isabelle/aefaaef29c58) and there are already interesting performance
> figures, e.g. see:
> 
> http://isabelle.in.tum.de/devel/build_status
> http://isabelle.in.tum.de/devel/build_status/Linux_A
> http://isabelle.in.tum.de/devel/build_status/AFP
> 
> Overall, performance is mostly the same as in Poly/ML 5.6 from
> Isabelle2017, but there are some dropouts. In particular, loading heap
> images has become relatively slow: this impacts long heap chains like
> HOL-Analysis or big applications in AFP. E.g. see
> http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
> (timing vs. ML timing).

Tobias and me have discovered an interesting discrepancy between your
AFP slow setup and our AFP slow setup. They run on identical hardware
with the only difference of 6 vs 8 threads. On 6 threads, it runs
significantly faster. For example, Flyspeck-Tame requires 9:44:16
(elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

That difference aside, what I also find alarming is that the total
runtime of Flyspeck-Tame increased by more than 20% after the switch to
Poly/ML 5.7. This now means that the slow sessions rapidly approach 24
hours in build time, which makes it less feasible to run them every day.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Fabian Immler]

I should have sent the message below also to isabelle-dev, sorry about that.
Has anything changed about integers in Poly/ML 5.7.1?

Lorenz_C0 did slow down by a factor of 5, which I find quite extreme.

Best,
Fabian

> Am 28.10.2017 um 23:57 schrieb Fabian Immler :
> 
> Lorenz_C0 is one of those "much slower" sessions.
> If it helps, this is how I would characterize it:
> It is essentially one long computation where the code (IIRC about 15000 lines 
> in SML) was generated in the parent session Lorenz_Approximation via 
> @{computation_check ...}). The computation depends heavily on IntInf 
> operations (but mostly in the <64 bit range)
> 
> Fabian
> 
>> Am 28.10.2017 um 22:45 schrieb Makarius :
>> 
>> On 28/10/17 22:26, Makarius wrote:
>>> We are presently testing Poly/ML 5.7.1 by default (see
>>> Isabelle/aefaaef29c58) and there are already interesting performance
>>> figures, e.g. see:
>>> 
>>> http://isabelle.in.tum.de/devel/build_status
>>> http://isabelle.in.tum.de/devel/build_status/Linux_A
>>> http://isabelle.in.tum.de/devel/build_status/AFP
>> 
>> The daily "AFP slow" timing has arrived just now, 4h hours later than
>> with Poly/ML 5.6:
>> http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads
>> 
>> I still need to investigate, why some sessions require much longer now.
>> It might be due massive amounts of generated code.
>> 
>> 
>>  Makarius
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 



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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 28/10/17 22:26, Makarius wrote:
>
> I still have some ideas for "isabelle build" in the pipeline (for
> several years) to skip building intermediate heaps in the first place.
> Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build
> time.
> 
> Until that emerges, AFP contributors may want to double-check, which
> auxiliary heaps ("Base", "Lib", "Pre") are really needed and beneficial
> for overall build times.

That now came out as options for "isabelle jedit", instead of more
"isabelle build" technology (and complexity).


Here is a summary of the present situation:

  * Poly/ML 5.7.1 (testing version) is quite fast in loading heaps, but
there are also file-system accesses and time to build heaps in the first
place (which also means full sharing of live data: at the order of 30s).

  * It does not make sense to refer to a parent session and then use
only a few small theories that require < 10s. Above 30s a parent that is
itself not too bulky usually helps.

  * Building a heap with many ancestors is more expensive than a rather
flat hierarchy. There is a small overhead in the Poly/ML runtime system
for managing the dynamic hierarchy, but more relevant are redundant
imports: a big stack of heaps usually contains many theories that are
not needed in the final application.

  * http://isabelle.in.tum.de/devel/build_status/AFP/index.html shows
some of the data that accumulates in one big Isabelle test database.
There is more than than shown here, e.g. individual theory timings
(which are meaningful for these builds with threads=1).

In the exploration, I've occasionally emitted handwritten SQL statements
to the PostgreSQL engine via the web interface of phppgadmin. At some
point there might be more generated HTML output or some IDE interface to
query the data.


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Tobias Nipkow]

On 29/10/2017 21:52, Makarius wrote:

On 28/10/17 22:26, Makarius wrote:


Overall, performance is mostly the same as in Poly/ML 5.6 from
Isabelle2017, but there are some dropouts. In particular, loading heap
images has become relatively slow: this impacts long heap chains like
HOL-Analysis or big applications in AFP. E.g. see
http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
(timing vs. ML timing).

I've shown this to David Matthews already and await his answer. It could
be just an accident in Poly/ML 905dae2ebfda or inherent due to the new
heap + GC management that is more robust against out-of-memory failures.


David Matthews has done a great job to improve this in Poly/ML
e8d82343b692 (see Isabelle/d0f12783cd80). It means that loading of
complex heap hierarchies is now faster than in Poly/ML 5.6.


Very nice indeed!

Tobias




Independently of that, excessive use of intermediate heap images makes
builds much slower than necessary, because multithreading is reduced by
the structural serialization. Here is a typical example:


Here is an updated test, on different hardware:

Isabelle/d0f12783cd80
AFP/88218011955a

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 3000 --maxheap 16000"

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.97)
Finished HOL (0:03:48 elapsed time, 0:11:11 cpu time, factor 2.93)
Finished HOL-Library (0:02:05 elapsed time, 0:08:49 cpu time, factor 4.24)
Finished HOL-Computational_Algebra (0:01:05 elapsed time, 0:02:44 cpu
time, factor 2.50)
Finished HOL-Algebra (0:01:44 elapsed time, 0:04:23 cpu time, factor 2.53)
Finished JNF-HOL-Lib (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.58)
Finished JNF-AFP-Lib (0:01:36 elapsed time, 0:06:37 cpu time, factor 4.13)
Finished Jordan_Normal_Form (0:04:47 elapsed time, 0:13:25 cpu time,
factor 2.80)
Finished Subresultants (0:01:01 elapsed time, 0:02:33 cpu time, factor 2.48)
Finished Pre_BZ (0:01:31 elapsed time, 0:05:35 cpu time, factor 3.66)
Finished Berlekamp_Zassenhaus (0:02:29 elapsed time, 0:07:41 cpu time,
factor 3.09)
Finished Pre_Algebraic_Numbers (0:00:32 elapsed time, 0:01:06 cpu time,
factor 2.06)
Finished Algebraic_Numbers_Lib (0:01:25 elapsed time, 0:03:44 cpu time,
factor 2.62)
Finished Linear_Recurrences (0:00:43 elapsed time, 0:01:22 cpu time,
factor 1.88)
Finished Linear_Recurrences_Test (0:02:15 elapsed time, 0:07:49 cpu
time, factor 3.46)
0:26:13 elapsed time, 1:17:50 cpu time, factor 2.97

$ isabelle build -o threads=6 -o timeout_scale=4 -d '$AFP' -f
Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.97)
Finished HOL (0:03:52 elapsed time, 0:11:22 cpu time, factor 2.93)
Finished Linear_Recurrences_Test (0:12:02 elapsed time, 0:52:56 cpu
time, factor 4.40)
0:16:42 elapsed time, 1:04:38 cpu time, factor 3.87


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





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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 28/10/17 22:26, Makarius wrote:
> 
> Overall, performance is mostly the same as in Poly/ML 5.6 from
> Isabelle2017, but there are some dropouts. In particular, loading heap
> images has become relatively slow: this impacts long heap chains like
> HOL-Analysis or big applications in AFP. E.g. see
> http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
> (timing vs. ML timing).
> 
> I've shown this to David Matthews already and await his answer. It could
> be just an accident in Poly/ML 905dae2ebfda or inherent due to the new
> heap + GC management that is more robust against out-of-memory failures.

David Matthews has done a great job to improve this in Poly/ML
e8d82343b692 (see Isabelle/d0f12783cd80). It means that loading of
complex heap hierarchies is now faster than in Poly/ML 5.6.


> Independently of that, excessive use of intermediate heap images makes
> builds much slower than necessary, because multithreading is reduced by
> the structural serialization. Here is a typical example:

Here is an updated test, on different hardware:

Isabelle/d0f12783cd80
AFP/88218011955a

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 3000 --maxheap 16000"

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.97)
Finished HOL (0:03:48 elapsed time, 0:11:11 cpu time, factor 2.93)
Finished HOL-Library (0:02:05 elapsed time, 0:08:49 cpu time, factor 4.24)
Finished HOL-Computational_Algebra (0:01:05 elapsed time, 0:02:44 cpu
time, factor 2.50)
Finished HOL-Algebra (0:01:44 elapsed time, 0:04:23 cpu time, factor 2.53)
Finished JNF-HOL-Lib (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.58)
Finished JNF-AFP-Lib (0:01:36 elapsed time, 0:06:37 cpu time, factor 4.13)
Finished Jordan_Normal_Form (0:04:47 elapsed time, 0:13:25 cpu time,
factor 2.80)
Finished Subresultants (0:01:01 elapsed time, 0:02:33 cpu time, factor 2.48)
Finished Pre_BZ (0:01:31 elapsed time, 0:05:35 cpu time, factor 3.66)
Finished Berlekamp_Zassenhaus (0:02:29 elapsed time, 0:07:41 cpu time,
factor 3.09)
Finished Pre_Algebraic_Numbers (0:00:32 elapsed time, 0:01:06 cpu time,
factor 2.06)
Finished Algebraic_Numbers_Lib (0:01:25 elapsed time, 0:03:44 cpu time,
factor 2.62)
Finished Linear_Recurrences (0:00:43 elapsed time, 0:01:22 cpu time,
factor 1.88)
Finished Linear_Recurrences_Test (0:02:15 elapsed time, 0:07:49 cpu
time, factor 3.46)
0:26:13 elapsed time, 1:17:50 cpu time, factor 2.97

$ isabelle build -o threads=6 -o timeout_scale=4 -d '$AFP' -f
Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.97)
Finished HOL (0:03:52 elapsed time, 0:11:22 cpu time, factor 2.93)
Finished Linear_Recurrences_Test (0:12:02 elapsed time, 0:52:56 cpu
time, factor 4.40)
0:16:42 elapsed time, 1:04:38 cpu time, factor 3.87


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 28/10/17 22:26, Makarius wrote:
> We are presently testing Poly/ML 5.7.1 by default (see
> Isabelle/aefaaef29c58) and there are already interesting performance
> figures, e.g. see:
> 
> http://isabelle.in.tum.de/devel/build_status
> http://isabelle.in.tum.de/devel/build_status/Linux_A
> http://isabelle.in.tum.de/devel/build_status/AFP

The daily "AFP slow" timing has arrived just now, 4h hours later than
with Poly/ML 5.6:
http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads

I still need to investigate, why some sessions require much longer now.
It might be due massive amounts of generated code.


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

[isabelle-dev] Slow builds due to excessive heap images

[Makarius]

We are presently testing Poly/ML 5.7.1 by default (see
Isabelle/aefaaef29c58) and there are already interesting performance
figures, e.g. see:

http://isabelle.in.tum.de/devel/build_status
http://isabelle.in.tum.de/devel/build_status/Linux_A
http://isabelle.in.tum.de/devel/build_status/AFP

Overall, performance is mostly the same as in Poly/ML 5.6 from
Isabelle2017, but there are some dropouts. In particular, loading heap
images has become relatively slow: this impacts long heap chains like
HOL-Analysis or big applications in AFP. E.g. see
http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
(timing vs. ML timing).

I've shown this to David Matthews already and await his answer. It could
be just an accident in Poly/ML 905dae2ebfda or inherent due to the new
heap + GC management that is more robust against out-of-memory failures.


Independently of that, excessive use of intermediate heap images makes
builds much slower than necessary, because multithreading is reduced by
the structural serialization. Here is a typical example:

Isabelle/4ff031d249b2
AFP/4482dd3b0471

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/wenzelm/.isabelle/contrib/polyml-test-905dae2ebfda/x86_64-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 1500"

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.96)
Finished HOL (0:03:32 elapsed time, 0:10:48 cpu time, factor 3.06)
Finished HOL-Library (0:02:04 elapsed time, 0:08:12 cpu time, factor 3.94)
Finished HOL-Computational_Algebra (0:01:11 elapsed time, 0:02:51 cpu
time, factor 2.39)
Finished HOL-Algebra (0:02:01 elapsed time, 0:04:51 cpu time, factor 2.41)
Finished JNF-HOL-Lib (0:00:43 elapsed time, 0:00:55 cpu time, factor 1.26)
Finished JNF-AFP-Lib (0:02:14 elapsed time, 0:07:32 cpu time, factor 3.37)
Finished Jordan_Normal_Form (0:06:54 elapsed time, 0:16:29 cpu time,
factor 2.38)
Finished Subresultants (0:03:00 elapsed time, 0:04:28 cpu time, factor 1.49)
Finished Pre_BZ (0:03:56 elapsed time, 0:08:15 cpu time, factor 2.09)
Finished Berlekamp_Zassenhaus (0:05:41 elapsed time, 0:11:14 cpu time,
factor 1.98)
Finished Pre_Algebraic_Numbers (0:05:02 elapsed time, 0:05:41 cpu time,
factor 1.13)
Finished Algebraic_Numbers_Lib (0:05:51 elapsed time, 0:08:07 cpu time,
factor 1.39)
Finished Linear_Recurrences (0:06:28 elapsed time, 0:07:11 cpu time,
factor 1.11)
Finished Linear_Recurrences_Test (0:08:24 elapsed time, 0:13:41 cpu
time, factor 1.63)
0:57:59 elapsed time, 1:50:38 cpu time, factor 1.91

That looks impressive, but there is not so much behind it. When
Linear_Recurrences_Test uses "HOL" as parent and "Linear_Recurrences" as
import session (see ch-test) the timing becomes:

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95)
Finished HOL (0:03:31 elapsed time, 0:10:32 cpu time, factor 2.99)
Finished Linear_Recurrences_Test (0:08:20 elapsed time, 0:37:48 cpu
time, factor 4.53)
0:12:31 elapsed time, 0:48:38 cpu time, factor 3.88

$ isabelle build -o threads=12 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.95)
Finished HOL (0:03:25 elapsed time, 0:12:12 cpu time, factor 3.56)
Finished Linear_Recurrences_Test (0:06:31 elapsed time, 0:39:11 cpu
time, factor 6.00)
0:10:34 elapsed time, 0:51:38 cpu time, factor 4.89


I still have some ideas for "isabelle build" in the pipeline (for
several years) to skip building intermediate heaps in the first place.
Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build
time.

Until that emerges, AFP contributors may want to double-check, which
auxiliary heaps ("Base", "Lib", "Pre") are really needed and beneficial
for overall build times.

Just for private development, it is always possible to specify auxiliary
sessions in $ISABELLE_HOME_USERS/etc/ROOT and comment them in or out on
demand. This simplifies the structure of the published AFP and makes
builds faster right now without further technology. Session-qualified
theory names allow this flexibility already.


Makarius
# HG changeset patch
# User wenzelm
# Date 1509220282 -7200
#  Sat Oct 28 21:51:22 2017 +0200
# Node ID 8d81720c2abab7677d00df167eba65341a302393
# Parent  4482dd3b04713302842a538c42902d2198ceab14
test

diff -r 4482dd3b0471 -r 8d81720c2aba thys/Linear_Recurrences/ROOT
--- a/thys/Linear_Recurrences/ROOT  Sat Oct 28 19:14:14 2017 +0200
+++ b/thys/Linear_Recurrences/ROOT  Sat Oct 28 21:51:22 2017 +0200
@@ -10,7 +10,9 @@
   document_files
 "root.tex"
 
-session Linear_Recurrences_Test (AFP) = Linear_Recurrences +
+session Linear_Recurrences_Test (AFP) = HOL +
   options [document = false, timeout = 600]
+  sessions
+"Linear_Recurrences"
   theories
 Linear_Recurrences_Test
___
isabelle-dev mailing list
isabelle-...@in.tum.de