Re: [isabelle-dev] Slowdown of ConcurrentGC
Hi Makarius, > I have studied this a bit further. The interval > 75130777ece4:d45b78cb86cf contains more than just the string type > change, but it is still the main thing. Here are also other sessions in > similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498: > > * faster: HOL-IMP, HOL-Quickcheck_Examples, > Network_Security_Policy_Verification, Pre_Perron_Frobenius, > JiveDataStoreModel, Partial_Function_MR > > * slower: Tarskis_Geometry, XML, Cauchy distangling the ancient misunderstaning of char in Isabelle vs. various character-related types in several target languages may indeed come at a certain price in exotic situations; anyway I will have a look at those sessions whether something meaningful can be derived from them. 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] Slowdown of ConcurrentGC
On 12/05/18 00:01, Makarius wrote: > The Isabelle/AFP timing charts show a recent slowdown of ConcurrentGC: > > https://isabelle.sketis.net/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_ConcurrentGC > > See also the attached copies of the chart and data file (the web version > updates itself dynamically). At the transition of Isabelle/75130777ece4 > to d45b78cb86cf there is a notable change of string type representation > in HOL (by Florian Haftmann). > > My impression is that the overall slowness of ConcurrentGC is due to its > rather aggressive use of string literals (and disjunctions over them). > So a small change in the representation can have a big impact here, and > there might be not proper way around it. > > I am posting this observation here nonetheless, in the hope that it > could be still improved. I have studied this a bit further. The interval 75130777ece4:d45b78cb86cf contains more than just the string type change, but it is still the main thing. Here are also other sessions in similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498: * faster: HOL-IMP, HOL-Quickcheck_Examples, Network_Security_Policy_Verification, Pre_Perron_Frobenius, JiveDataStoreModel, Partial_Function_MR * slower: Tarskis_Geometry, XML, Cauchy In particular, I am glad that Network_Security_Policy_Verification is now back to its fairly good timing from some months ago (see attachments and this thread: https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07717.html). Many other sessions have become much faster, without becoming slow before. Very good. >From the (few) ones that become slower, small sessions like XML or Cauchy might help to see clearly what are the reasons for it. Makarius session_name,chapter,pull_date,afp_pull_date,isabelle_version,afp_version,timing_elapsed,timing_cpu,timing_gc,ml_timing_elapsed,ml_timing_cpu,ml_timing_gc,maximum_heap,average_heap,stored_heap,status Network_Security_Policy_Verification,AFP,2018-05-12 00:18:16,2018-05-12 00:40:11,42d63ea39161,92ec39882136,114,1137000,0,1137526,1135707,68343,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-09 00:40:12,2018-05-09 00:40:12,2b18a770911f,f0b5c34b4a85,0,0,0,0,0,0,0,0,0,failed Network_Security_Policy_Verification,AFP,2018-05-08 00:18:06,2018-05-08 00:40:17,2277fe496d78,4a788844049b,1136000,1134000,0,1134349,1132316,66615,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-07 00:18:09,2018-05-07 00:39:33,0b66aca9c965,ba558fdf522c,1143000,114,0,1140346,1138024,68710,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-05 00:18:07,2018-05-05 00:39:54,b25ccd85b1fd,ad1d95d5ace6,1147000,1144000,0,1145196,1142685,66892,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-05 00:18:07,2018-05-05 00:18:07,b25ccd85b1fd,ba558fdf522c,1139000,1135000,0,1136775,1134010,65072,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-03 00:40:00,2018-05-03 00:40:00,b91c4acc1aaf,8c085909633b,1135000,1132000,0,1132392,1130552,66562,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-02 00:18:06,2018-05-02 00:18:06,3931ed905e93,8c085909633b,1147000,1144000,0,1145221,1142700,68684,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-05-01 00:39:45,2018-05-01 00:39:45,7811d8828775,83c48344a96f,1141000,1138000,0,1138705,1136855,64598,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-30 00:18:26,2018-04-30 00:40:00,9e077a905209,d2059b336ac3,1147000,1144000,0,1145257,1142771,71377,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-29 00:18:24,2018-04-29 00:40:00,ebd179b82e20,5d888a880328,1153000,115,0,1150513,1148483,66650,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-28 00:18:28,2018-04-28 00:39:53,e98988801fa9,f0759507c46c,1136000,1133000,0,1134476,1131261,63513,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-27 00:18:31,2018-04-27 00:40:52,f76e8180c498,6dacb8b19575,1153000,1151000,0,1150874,1149165,73225,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-24 00:18:31,2018-04-24 00:18:31,75130777ece4,efd58f8b1659,2863000,2861000,0,2861387,2859236,69096,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-23 00:18:24,2018-04-23 00:18:24,c8a506be83bd,efd58f8b1659,2877000,2874000,0,2875073,2872755,66381,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-22 00:18:27,2018-04-22 00:40:19,b91a043c0dcb,b6b5f48aa576,2944000,2941000,0,2941441,2939396,67053,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-21 00:18:17,2018-04-21 00:40:10,32d19862781b,4bf3efef63d6,2938000,2935000,0,2935833,2933481,63102,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-20 00:18:13,2018-04-20 00:40:19,72e1d5da30c6,715c7d15b226,2884000,2881000,0,2881937,2879495,64859,0,0,0,finished Network_Security_Policy_Verification,AFP,2018-04-19 00:18:17,2018-04-19
[isabelle-dev] Slowdown of ConcurrentGC
The Isabelle/AFP timing charts show a recent slowdown of ConcurrentGC: https://isabelle.sketis.net/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_ConcurrentGC See also the attached copies of the chart and data file (the web version updates itself dynamically). At the transition of Isabelle/75130777ece4 to d45b78cb86cf there is a notable change of string type representation in HOL (by Florian Haftmann). My impression is that the overall slowness of ConcurrentGC is due to its rather aggressive use of string literals (and disjunctions over them). So a small change in the representation can have a big impact here, and there might be not proper way around it. I am posting this observation here nonetheless, in the hope that it could be still improved. Makarius session_name,chapter,pull_date,afp_pull_date,isabelle_version,afp_version,timing_elapsed,timing_cpu,timing_gc,ml_timing_elapsed,ml_timing_cpu,ml_timing_gc,maximum_heap,average_heap,stored_heap,status ConcurrentGC,AFP,2018-05-11 00:18:11,2018-05-11 00:39:55,53b4e204755e,2d77f99edaa7,9419000,30025000,0,9415959,30023100,1907620,10933,7817,0,finished ConcurrentGC,AFP,2018-05-10 00:18:13,2018-05-10 00:39:50,f6a22490cca8,c3cfeceda7a0,9505000,30094000,0,9502443,30091596,2149764,10649,7342,0,finished ConcurrentGC,AFP,2018-05-09 00:40:12,2018-05-09 00:40:12,2b18a770911f,f0b5c34b4a85,9655000,30126000,0,9652887,30123908,2133668,9412,5266,0,finished ConcurrentGC,AFP,2018-05-08 00:18:06,2018-05-08 00:40:17,2277fe496d78,4a788844049b,9491000,29751000,0,9488339,29749640,2028628,10380,5722,0,finished ConcurrentGC,AFP,2018-05-07 00:18:09,2018-05-07 00:39:33,0b66aca9c965,ba558fdf522c,959,30077000,0,9587001,30074596,2088648,9111,5544,0,finished ConcurrentGC,AFP,2018-05-05 00:18:07,2018-05-05 00:39:54,b25ccd85b1fd,ad1d95d5ace6,993,30837000,0,9927226,30835360,2350904,9053,5058,0,finished ConcurrentGC,AFP,2018-05-05 00:18:07,2018-05-05 00:18:07,b25ccd85b1fd,ba558fdf522c,9733000,30766000,0,9730146,30763944,2195328,9579,6815,0,finished ConcurrentGC,AFP,2018-05-04 00:18:04,2018-05-04 00:39:39,262b42b59151,8527935d1eed,9473000,29794000,0,9470880,29792080,2049904,9119,5590,0,finished ConcurrentGC,AFP,2018-05-03 00:40:00,2018-05-03 00:40:00,b91c4acc1aaf,8c085909633b,9635000,3004,0,9632922,30037860,2216072,9042,5140,0,finished ConcurrentGC,AFP,2018-05-02 00:18:06,2018-05-02 00:18:06,3931ed905e93,8c085909633b,955,30187000,0,9547094,30184516,2077948,9875,7086,0,finished ConcurrentGC,AFP,2018-05-01 00:39:45,2018-05-01 00:39:45,7811d8828775,83c48344a96f,938,29263000,0,9377459,29261500,1923772,10412,6441,0,finished ConcurrentGC,AFP,2018-04-30 00:18:26,2018-04-30 00:40:00,9e077a905209,d2059b336ac3,9597000,29982000,0,9594967,29979888,2119664,10292,5485,0,finished ConcurrentGC,AFP,2018-04-29 00:18:24,2018-04-29 00:40:00,ebd179b82e20,5d888a880328,9622000,29991000,0,9619983,29989176,2178860,9115,5230,0,finished ConcurrentGC,AFP,2018-04-28 00:18:28,2018-04-28 00:39:53,e98988801fa9,f0759507c46c,9318000,29461000,0,9315451,29459256,1890596,11199,8016,0,finished ConcurrentGC,AFP,2018-04-27 00:18:31,2018-04-27 00:40:52,f76e8180c498,6dacb8b19575,918,29103000,0,9177587,29101188,1867552,10893,7873,0,finished ConcurrentGC,AFP,2018-04-26 00:18:14,2018-04-26 00:40:14,d45b78cb86cf,ba5034372e45,9336000,2953,0,914,29527536,1824824,10972,8041,0,finished ConcurrentGC,AFP,2018-04-24 00:18:31,2018-04-24 00:18:31,75130777ece4,efd58f8b1659,8515000,26414000,0,8512839,26412460,1702600,9317,6766,0,finished ConcurrentGC,AFP,2018-04-23 00:18:24,2018-04-23 00:18:24,c8a506be83bd,efd58f8b1659,8463000,26393000,0,8460524,26391036,1774012,8780,6000,0,finished ConcurrentGC,AFP,2018-04-22 00:18:27,2018-04-22 00:40:19,b91a043c0dcb,b6b5f48aa576,853,26929000,0,8527717,26926600,1786652,9153,6799,0,finished ConcurrentGC,AFP,2018-04-21 00:18:17,2018-04-21 00:40:10,32d19862781b,4bf3efef63d6,8266000,25957000,0,8263230,25954752,1646084,8637,5570,0,finished ConcurrentGC,AFP,2018-04-20 00:18:13,2018-04-20 00:40:19,72e1d5da30c6,715c7d15b226,8599000,27063000,0,8596321,27061196,1799108,10302,5560,0,finished ConcurrentGC,AFP,2018-04-19 00:18:17,2018-04-19 00:40:51,0a2a1b6507c1,e97d5b6aa872,8277000,26169000,0,8274600,26166888,1680696,8782,5599,0,finished ConcurrentGC,AFP,2018-04-18 00:18:13,2018-04-18 00:39:37,ae76012879c6,7c3ea015c632,8157000,25645000,0,8154626,25643008,1639424,10336,5667,0,finished ConcurrentGC,AFP,2018-04-17 00:18:19,2018-04-17 00:40:12,c0ebecf6e3eb,7a9e13c52757,802,25273000,0,8017863,25271084,1585068,10194,5721,0,finished ConcurrentGC,AFP,2018-04-16 00:18:15,2018-04-16 00:39:47,b65c4a6a015e,54e15e31c3ea,8233000,25828000,0,8230843,25826424,1705004,10176,5589,0,finished ConcurrentGC,AFP,2018-04-15 00:18:06,2018-04-15 00:39:23,349c639e593c,d2f502a794b7,7988000,25242000,0,7985231,25239672,1713680,10287,7309,0,finished ConcurrentGC,AFP,2018-04-14 00:18:09,2018-04-14
