[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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 
performance.

Running just the 2 threads alone in Turbo Boost mode, might make a big 
difference in reactivity. See also
http://en.wikipedia.org/wiki/Intel_Turbo_Boost versus 
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
http://docs.oracle.com/javase/8/docs/technotes/guides/concurrency/threadPrimitiveDeprecation.html

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.


 	Makarius