On Thu, 8 May 2014, Thomas Sewell wrote:
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.
The important point is that a system like Isabelle cannot be built on the
basis of pragmatism. It is occasionally helpful to recall the cultural
foundations on which one is standing.
The system can be used pragmatically, or rather practically, of course.
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.
Definitely. I've introduced the slogan of "Isabelle as logical operating
system" already in 2007, when the parallel batch mode with its ML threads
was still new. Many years later that has become reality in PIDE
interaction, but it was much harder to get there than anticipated. In
recent years I have become more cautious in the ambitions of what the
system is meant to do. It is already too far ahead of anything else in the
ITP world, and hardly anyone understands how it really works.
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.
Luckily Isabelle no longer depends on "make" and its many historical
problems. The Isabelle build tool is fast, because it does not access all
these files over and over again. Thus the need for extra tricks is
avoided, by giving up old habits from the 1970-ies.
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.
That sounds rather obvious, but also like even more complication. David
Matthews has provided a nice simplified version of pthreads in Poly/ML.
He could probably do more, but even on the more complex JVM the influence
on thread scheduling is limited.
My canonical approach in such situations is to ask: Is there a way to
avoid the need for all that extra weight? It requires looking at concrete
applications carefully, to "disprove" their approach as something that
could be done differently, with less impact on resources.
That is not pragmatic, but it is how genuine scientific progress usually
works.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
