[isabelle-dev] performance regression for simp_all

[Makarius]

On Thu, 11 Aug 2011, Brian Huffman wrote:

> Recently I've been hacking on a bunch of proof scripts using the 
> development version of Isabelle, and I noticed that when processing 
> proof scripts, I often get a noticeable pause at uses of "simp_all". The 
> same pause does not occur with Isabelle2011.

> lemma shows "True" and "True"
> by (simp, simp)
> (* 0.001s elapsed time, 0.000s cpu time, 0.000s GC time *)
>
> lemma shows "True" and "True"
> by simp_all
> (* 0.253s elapsed time, 0.004s cpu time, 0.000s GC time *)

This is indeed a bit slow, although it is not CPU time, only some latency 
of the tty loop (which is inherently synchronous and thus slow).

http://isabelle.in.tum.de/repos/isabelle/rev/aaaa13e297dc improves startup 
time of the worker thread farm significantly, and I've got real times in 
the range of 0.003s -- 0.005s on my "old" machine from 2 years ago with 
Proof General.

Really old machines with only 1 core should not experience any slowdown 
from the parallel combinator, because multithreading is not enabled.


> The first bad revision is:
> changeset:   42372:6cca8d2a79ad
> user:        wenzelm
> date:        Sat Apr 16 23:41:25 2011 +0200
> summary:     PARALLEL_GOALS for method "simp_all";
>
> http://isabelle.in.tum.de/repos/isabelle/rev/6cca8d2a79ad
>
> Was this change supposed to *improve* performance? Was the performance 
> impact tested? Maybe the performance penalty only appears when 
> interactively stepping through proofs, and not in batch mode?

Yes, it improves some sessions like HOL-Hoare_Parallel, probably also some 
larger AFP ones, but we still don't have any old-style isatest statistics.

The worst-case overhead for batch mode should be neglible -- same for 
Isabelle/jEdit which is closer to batch mode than PG tty mode.


 	Makarius