[isabelle-dev] Slowdown of ConcurrentGC

[Makarius]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ConcurrentGC_timing.png
Type: image/png
Size: 7103 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180512/7f984bb9/attachment.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ConcurrentGC.csv
Type: text/csv
Size: 4504 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180512/7f984bb9/attachment.csv>