[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Mon May 12 16:01:06 CEST 2014
On Thu, 8 May 2014, David Matthews wrote:
> On 08/05/2014 11:25, Makarius wrote:
>> 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 the last 7 years of using Poly/ML threads, I have occasionally wondered
about the extra options (and complexity) of phthreads, compared to your
somewhat sanitized view on it. (I have always found it beneficial that
Poly/ML presents an abstracted version of the range of platforms it
supports. If we wanted the bare-metal system programming interfaces, we
would have to go for OCaml, but its threads are not very useful.)
The last time to reconsider ML thread priorities (or the lack thereof) was
in summer 2013, when I made the worker thread farm "monotonic" in the
sense that it is never interrupted, until its execution fragments become
inaccessible to the PIDE document model. As a consequence, the PIDE
protocol thread has to work against the worker thread farm running at full
speed on many cores, which causes some noticable delays in the update of
the document state (but this is not such a big deal, because PIDE is
asynchronous). Thread priorities or other policies might change that, but
I am unsure about the practical relevance.
Thread priorities in the standard APIs seem to be a left-over from quite
different hardware: a single-core CPU doing round-robin scheduling of
threads. If we take typical mid-range hardware from today, it has
something like 2 CPU modules, each with 4 real cores, times 2 because of
hyperthreading. These are 16 hardware threads. So even if the PIDE
protocol thread, and another speculative "high-priority PIDE execution
thread" get top priority, there are plenty of free slots on the hardware
that will be filled by the OS with low-priority threads. Thus we have
again the situation of 2 threads running "against" many others, which use
the caches and pipelines, heat the hardware etc. and thus degrade system
Running just the 2 threads alone in Turbo Boost mode, might make a big
difference in reactivity. See also
http://en.wikipedia.org/wiki/Hyperthreading for some general explanations
of what might be going on in the Silicon -- only Intel knows the details,
and AMD is quite different anyway.
> 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.
This sounds to me like it is not worth to persue further. To much
low-level system tinkering for my taste.
> 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.
Explicit "yield" is a bit awkward to program with, but for people who like
to burn a lot of CPU cycles in their tools it might be adequate to get
burdened with such extra details. Note that the Isabelle/ML future thread
farm could already implement that with the existing Poly/ML threading
model, similarly to the explanation of "threadSuspended" in
The latter document is interesting for other reasons as well, e.g. the
hint to "reinterrupt itself" in order to deal with deferred
InterruptedException that Poly/ML already does on its own. I have
rediscovered some of that just last week, when porting Isabelle/ML
concurrency modules to Isabelle/Scala. With a bit more of that, I might
eventually approximate the general level of convenience and quality of
Poly/ML multithreading on the JVM.
The JVM does have thread priorities, but I don't think that using them
changes the situation significantly. These guys still allocate the full
number of virtual hardware threads by default, and thus maximize the CPU
burn factor instead of performance and reactivity.
More information about the isabelle-dev