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