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