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