makarius at sketis.net
Fri Apr 25 15:27:53 CEST 2014
On Wed, 23 Apr 2014, Makarius wrote:
> I am presently considering to discontinue actors altogether, and merely
> use the thread task pool, explicit threads, and typed channels between
> them. But I also need to see how Akka actors do it today, to get a few
> more ideas, before trimming it down to the simplest possible approach.
I have done this now in Isabelle/e1317a26f8c0 (and the row of changes
After looking at the approx. 500 pages Akka manual, its sources, and the
sources of scala.concurrent, I learned a lot how big industrial-strength
concurrency frameworks are done these day. Akka does have a purpose (e.g.
for the Twitter server infrastructure), but not for us -- we are just
doing a little shared-memory multiprocessing with one machine and two
So most of the PIDE "operating system" functionality is now re-implemented
by more basic means, in just 48 hours. It is interesting that this can be
done, but that is mostly a port of existing Isabelle/ML modules from
src/Pure/Concurrent. The resulting Scala/PIDE sources are more concise,
and the implementation presumably more robust and efficient.
This means we no longer depend on the deprecated scala.actors library at
That was a fine master / PhD project by Phillip Haller some years ago, but
it is no longer actively maintained. In the early years of PIDE, I spent
a lot of energy to isolate its hidden performance problems, e.g. due to
the use of standard mutable structures from Java like
instead of the more canonical queue that is now a hybrid Isabelle module
The Isabelle/ML Mailbox uses our canonical Queue implementation, and the
Isabelle/Scala the same canonical Queue from the scala.collection library,
which explains the meaning of the word "canonical". The Mailbox started
as a toy example some years ago for concurrent programming in ML, but
seems to perform quite well in the Prover IDE.
In the coming weeks / months we need to watch out for new problems that
were inevitably introduced by such substantial changes of the PIDE
mechanics. I also need to start thinking about "converging" towards the
release this summer.
More information about the isabelle-dev