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