[isabelle-dev] Isabelle/ML/Scala parallel computation and PIDE execution

[Makarius]

Over the past few weeks, I have reworked a few aspects of parallel 
computation in Isabelle/ML and Isabelle/Scala, e.g. to provide 
Par_List.map on both sides with more or less the same semantics 
(concerning max. threads and cancelation of tasks).  As Lars Hupel has 
pointed out, Scala .par is not the best way to do parallel computation, so 
more Isabelle library support for that makes sense.

This unification of ML/Scala libraries has lead to small re-adjustments 
like Synchronized.value with actual synchronization in e557a9ddee5f.

This seamingly tiny change (NEWS: "subtle change of semantics with minimal 
potential for INCOMPATIBILITY") has lead to various bad consequences, such 
as huge waste of cycles on more than 4 cores and spurious deadlocks. 
(There were some private mail threads about both, concluding eventually 
with ba2a326fc271 and e99f706aeab9.)


After some more refinements, there is even less access to costly 
Synchronized.value than before and more plain value-oriented programming. 
Moreover, I have pushed some reforms from the bottom to the top of PIDE. 
In particular, the global execution is no longer sequential over its 
ongoing history (e.g. current 702e0971d617).

The practical consequence of the latter should be improved scheduling of 
long-running print functions, notably Sledgehammer.  This means the 
Sledgehammer panel should work more asynchronously from the document 
processing, even after several edits of the text.


So far this is just an intermediate outline of some reforms that came 
about spontaneously.  We are right in the middle between two releases, so 
more is likely to happen.

As usual, problems, observations etc. can be posted at any time, but it is 
important to refer to a *current* and *explicit* repository version.


 	Makarius

----------------------------------------------------------------------------
                 http://stop-ttip.org  1,235,896 Participants
----------------------------------------------------------------------------