Email Gateway (Aug 15 2020 at 23:20): Email Gateway (Aug 15 2020 at 23:20):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
There is something that I have noticed that makes optimizing the processing time of Isabelle theories more difficult:
The timings reported in the "Timings" panel are highly variable, especially under near-thrashing conditions.
An inference that can be performed in a few tens of ms can, under conditions of severe memory stress, be reported as
taking many minutes. This makes optimization difficult, as the timing results are not repeatable.
I would like the timing numbers to only reflect actual computation time expended, not incidental delays that are
dependent on the memory conditions in which the particular inference is run. It does not match my current goals to
spend time trying to read the source code to try to figure out why this occurs, but I am hoping that someone who already
understands the timing instrumentation code would be able to make simple modifications to make the results repeatable
and ultimately more useful.
Thanks.
Email Gateway (Aug 31 2020 at 12:30):From: Makarius <makarius@sketis.net>
I read from this observation that big Isabelle applications become more and
more memory-bound: having too little heap space requires rather expensive
operations for garbage-collection and sharing of live data.
David Matthews, the grand master behind Poly/ML, has recently provided more
facilities for runtime statistics of memory management. I have already
integrated some of this into the Isabelle/jEdit monitoring facilities (for the
next release, presumably in Feb-2021). This confirms the impression that
overall heap usage is now more relevant than individual timing.
How much memory do you actually have on your machine?
For non-trivial applications 16 GB are already standard, and 32-64 GB are not
uncommon for really big things.
Makarius
Email Gateway (Aug 31 2020 at 14:49):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I have 24GB.
I understand what you are saying, but I am asking for the timing numbers not to be confounded by non-CPU overhead.
That way, even if I am running with a few extra browser tabs open I will see the same timing results and will still
know whether what I am doing is optimizing something or making pointless changes.
Thank you.
Email Gateway (Aug 31 2020 at 15:04):From: Makarius <makarius@sketis.net>
On 31/08/2020 16:48, Eugene W. Stark wrote:
I understand what you are saying, but I am asking for the timing numbers not to be confounded by non-CPU overhead.
That way, even if I am running with a few extra browser tabs open I will see the same timing results and will still
know whether what I am doing is optimizing something or making pointless changes.
Isabelle as an application of symbolic logic mainly allocates tree data
structures in memory, while gargabe collection deallocates them later on on.
Thus it is inherently hard to isolate the "non-CPU overhead": it is the main
part of the program.
I have 24GB.
That it not much for the size of your typical applications on AFP.
Do you see a chance to double the memory on that hardware?
I have 32GB on my development machine, and don't do really big Isabelle
applications.
Makarius
Email Gateway (Aug 31 2020 at 17:38):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I could increase to 32GB on this hardware if I throw away some of the existing memory.
But that is certainly not my point.
An operating system (such as Linux, which is what I am using) provides system calls (cf getrusage(2),
clock_gettime(2)) that an application can use to measure resource consumption in various ways:
CPU time used in user mode
CPU time used in kernel mode
Wall clock time
For Isabelle (using JEdit), CPU time is consumed by Java (to run JEdit) and CPU time is consumed by
Poly/ML (to do inferences). The CPU time spent by Java, while potentially significant, has to do with
the manipulation of the annotated syntax tree of the theories being edited, depends primarily on the
size of that document and its annotations (not on the complexity of proof steps) and is not of interest
to me here. In any case, I assume that this time is not intended to be included in the figures reported
in the "Timings" panel and the values one sees if one CTRL-hovers over "by", "apply", etc.
I would expect that the times shown in the "Timings" panel are intended to reflect the actual CPU time
spent by ML in user mode. CPU time spent in user mode by ML may be partitioned into time running ML code
and time spent doing garbage collection. It does not include time spent with the CPU idle waiting for paging,
or CPU time spent running other unrelated processes. It probably also ought not to include CPU time spent
in kernel mode. As the page fault rate of the ML process increases to the point of saturating the paging
devices, the wall clock time taken to accomplish a particular task will increase dramatically.
The CPU time spent in system mode will also increase, though this will typically not be that significant.
In addition, once the heap size reaches its maximum value (as a result of actual hardware limitation or
artificial software limits placed on the ML process) the fraction of live data in the heap will become larger
and larger and consequently the garbage collector will consume more and more CPU time to perform the same
underlying computational task. However, as far as I know, the ML implementation accounts separately for
CPU time used in garbage collection versus CPU time used to run ML code, so it is not necessarily the
case that garbage collection time should be a significant component of the "Timings" numbers.
But you know all that. Let me try again to make what I believe is a very simple point: Empirical
observation shows that figures reported under "Timings" do not reflect only time spent by ML running
ML code in user mode: depending on the system conditions under which a task is run, they apparently also
include either CPU time spent in garbage collection, wall clock time spent waiting for paging,
or a combination of the two. This is not desirable because it makes the timings not repeatable.
The timings would be more useful if they would more or less reflect the amount of user CPU time spent
in user mode to run ML code to accomplish a particular computational task. These numbers ought to agree
closely with the amount of wall clock time it would take to accomplish that same task on a system in which
RAM size is large enough that there is an insignificant page fault rate, and on which there is no
competition for CPU with unrelated applications. Under those conditions, one can expect the "Timings"
numbers to be repeatable across separate runs, and that optimizations that reduce the numbers reported
under "Timings" will reflect actual improvements in wall clock time when the task is run under conditions
where memory limitations are not significant.
Well, that is the point I am trying to make. Perhaps you are trying to say that one ought to be optimizing
memory consumption rather than CPU consumption. Well that would certainly be a valid point, but to do that
that would require a "Memory usage" panel that reports the amount of allocation performed in conjunction with
each basic proof step. I would expect this to be a more complex instrumentation task than recording CPU
usage associated with each basic proof step. Since there is likely to be a tradeoff between memory utilization
and CPU consumption, it is not clear to me at the moment that this is primarily what one wants to do.
Email Gateway (Sep 01 2020 at 10:44):From: Makarius <makarius@sketis.net>
The Timing panel works with elapsed time. See also the general explanations in
section 6.1 of the "jedit" manual (Documentation panel).
If you want repeatable results for a single proof command, you can approximate
it like this:
* Use sufficient physical memory to avoid use of virtual memory by the
underlying OS (no disk thrashing while timing).
* Avoid non-trivial applications running in parallel.
* Disable Isabelle/ML multithreading by using system option threads=1 (e.g.
via the Isabelle/jEdit menu Plugins / Plugin Options / Isabelle / General /
Threads.
* Use a well-defined initial state of the ML heap to minimize subsequent
garbage collection, e.g. via
ML "ML_Heap.share_common_data ()"
The latter is rather drastic: it is only required for substantial ML heap
usage, as in your own AFP/Bicategory
https://isabelle.sketis.net/devel/build_status/AFP_64bit_8_threads/index.html#session_Bicategory
Makarius
Last updated: Apr 18 2024 at 20:16 UTC