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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
