On 05/06/2017 11:27, Makarius wrote:
On 05/06/17 10:35, [email protected] wrote:
Both this (with Posix.Process open):
case fork() of
NONE => (exece(proc,proc::args,env')
and this:
case fork() of
exece(executable,nm_args,env)
seem to be causing us grief, particularly on a recent Linux, PolyML 5.7 and
under conditions of some memory load.
Is there a better idiom we might use?
For Isabelle, I have made many variations and refinements in the past 10
years -- without fork/exec due to portability problems. The present
state in this quest for perfection is here (both for ML and Scala):
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/System/bash.ML
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/System/bash.scala
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/Admin/bash_process/bash_process.c
The main idea is to use plain OS.Process.system (Posix) or
Windows.simpleExecute with a Thread.fork around it. Thus a synchronous
process execution is management asynchronously by a separate thread.
I would certainly recommend the use of OS.Process.system rather than
fork and exec. I wonder if there is a problem if there is a need for a
GC or some other action before the child process can actually perform
the exece ? Looking at the code, Poly/ML sets a "singleThreaded" flag
in the child process to indicate that it should not expect any other
threads to be running but there is a lot of state in the run-time system
associated with threads. It may be that this state would have to be
explicitly reset.
OS.Process.system does use fork/exec underneath on Unix but the exec
occurs immediately after the fork within the same C function. There is
also special-case code for OS.Process.system on Cygwin since fork/exec
is very inefficient on Windows.
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
