[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some
bulwahn at in.tum.de
Wed Jul 20 16:57:52 CEST 2011
While trying to parallelize different testing approaches under the hood
of the quickcheck tool in Isabelle, I frequently noticed that Interrupt
exceptions were thrown.
Inspecting this problem closer, I distilled the following small example
that shows an unexpected behaviour:
Par_List.get_some (fn x => if x = 3 then SOME 3 else NONE) [0,1,2,3];
for i in $(seq 1 100); do ../../../bin/isabelle-process -e 'use_thy
"Test"' -q; done
Running this theory on lxbroy10, in 21 of 100 times, it raises an
Is this a general issue when working with Par_List.get_some?
N.B.: In my scenario, the function that is parallelized is much larger
(and should take at least 100 ms for its execution, there I could
observe similar behaviour as well).
Also on my local machine, the exceptions do not occur, so it is related
to the machine's configuration as well.
More information about the isabelle-dev