[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some

Lukas Bulwahn bulwahn at in.tum.de
Wed Jul 20 16:57:52 CEST 2011


Hello all,


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:

theory Test
imports Main
begin

ML {*
   Par_List.get_some (fn x => if x = 3 then SOME 3 else NONE) [0,1,2,3];
*}

end

bash script:
   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 
Interrupt exception.

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.



Lukas





More information about the isabelle-dev mailing list