On 08/05/2014 11:25, Makarius wrote:
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.
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.
I've had a look at providing thread priority in the Poly/ML thread
package and I may have a go at including something. Poly/ML leaves
thread scheduling to the pthreads library which really means to the OS
and what is available depends on the particular OS. In general pthreads
allows control over both priority and "scheduling policy". I've done
some tests on what various OSs allow for user (i.e. non-privileged) threads.
Linux. Does not allow either policy or priority to be changed.
Mac OS X. Allows both policy and priority to be changed.
Cygwin/Windows. Single scheduling policy. Allows priority to be changed.
FreeBSD. Allows priority but not policy to be changed.
What this means is that ML code that wants to set a thread priority is
going to have to make some enquiries about the priority range allowed.
It looks as though adding a "yield" function would not be hard. There's
a question about whether you would really want to use it. There is a
cost involved even if there is no other thread that can be scheduled so
you wouldn't want to call it too often.
David
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
