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 00:40:51,0a2a1b6507c1,e97d5b6aa872,2894000,2891000