[isabelle-dev] Slowdown of ConcurrentGC

[Makarius]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Network_Security_Policy_Verification_timing.png
Type: image/png
Size: 12432 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180512/fbde1c79/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Network_Security_Policy_Verification.csv
Type: text/csv
Size: 15811 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180512/fbde1c79/attachment-0002.csv>