Re: [isabelle-dev] Isabelle build status with timing information

2017-05-10 Thread Makarius 
On 10/05/17 13:07, Lawrence Paulson wrote:
> Thanks for those graphs, which are really interesting. Note in
> particular the sharp drops in elapsed time or heap for Analysis,
> Probability, Algebra and several others. What gets the credit for this?

This is indeed the canonical question. In a later iteration, the
presentation should allow to click there and go to the changeset id in
the repository.

Right now I can only answer this informally: it is in the vicinity of
http://isabelle.in.tum.de/repos/isabelle/rev/0f3fdf689bf9 where I have
rearranged some parent images, both for clarity and for performance
improvements. This was motivated by the still pending reform of
session-qualified theory names.

In fact, since such session rearrangements can sometimes go amiss, that
project also motivated to get the performance charts right now, so that
we can proceed more boldly without messing it all up.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle build status with timing information

2017-05-10 Thread Lawrence Paulson 
Thanks for those graphs, which are really interesting. Note in particular the 
sharp drops in elapsed time or heap for Analysis, Probability, Algebra and 
several others. What gets the credit for this?

Larry

> On 10 May 2017, at 10:55, Makarius  wrote:
> 
> After a delay of some weeks (actually several months since October 2016)
> there is now an updated version of the classic Isabelle build status
> with timing information, see
> http://isabelle.in.tum.de/devel/build_status and its source
> http://isabelle.in.tum.de/repos/isabelle/annotate/96b4799a2e04/src/Pure/Admin/isabelle_devel.scala#l82
> 
> 
> This demonstrates that it is still possible to produce performance
> charts in the quality that we've known from the past. Two main factors
> are relevant for this:
> 
>  (1) The physical measurements need to be done without disturbance by
> other processes, especially no other test processes running in parallel
> on the same CPU/memory node. (The numactl tool can be a great help.)
> 
>  (2) Data plotting requires care about the gnuplot installation. For
> reasons that I don't understand, various Linux distributions (e.g
> Gentoo) can show quite bad interpolation in gnuplot, and make the data
> look worse than it really is. For the above, I have just compiled
> gnuplot-5.0.6 from the original source and suddenly it worked smoothly.
> 
> 
> The data for the charts is collected as plain log files for archival
> purposes in /home/isatest/cronjob/log/ at TUM. This directory is
> uploaded every day to a PostgreSQL database server in the background
> (only accessible by "isatest"). It can then be used with tools like
> "isabelle build_status" to make the charts.
> 
> In addition, there is a small database snapshot in SQLite format:
> http://isabelle.in.tum.de/devel/build_log.db -- e.g. for exploration
> with sqlitebrowser (which also supports minimal plotting). Here is an
> example query for its "Execute SQL" window:
> 
> SELECT pull_date, heap_size FROM isabelle_build_log
> WHERE session_name = 'HOL-Analysis' AND  build_host = 'lxbroy9' AND
> threads = 1
> ORDER BY pull_date
> 
> Comparing this with threads = 2 shows that heap images produced by a
> multi-threaded build process are slightly bigger, which I did not know
> before. So this is one of the usual starting points for performance and
> resource usage tuning, based on such relevant performance measurements.
> 
> 
> There is more in the data that is not plotted yet, e.g. the precise
> relation of tests run with threads=1,2,4,6. Or online heap usage, thread
> activity, future tasks, etc. for an individual process (ml_statistics).
> 
> At last we are no longer "flying blind" ...
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Isabelle build status with timing information

2017-05-10 Thread Makarius 
After a delay of some weeks (actually several months since October 2016)
there is now an updated version of the classic Isabelle build status
with timing information, see
http://isabelle.in.tum.de/devel/build_status and its source
http://isabelle.in.tum.de/repos/isabelle/annotate/96b4799a2e04/src/Pure/Admin/isabelle_devel.scala#l82


This demonstrates that it is still possible to produce performance
charts in the quality that we've known from the past. Two main factors
are relevant for this:

  (1) The physical measurements need to be done without disturbance by
other processes, especially no other test processes running in parallel
on the same CPU/memory node. (The numactl tool can be a great help.)

  (2) Data plotting requires care about the gnuplot installation. For
reasons that I don't understand, various Linux distributions (e.g
Gentoo) can show quite bad interpolation in gnuplot, and make the data
look worse than it really is. For the above, I have just compiled
gnuplot-5.0.6 from the original source and suddenly it worked smoothly.


The data for the charts is collected as plain log files for archival
purposes in /home/isatest/cronjob/log/ at TUM. This directory is
uploaded every day to a PostgreSQL database server in the background
(only accessible by "isatest"). It can then be used with tools like
"isabelle build_status" to make the charts.

In addition, there is a small database snapshot in SQLite format:
http://isabelle.in.tum.de/devel/build_log.db -- e.g. for exploration
with sqlitebrowser (which also supports minimal plotting). Here is an
example query for its "Execute SQL" window:

SELECT pull_date, heap_size FROM isabelle_build_log
WHERE session_name = 'HOL-Analysis' AND  build_host = 'lxbroy9' AND
threads = 1
ORDER BY pull_date

Comparing this with threads = 2 shows that heap images produced by a
multi-threaded build process are slightly bigger, which I did not know
before. So this is one of the usual starting points for performance and
resource usage tuning, based on such relevant performance measurements.


There is more in the data that is not plotted yet, e.g. the precise
relation of tests run with threads=1,2,4,6. Or online heap usage, thread
activity, future tasks, etc. for an individual process (ml_statistics).

At last we are no longer "flying blind" ...


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev