Hi, Makarius, Thank you very much for these information, and I apologize that I reply this so late. I will start working on topics related to parallel computer algebra during this summer, and is very interested in knowing how these examples work so well from your Poly/ML paper so that I can take advantage of the mechanism in the paper to my work, therefore I was asking for these useful examples presented in the paper. I will ask more if I have further questions.
Thank you very much, Yue On Fri, Feb 12, 2010 at 6:11 PM, Yue K. Li <[email protected]> wrote: > ---------- Forwarded message ---------- > From: Makarius <[email protected]> > Date: Fri, Feb 12, 2010 at 2:21 PM > Subject: Re: [polyml] Code examples in Parallel Poly/ML and Isabelle/ML paper > To: Yue Li <[email protected]> > Cc: [email protected] > > > 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
