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
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,

isabelle-dev mailing list

Reply via email to