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.
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.)
Makarius
fun elapsed_time f x =
let
val now = Time.now ();
val res = f x;
val _ = TextIO.output (TextIO.stdOut, Time.toString (Time.now () - now) ^
"\n");
in res end;
fun fork cmdline =
let
val _ = TextIO.flushOut TextIO.stdOut;
val {infd = in1, outfd = out1} = Posix.IO.pipe ();
val {infd = in2, outfd = out2} = Posix.IO.pipe ();
in
(case Posix.Process.fork () of
SOME pid =>
(Posix.IO.close in1;
Posix.IO.close out2;
{pid = pid, stdin = out1, stdout = in2})
| NONE =>
(Posix.IO.close out1;
Posix.IO.close in2;
Posix.IO.dup2 {old = in1, new = Posix.FileSys.wordToFD 0w0};
Posix.IO.dup2 {old = out2, new = Posix.FileSys.wordToFD 0w1};
Posix.IO.close in1;
Posix.IO.close out2;
Posix.Process.execp ("bash", ["bash", "-c", cmdline]);
OS.Process.terminate OS.Process.failure)
handle _ => OS.Process.terminate OS.Process.failure)
end;
fun join {pid, stdin, stdout} =
let
val _ = Posix.IO.close stdin;
val _ = Posix.IO.close stdout;
fun wait () =
(case #2 (Posix.Process.waitpid (Posix.Process.W_CHILD pid, [])) of
Posix.Process.W_STOPPED _ => wait ()
| status => status);
in
(case wait () of
Posix.Process.W_EXITED => 0
| Posix.Process.W_EXITSTATUS 0wx82 => raise SML90.Interrupt
| Posix.Process.W_EXITSTATUS w => Word8.toInt w
| Posix.Process.W_SIGNALED s =>
if s = Posix.Signal.int then raise SML90.Interrupt
else 256 + LargeWord.toInt (Posix.Signal.toWord s))
end;
fun kill {pid, stdin, stdout} =
Posix.Process.kill (Posix.Process.K_PROC pid, Posix.Signal.int);
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
