your mail
Matthew Fluet
mfluet@intertrust.com
Sat, 28 Jul 2001 13:37:54 -0700 (PDT)
> So I suggest the following process structure:
>
> Get the current (real) time.
>
> Make the directory in /tmp. cat standard input into a file in that
> directory. (We now have the first possible answer.) fork off brain
> process. This process will get standard input the file just made and
> a single argument which is directory to put answer in. It's
> (initial) current directory will be /tmp.
>
> Wait, polling directory, cleaning up longer files until time runs out or
> child (brain) exits. If time runs out, kill brain. Print shortest
> file in directory to standard output. Remove the file and the
> directory and exit.
>
> Sound sane and safe?
My only modification is that the brain process should also get the time
(which it can understand to be a rough estimate, given that the polling
process took some time). Maybe we can use that to ensure that we do some
local improvments on a big file with a short time rather than be killed
without returning any new results.