Thanks Makarius.
A few of us at NICTA have ported this change to our various versions of
Isabelle and begun playing with it. It seems to improve the situation
sometimes, though we haven't yet got a feel for when in particular it
helps. In fact, we haven't really understood what the change does.
On 07/05/14 22:59, Makarius wrote:
On Mon, 5 May 2014, Makarius wrote:
Users running on batteries might also want a mode that restricts all
threads to the behaviour above.
Have you tried that with "threads = 1" (there is also a special
treatment for high-priority prints in that mode)? So far I guess
that most people run with defaults, without any idea of the tuning
parameters.
See also:
changeset: 56875:f6259d6fb565
user: wenzelm
date: Tue May 06 16:05:14 2014 +0200
files: etc/options src/Pure/PIDE/command.ML
description:
explicit option parallel_print to downgrade parallel scheduling, which
might occasionally help for big and heavy "scripts";
In principle this is an instance of the "too many options" syndrome,
but here the implicit change of behaviour on 1 core is merely made
explicit. Moreover, according to the "waterbed-syndrome" in its
positive sense, it means that options added here inevitably cause
other old/obsolete options to be removed faster.
I completely agree that having too many options is a problem. There's no
point having them if noone knows that they're there, or which ones to
try. That said, I think it's a good path for performance adjustments
which might or might not be helpful. I suspect you could get away with
adding far more options than you plan to have in the end, and keep only
the ones that end up with a quorum of users. I'm a bit of an optimist
though.
This sounds a bit too pragmatic and opportunistic to me. What is
special about print tasks anyway, apart from their priority? The
recent concept for asynchronous print functions makes print tasks
rather general, and there are more automated provers or disprovers in
that category than actual printing.
What is even more important than prints, is the main protocol thread,
which presently needs to work against the whole farm of worker threads
to update certain administrative structures of the document model. If
I knew a proper way to reduce the priority (or to pre-empt) worker
threads for that, I would do it. But it probably needs some work by
David Matthews on the ML thread infrastructure.
Consider me an unashamed pragmatist. I see a similarity between
task/thread scheduling in Isabelle and task/thread scheduling in
operating systems. All modern operating systems are full of ad-hoc
heuristics designed to bump up the priority of tasks that are likely to
create I/O requests or update things for the user. A parallel "make",
for instance, will run much faster if the OS prioritises the compile
tasks that are still reading files ahead of the ones that have begin
compiling and computing. This keeps the disk working throughout the
build. Windows raises the priority of in-focus windows, and Mac OS X
pushes the audio threads of apps up to the highest priority, etcetera.
I may have misspoken with regard to "print task". I guess I meant "task
that will produce output which at some point the user has directly
requested into their output panel, query panel etc". If we see the user
as an external resource like a hard disk, these are the tasks we need to
front-load to keep the external task running at full capacity. I see the
some of the other output tasks, which possibly produce counterexamples
or which produce squiggly lines which are possibly helpful, as lower
priority.
Preempting long-running tasks would change the tradeoffs a lot. Another
possibility would be to introduce a yield-point (cooperative
multitasking) which a task can execute, which will possibly cause its
execution to be delayed in favour of a higher priority task. Adding that
to the tactic combinators would make nearly all Isabelle workloads much
finer-grained.
Well, those are just my thoughts. Thanks for the adjustment, I hope it
solves our responsiveness problems.
Best wishes,
Thomas.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
