On Thu, 11 Feb 2010, Yue Li wrote:

Recently I read the paper "Efficient Parallel Programming in Poly/ML and Isabelle/ML" published in DAMP'10. It's really a nice paper for me to read. Especially, I'm deeply impressed by the good scalability and cpu utilization of multithreading implementation as shown in the data section. I'm very interested in the parallel implementation of Poly/ML, and would like to try to use it. Here may I ask is there any way for me to obtain the testing examples used in the paper's experiment so that I could study and play with the parallel features?

In the paper we point to a particular repository version of Isabelle (with Mercurial changeset id), but it is easier to use the official Isabelle2009-1 release that came out a few weeks later -- the parallel infrastructure did not change much in between.

See http://isabelle.in.tum.de and http://isabelle.in.tum.de/installation.html in particular. A suitable Poly/ML compilation for many platforms is also included here -- this is actually required to use the Isabelle logic images from that website.

To work with Isabelle/ML, you can mostly forget about everything involving Proof General and Emacs, which causes the main problems for first-time installation. If you have the GNU "rlwrap" ("readline wrapper") tool on your system, you already get a convenient tty interface. E.g. run it like this:

$ Isabelle2009-1/bin/isabelle tty -l HOL Welcome to Isabelle/HOL (Isabelle2009-1: December 2009)

exit

ML>

Strictly speaking, the "Pure" image is sufficient, instead of the slightly bulky "HOL" one, but the latter is available as precompiled on the Isabelle download site.

If you want to compile only the core Isabelle/Pure system you can do it like this:

$ Isabelle2009-1/build Pure ... Press RETURN to compilation of

Pure

Started at Fri Feb 12 21:01:22 CET 2010 (polyml-5.3.0_x86-linux on ...) Building Pure ... Finished Pure (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.90) Finished at Fri Feb 12 21:01:33 CET 2010 0:00:11 elapsed time, 0:00:10 cpu time, factor 0.90

And invoke it as above, replacing "HOL" by "Pure" in the command line.

The "applications" from the paper are all relatively big Isabelle logic sessions, with formal definitions and proofs being processed by semi-automatic tools. The ideas behind parallelizing formal document processing is further explained in http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf

You need to use "isabelle usedir ..." and/or "isabelle make" with certain parameters in certain directories to reproduce the examples. I can give you further details on demand -- even some Scala script to produce the graphs from the paper. Note that certain server-class hardware sometimes needs extra tweaking to get good results, while high-end workstations usually work without further worries (notably Mac Pro).

Probably your main interest will be the Isabelle/ML library for working with synchronized variables, future values etc. All of this is in Isabelle2009-1/src/Pure/Concurrent/. The ML names in the paper have been slightly shortened.

Here is an example:

val x = Future.fork (fn () => 1 + 1);

The ML toplevel pretty printer will display the value of x, just type "x" again at the toplevel later. You can also use Future.join explicitly.

Here is the example from section 4.2:

fun loop () : int = loop ();

val g = Task_Queue.new_group NONE; val x = Future.fork_group g loop; val y = Future.fork_group g (fn () => 1 div 0);

The library implementation is fine-tuned towards the particular needs of Isabelle proof checking, but it should be straight forward to turn this into a fully generic ML library. (I would be willing to assist anybody in doing this, but I can myself only maintain the Isabelle/ML version.)

Makarius