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 30000 --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 30000 --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 30000 --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 30000 --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 30000 --gcthreads 6" "build_history_2017-10-26.02857_lrzcloud1_x86_64-linux_M6_AFP","2017-10-26 00:18:24+02","24490000","37288000","1.5225806451612902","24482894","37281088","1507308","1.5843060056543969","6","polyml-5.6","x86_64-linux","--minheap 3000 --maxheap 30000 --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 30000 --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 30000 --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 30000 --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 30000 --gcthreads 6" "build_history_2017-10-31.02960_lrzcloud1_x86_64-linux_M6_AFP","2017-10-31 00:18:27+01","31090000","47390000","1.5242843357992923","31089250","47388936","1276672","1.5653516247577539","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-01.02959_lrzcloud1_x86_64-linux_M6_AFP","2017-11-01 00:18:24+01","31855000","48184000","1.5126039868152565","31853915","48183080","1457508","1.5583826352270984","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-02.02874_lrzcloud1_x86_64-linux_M6_AFP","2017-11-02 00:18:24+01","32101000","48633000","1.5149995327248373","32099766","48631972","1513312","1.5621697678419213","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-03.02896_lrzcloud1_x86_64-linux_M6_AFP","2017-11-03 00:18:27+01","32157000","48904000","1.5207886307802345","32156397","48903480","1528644","1.5683387663114123","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-04.02876_lrzcloud1_x86_64-linux_M6_AFP","2017-11-04 00:18:24+01","31696000","48113000","1.5179517920242303","31694130","48111996","1311480","1.5593889467860453","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-05.02876_lrzcloud1_x86_64-linux_M6_AFP","2017-11-05 00:18:23+01","32440000","49028000","1.51134401972873","32438330","49027304","1500060","1.5576438121197977","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-06.02878_lrzcloud1_x86_64-linux_M6_AFP","2017-11-06 00:18:23+01","27630000","41956000","1.518494390155628","27629082","41955360","1470200","1.5717337260789193","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "build_history_2017-11-07.02868_lrzcloud1_x86_64-linux_M6_AFP","2017-11-07 00:18:23+01","27527000","41816000","1.5190903476586624","27525217","41814936","1457136","1.5720883145081108","6","polyml-5.7.1","x86_64-linux","--minheap 3000 --maxheap 30000 --gcthreads 6" "jenkins_2017-10-19.05591_isabelle-nightly-slow","2017-10-19 01:33:11+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-20.05590_isabelle-nightly-slow","2017-10-19 01:33:11+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-21.05591_isabelle-nightly-slow","2017-10-21 00:20:50+02","26627000","39970000","1.5011078979982724","26611146","39950388","788724","1.5309040805683454","8","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-22.05591_isabelle-nightly-slow","2017-10-22 00:20:52+02","26652000","39854000","1.4953474410926009","26635879","39834440","708276","1.5221091821298631","8","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-23.05589_isabelle-nightly-slow","2017-10-23 00:18:22+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-24.05589_isabelle-nightly-slow","2017-10-24 00:18:23+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-25.05589_isabelle-nightly-slow","2017-10-25 00:18:22+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-26.05592_isabelle-nightly-slow","2017-10-26 00:18:24+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.6","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-27.05591_isabelle-nightly-slow","2017-10-27 00:18:26+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-28.05601_isabelle-nightly-slow","2017-10-28 00:18:26+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-29.05591_isabelle-nightly-slow","2017-10-29 00:18:24+02","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-30.05592_isabelle-nightly-slow","2017-10-30 00:18:27+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-10-31.05594_isabelle-nightly-slow","2017-10-31 00:18:27+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-01.05597_isabelle-nightly-slow","2017-11-01 00:18:24+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-02.05592_isabelle-nightly-slow","2017-11-02 00:18:24+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-03.05591_isabelle-nightly-slow","2017-11-03 00:18:27+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-04.05612_isabelle-nightly-slow","2017-11-04 00:18:24+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-05.05590_isabelle-nightly-slow","2017-11-05 00:18:23+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-06.05592_isabelle-nightly-slow","2017-11-06 00:18:23+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G" "jenkins_2017-11-07.05590_isabelle-nightly-slow","2017-11-07 00:18:23+01","\N","\N","\N","\N","\N","\N","\N","\N","polyml-5.7.1","x86_64-linux","-H 4000 --maxheap 10G"
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
