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
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to