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

[Makarius]

On Wed, 20 Jul 2011, Lukas Bulwahn wrote:

> 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.

Here is a simpler way to reproduce it:

   fun test () =
     ignore (Par_List.get_some (fn x => if x = 3 then SOME 3 else NONE) [0, 1, 2, 3]);

   funpow 1000 test ();

The problem is also independent of ML versions and platforms.


In Isabelle/318ca53e3fbb it works half-way, when the outer execution 
context is not a worker task itself, e.g. on the tty.

This problem of delayed interrupt propagation has existed in many 
variations from the beginning of the parallelization efforts.  The 
situation has continously improved, and every time I have learned a new 
aspect of the physics of the parallel hardware.  I hope this will converge 
eventually.


 	Makarius