Hello polyglots,
I was wondering, do any of you have some little examples or chunks of code that do some parallel computation, possibly using some of the code in Isabelle's "Pure/Concurrent" dir?
Say, for instance, I have a stack of names and an (expensive) function from names to bools. I'd like to spawn a handful of workers and wait for them to finish. The workers then pop names off, compute the boolean function and push the names back on to "true" and "false" stacks. This kind of setup should be pretty straightforward to implement, but a few pointers as far as what structs to use and how to use them would be useful.
Thanks! Aleks
On Tue, 21 Jun 2011, Aleks Kissinger wrote:
Say, for instance, I have a stack of names and an (expensive) function from names to bools. I'd like to spawn a handful of workers and wait for them to finish. The workers then pop names off, compute the boolean function and push the names back on to "true" and "false" stacks. This kind of setup should be pretty straightforward to implement, but a few pointers as far as what structs to use and how to use them would be useful.
The main entry point for Isabelle/Pure parallel programming is structure Future.
What is the purpose of the stack in the above application? It reminds me a little of the task queue that is already managed in the Future implementation, and is a bit more complex. (Its general policy is FIFO, with optional priorities or dependencies.)
If the above is meant to be a parallel version of List.partition, it could be done like that:
fun parallel_partition pred list = List.partition I (Par_List.map pred list);
Structure Par_List in src/Pure/Concurrent/par_list.ML can serve as general introduction to managed evaluation with futures. (There are a few special things concerning parallel exception handling in this library.)
Makarius
Yes! Par_List (and by association Future) seems to be exactly the kind of thing I'm looking for.
The specific task is as follows. I have a list of graphs and want to know if any graph is (roughly speaking) a subgraph of another. I'd like to do this in time bounded by N*(N/k) instead of N^2, for k the number of cores on the computer. Par_List.exists seems to be a good candidate.
On a related note, any idea why Par_List.exists would raise the "EXCEPTIONS []" exception? The predicate function shouldn't be throwing exceptions (at least it doesn't with List.exists substituted in), and doesn't use side effects.
a
On 21 June 2011 13:29, Makarius makarius@sketis.net wrote:
On Tue, 21 Jun 2011, Aleks Kissinger wrote:
Say, for instance, I have a stack of names and an (expensive) function from names to bools. I'd like to spawn a handful of workers and wait for them to finish. The workers then pop names off, compute the boolean function and push the names back on to "true" and "false" stacks. This kind of setup should be pretty straightforward to implement, but a few pointers as far as what structs to use and how to use them would be useful.
The main entry point for Isabelle/Pure parallel programming is structure Future.
What is the purpose of the stack in the above application? ?It reminds me a little of the task queue that is already managed in the Future implementation, and is a bit more complex. ?(Its general policy is FIFO, with optional priorities or dependencies.)
If the above is meant to be a parallel version of List.partition, it could be done like that:
?fun parallel_partition pred list = ? ?List.partition I (Par_List.map pred list);
Structure Par_List in src/Pure/Concurrent/par_list.ML can serve as general introduction to managed evaluation with futures. ?(There are a few special things concerning parallel exception handling in this library.)
? ? ? ?Makarius
On Tue, 21 Jun 2011, Aleks Kissinger wrote:
On a related note, any idea why Par_List.exists would raise the "EXCEPTIONS []" exception? The predicate function shouldn't be throwing exceptions (at least it doesn't with List.exists substituted in), and doesn't use side effects.
EXCEPTIONS [] means spontanous cancellation, say via external interrupt or internal sigalling from peer task groups. E.g. there could be a stack overflow in one future task. The Poly/ML runtime systems turns this into exception Interrupt, which the future scheduler will propagate to other futures of the same group, turning it into EXCEPTIONS [] at some point.
(There can also some boundary cases with *incorrect* treatment in my implementation. I have had rare situations where there are some surprises concerning this.)
Anyway, you can check with Multithreading.max_threads := 1 without any special things getting in between. If you now see Interrupt it means Poly/ML RTS failure, typically stack overflow (max. 64MB) or virtual memory exhaustion (max. 2GB). You can then try with x86_64 to see if the problem persists, although it might lead to disk thrashing instead.
Assuming that you have Isabelle2011, this is how to configure x86_64 in your $HOME/.isabelle/etc/settings file:
ML_PLATFORM="$ISABELLE_PLATFORM64" ML_HOME="$ISABELLE_HOME/contrib/polyml-5.4.0/$ML_PLATFORM" ML_SYSTEM=polyml-5.4.0 ML_OPTIONS="-H 1000" ML_SOURCES="$ML_HOME/../src"
You then need to build Pure for that platform:
Isabelle2011/build Pure
or on Mac OS X:
Isabelle2011.app/Isabelle/build Pure
Makarius
On Tue, 21 Jun 2011, Makarius wrote:
On Tue, 21 Jun 2011, Aleks Kissinger wrote:
On a related note, any idea why Par_List.exists would raise the "EXCEPTIONS []" exception? The predicate function shouldn't be throwing exceptions (at least it doesn't with List.exists substituted in), and doesn't use side effects.
EXCEPTIONS [] means spontanous cancellation, say via external interrupt or internal sigalling from peer task groups. E.g. there could be a stack overflow in one future task. The Poly/ML runtime systems turns this into exception Interrupt, which the future scheduler will propagate to other futures of the same group, turning it into EXCEPTIONS [] at some point.
(There can also some boundary cases with *incorrect* treatment in my implementation. I have had rare situations where there are some surprises concerning this.)
I have spent some more time on this suspicious situation. It seems that the "boundary case" is simply any parallel program that makes serious use of future group cancelation, such as Par_List.exists or Par_List.get_some.
This is now addressed by the changeset http://isabelle.in.tum.de/repos/isabelle/rev/de5c79682b56 in the main Isabelle repository. Normally I do not recommend to "use" arbitrary snapshots, unless you have a lot of extra time for building and testing the system.
Which Isabelle/ML version are you actually using? It should be resonably easy to apply the change manually to older versions as well.
Makarius
-
aleks0＠gmail.com -
makarius＠sketis.net