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,9590000,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,9930000,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,30040000,0,9632922,30037860,2216072,9042,5140,0,finished
ConcurrentGC,AFP,2018-05-02 00:18:06,2018-05-02 00:18:06,3931ed905e93,8c085909633b,9550000,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,9380000,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,9180000,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,29530000,0,9333314,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,8530000,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,8020000,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 00:40:06,06bce659d41b,1372a2309c0c,8322000,26229000,0,8320293,26227348,1757912,8655,5361,0,finished
ConcurrentGC,AFP,2018-04-12 00:18:07,2018-04-12 00:39:57,959b0aed2ce5,a5a33a4a38f1,8149000,25568000,0,8146522,25566172,1548772,9087,7010,0,finished
ConcurrentGC,AFP,2018-04-12 00:18:07,2018-04-12 00:18:07,959b0aed2ce5,403715e495c8,7944000,25223000,0,7942044,25221448,1451916,9253,7271,0,finished
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
