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,1140000,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,1140000,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,1150000,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,0,2892277,2889979,70549,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-18 00:18:13,2018-04-18 00:39:37,ae76012879c6,7c3ea015c632,2851000,2848000,0,2848718,2846479,65164,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-17 00:18:19,2018-04-17 00:40:12,c0ebecf6e3eb,7a9e13c52757,2888000,2885000,0,2886576,2884123,68830,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-16 00:18:15,2018-04-16 00:39:47,b65c4a6a015e,54e15e31c3ea,2857000,2854000,0,2855328,2852947,63448,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-15 00:18:06,2018-04-15 00:39:23,349c639e593c,d2f502a794b7,2891000,2888000,0,2889579,2887106,69213,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-14 00:18:09,2018-04-14 00:40:06,06bce659d41b,1372a2309c0c,2865000,2863000,0,2863664,2861409,64090,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-12 00:18:07,2018-04-12 00:39:57,959b0aed2ce5,a5a33a4a38f1,2912000,2909000,0,2910224,2907355,67032,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-12 00:18:07,2018-04-12 00:18:07,959b0aed2ce5,403715e495c8,2891000,2888000,0,2889109,2886474,67080,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-11 00:18:03,2018-04-11 00:39:27,e9f66b35d636,14c80444e85d,2831000,2828000,0,2829301,2826970,67752,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-08 00:18:08,2018-04-08 00:18:08,9541f2c5ce8d,6c7328a7eef2,2892000,2889000,0,2890520,2887985,65302,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-05 00:18:10,2018-04-05 00:42:45,78a64f3f7125,6b525e899f93,2888000,2887000,0,2886366,2886006,74976,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-31 00:18:03,732c0b059463,c31f76fe5d07,2907000,2906000,0,2905331,2904200,69738,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-31 00:18:03,732c0b059463,c31f76fe5d07,2869000,2867000,0,2866821,2865905,67962,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-31 00:18:03,732c0b059463,c31f76fe5d07,2916000,2915000,0,2913904,2913475,70698,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-31 00:18:03,732c0b059463,c31f76fe5d07,2907000,2905000,0,2904483,2903899,65509,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-29 00:40:29,732c0b059463,e9aaf72d221c,2866000,2865000,0,2863939,2864088,70508,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-29 00:18:07,732c0b059463,c4818b0d2411,2889000,2886000,0,2886702,2885090,68108,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-29 00:18:07,2018-03-29 00:18:07,732c0b059463,c4818b0d2411,2887000,2886000,0,2884994,2884493,67791,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-25 00:18:05,2018-03-25 00:18:05,83902fff6243,91efd45cb040,2892000,2891000,0,2890049,2889525,66008,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-25 00:18:05,2018-03-25 00:18:05,83902fff6243,91efd45cb040,2804000,2802000,0,2801658,2800867,69817,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-24 00:18:05,2018-03-24 00:39:28,49a34b2fa788,0f8992e9d350,2890000,2888000,0,2888118,2886739,85295,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-23 00:18:04,2018-03-23 00:39:29,0b70405b3969,7b0364ae0185,2890000,2889000,0,2888017,2887494,72426,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-21 00:18:04,2018-03-21 00:39:38,9cc32b18c785,5e73b2289f6e,2851000,2850000,0,2849142,2849100,65685,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-21 00:18:04,2018-03-21 00:18:04,9cc32b18c785,a0d561998f20,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-03-20 00:18:03,2018-03-20 00:18:03,465f43a9f780,5e73b2289f6e,2801000,2800000,0,2798405,2798798,67756,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-19 00:18:03,2018-03-19 00:39:37,c88044b10bbf,5409eaef5cf4,2873000,2873000,0,2871487,2871378,68544,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-18 00:17:59,2018-03-18 00:39:38,736673784fac,f3899ff0e1c8,2807000,2805000,0,2804712,2803840,72277,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-17 00:18:01,2018-03-17 00:18:01,839a624aabb9,f3899ff0e1c8,2883000,2882000,0,2881142,2880997,68442,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-15 00:17:58,2018-03-15 00:49:41,cd1cac824ef8,90bc651cbc2c,2886000,2886000,0,2884400,2884216,68310,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-14 00:17:58,2018-03-14 00:17:58,8374c80165e1,90bc651cbc2c,2890000,2889000,0,2887972,2888079,70509,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-13 00:18:05,2018-03-13 00:39:21,07f5588f2735,2ec9f121e14e,2883000,2882000,0,2881143,2880958,66944,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-12 00:18:03,2018-03-12 00:39:09,b027c97c77c9,97e87fffff43,2910000,2910000,0,2908517,2908308,70936,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-11 00:18:05,2018-03-11 00:18:05,8b3d9a91706e,97e87fffff43,2889000,2889000,0,2887504,2887899,69789,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-09 00:18:03,2018-03-09 00:18:03,839de121665c,97e87fffff43,2882000,2882000,0,2879906,2880525,70459,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-09 00:18:03,2018-03-09 00:18:03,839de121665c,97e87fffff43,2871000,2872000,0,2869745,2870413,66908,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-08 00:18:04,2018-03-08 00:40:10,7655e6369c9f,08e91a3b31fc,2876000,2876000,0,2874274,2874948,68277,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-07 00:18:02,2018-03-07 00:50:17,44efac3d8638,9e3ecdedcb13,2846000,2847000,0,2844636,2845248,67842,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-04 00:18:31,2018-03-04 00:56:00,f4b1cf9e7010,255a81ed190a,2876000,2876000,0,2874462,2875009,68079,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-02 00:18:33,2018-03-02 00:50:08,e512938b853c,6cada0d3cb26,2877000,2877000,0,2875230,2875741,64740,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-03-01 00:18:32,2018-03-01 00:18:32,7b0b0a02b303,6cada0d3cb26,2818000,2818000,0,2816006,2816544,71103,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-27 00:18:33,2018-02-27 00:49:38,f91c437f6f68,fd517455d6c7,2844000,2844000,0,2842185,2842709,65135,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-27 00:18:33,2018-02-27 00:18:33,f91c437f6f68,1823d8d10be1,2819000,2819000,0,2817063,2817684,66287,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-24 00:18:32,2018-02-24 00:50:47,3f611f444c2d,d961a099a3fa,2839000,2839000,0,2837056,2837890,63845,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-23 00:18:34,2018-02-23 00:50:02,34e0e0d5ea7c,fb1cf909b8b1,2796000,2796000,0,2794554,2795133,70275,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-22 00:18:33,2018-02-22 00:49:56,817944aeac3f,016b5fa3a87f,2794000,2794000,0,2792327,2793046,68866,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-21 00:18:32,2018-02-21 00:49:44,00c436488398,ff3dd1d15915,2870000,2870000,0,2867946,2868624,64184,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-20 00:18:31,2018-02-20 00:18:31,52b0d4cd4be7,ff3dd1d15915,2914000,2914000,0,2912401,2912559,54218,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-19 00:18:33,2018-02-19 00:49:46,8f4810b9d9d1,87ff8e7e553d,2909000,2909000,0,2907047,2907592,57969,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-18 00:18:33,2018-02-18 00:18:33,f6e351043014,87ff8e7e553d,2839000,2839000,0,2837285,2837590,56227,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-17 00:18:33,2018-02-17 00:18:33,3817a93a3e5e,87ff8e7e553d,2831000,2831000,0,2829615,2829837,56861,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-16 00:18:32,2018-02-16 00:50:09,967213048e55,0b9dcb4a0341,2915000,2914000,0,2913062,2912983,56949,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-15 00:18:33,2018-02-15 00:18:33,e4e57da0583a,0b9dcb4a0341,2865000,2865000,0,2863003,2863513,66808,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-14 00:18:32,2018-02-14 00:18:32,4939494ed791,0b9dcb4a0341,2777000,2776000,0,2774732,2774483,58985,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-13 00:18:33,2018-02-13 00:50:14,3b3188ae63da,cd9c197778cd,2797000,2798000,0,2795566,2796210,67278,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-12 00:18:30,2018-02-12 00:18:30,686679dedb46,cd9c197778cd,2787000,2786000,0,2784779,2784679,67476,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-11 00:18:33,2018-02-11 00:18:33,6fd9902057f5,cd9c197778cd,2825000,2824000,0,2822977,2822777,56613,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-10 00:18:32,2018-02-10 00:49:47,8b19a8a7f029,ec36dda080ec,2849000,2847000,0,2846907,2846176,58806,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-09 00:18:31,2018-02-09 00:49:22,1a636c22d85c,b5e453029b52,2833000,2833000,0,2831071,2831244,58079,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-08 00:18:31,2018-02-08 00:49:32,4a3d657adc62,155bf0fe338a,2886000,2886000,0,2884541,2884559,62283,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-06 00:18:32,2018-02-06 00:49:43,ed0a7090167d,d8f547b136ef,2777000,2777000,0,2775260,2775821,66603,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-06 00:18:32,2018-02-06 00:18:32,ed0a7090167d,26f074817c9a,2865000,2865000,0,2863318,2863861,57549,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-04 00:18:31,2018-02-04 00:18:31,a93cf1d6ba87,d8f547b136ef,2801000,2801000,0,2798916,2799368,64224,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-04 00:18:31,2018-02-04 00:18:31,a93cf1d6ba87,d8f547b136ef,2908000,2908000,0,2906506,2906838,60659,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-02-03 00:18:32,2018-02-03 00:49:57,c555f1778dd8,a6e1af6e0ad2,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-02-02 00:18:34,2018-02-02 00:49:40,e13378b304dd,724f6bceac14,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-02-01 00:18:31,2018-02-01 00:49:47,c46910a6bfce,0b99a44c62fb,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-01-31 00:18:32,2018-01-31 00:49:44,aefe7a7b330a,2f3bdae911bb,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-01-30 00:18:29,2018-01-30 00:49:42,a7de81d847b0,455f23697b09,990000,990000,0,988227,988223,55898,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-27 00:18:30,2018-01-27 00:49:52,9624711ef2de,de6627121446,1010000,1007000,0,1007677,1005803,55037,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-24 00:18:31,2018-01-25 00:18:31,b8e093f7a802,1372df8e7299,1003000,1003000,0,1001667,1001298,55408,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-24 00:18:31,2018-01-24 00:49:43,b8e093f7a802,45181c49c624,1000000,999000,0,997779,997805,54485,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-24 00:18:31,2018-01-24 00:18:31,b8e093f7a802,b066c154e09a,1002000,1002000,0,1000590,1000556,57636,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-23 00:18:36,2018-01-23 00:49:44,3d33847dc911,9bd921d1073b,1000000,999000,0,998002,998010,54484,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-22 00:18:30,2018-01-22 00:49:43,dce667537607,14c525483c56,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-01-21 00:18:30,2018-01-21 00:49:25,14d3163588ae,1a588d68418f,1001000,1000000,0,999420,998731,55375,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-20 00:18:30,2018-01-20 00:49:35,056be95db703,c1bc6a2cb955,995000,995000,0,993490,993479,52780,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-19 00:18:31,2018-01-19 00:50:08,fe6bcf0137b4,23020f3805c1,1001000,1001000,0,999640,999647,55810,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-18 00:18:30,2018-01-18 00:59:43,aab817885622,e00de3e653c2,1001000,1000000,0,998923,998829,55325,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-01-17 00:18:31,2018-01-17 00:49:46,b0ae74b86ef3,cda7cc51c330,0,0,0,0,0,0,0,0,0,failed
Network_Security_Policy_Verification,AFP,2018-01-15 00:18:29,2018-01-15 00:49:30,e446505a4ec6,f787608b0ab7,999000,999000,0,997696,997682,53989,0,0,0,finished
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
