[isabelle-dev] Remaining uses of Proof General?

[David Matthews]

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