Makarius wrote:
On Wed, 12 May 2010, Michael Norrish wrote:
Cygwin is not really relevant, but I suppose that, out of idle curiosity, it would nice to know if Posix.Process.exec worked there.
I have checked the (long) mail exchange with David from 2 years ago, when we sorted out many issues to make it work the way it is in Isabelle2008 or later, until today.
Attached is an earlier experiment involving straight-forward fork/exec with join/kill operations. Here is an example on Cygwin:
ML> elapsed_time (fn () => join (fork "true")) (); 0.719
That's almost a second penalty. The delay depends on various factors, including the size of the running ML process. The best I can get here is approx. 0.4 seconds.
The problem is that there's no equivalent to "fork" on Windows so Cygwin has to simulate it. I don't know how it does it but it's bound to be expensive. Ironically, the CreateProcess call in Windows does exactly what's required most of the time by providing a combined "fork" and "exec".
On Linux on the same hardware class the result is like that:
ML> elapsed_time (fn () => join (fork "true")) (); 0.102
These 100ms are somehow intrinsic to the way the Poly/ML runtime system invokes external processes. David can explain that better. (I wonder if the builtin delay loop is still required these days.)
The reason has to do with the limitations of the "waitpid" system call. The "select" system call allows a thread to block until any of a set of file descriptors become available or until a time-out whichever comes first. There's no equivalent when waiting for a process. The only choices are to block indefinitely or to include the WNOHANG option bit and poll the current status and return immediately. We don't want a thread to block indefinitely because if it receives an interrupt through Thread.Thread.interrupt() it needs to be woken up. That means the only option is to use polling. The current code blocks for 100ms then checks again. I guess an alternative would be to use an extra internal (blocking) thread and pipe and have the ML thread use "select" on the pipe. I could do that if this is a significant problem. Another possibility would be for your code to install a signal handler for SIGCHLD.
David