[isabelle-dev] PolyML.Statistics

[Alexander Krauss]

Hi all,

Recent SVN versions of the PolyML runtime system contain a useful
statistics interface, which can help improve the understanding of how
Isabelle really works.

In essence, you can query various runtime parameters, such as the heap
size, number of garbage collections, threads etc. Tracking these
values over time during a session (and possibly correlating it with
other events) can give useful insights, and has already helped us
understanding performance issues with the new importer.

As as example, attached is a graph of the heap consumption when
building HOL (as of 26c1a97c7784), running on my laptop. The graph
itself is not very exciting, but in other situations, this may show
bottlenecks. I am currently trying to generate the same for
JinjaThreads, which may be more interesting.

Technically, there are two ways of retrieving the data:

  a) via PolyML.Statistics.getLocalStats for the local polyml process

  b) via PolyML.Statistics.getRemoteStats for some remote process
     identified by its PID.  (the two PolyML instances then communicate
     via a memory-mapped file).

The data above was generated via b) and a somewhat ad-hoc script
(which is plain PolyML, not Isabelle/ML) which I attach for those
who want to play with it.

Obviously, we should be collecting this information on a regular basis.
Here, I think, approach a) is more convenient: An Isabelle session
would then report its own runtime statistics in a suitable way, as part
of the logs.

More concretely, here is what I think we should do:

1) Introduce an "Isabelle Statistics Interface" that exposes the data
    in a portable way as part of the ML compatibility layer (reporting
    dummy values if the runtime does not have statistics).

2) The Isabelle session runtime maintains a reporting thread, which
    emits the current values in configured time intervals, via
    some existing channel (tracing, stderr, ...?).

3) A simple script in the spirit of Admin/profiling_report extracts the
    data from the logs and outputs them in a plot-friendly format, 
preferably CSV.

I guess I'll try to do 1., which should be easy but needs review from
Makarius. Then, 2 can be prototyped in user-space first.

Any comments? Ideas?

Alex

-------------- next part --------------
A non-text attachment was scrubbed...
Name: HOL_heap.png
Type: image/png
Size: 30784 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120411/b6f8c903/attachment-0001.png>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: polyml_collector
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120411/b6f8c903/attachment-0001.ksh>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: polyml_collector.ML
Type: text/x-ocaml
Size: 2791 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120411/b6f8c903/attachment-0001.bin>