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.