On 05/06/2017 11:27, Makarius wrote:
On 05/06/17 10:35, Michael.Norrish at data61.csiro.au 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... http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/System... http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/Admin/bash_proc...
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