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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
