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