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

[Lukas Bulwahn]

On 07/24/2011 12:06 AM, Makarius wrote:
> 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.
>
For tool developers, this means as consequence, we either do not use 
Par_List.get_some or ensure by other means, that we know if the outer 
execution context is a worker task or not, when being invoked, right?

> 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.
>
Eventually, this context-sensitive behaviour implemented above can then 
be removed if nested Par_List operations are allowed.

Lukas

>
>     Makarius