Time bug is kernel bug, not MLton

[Matthew Fluet]

> Well  now  I  am  confused  again.  I figured that what was going on was that
> while one CPU was running the MLton process, which was doing  a  system  call
> (the  getrusage()),  the other was handling a clock tick and incrementing the
> MLton processes system time.  This was where the race was going on.  At least
> in  traditional  Unix  kernels  and Linux in the old days, the system was not
> interruptable, so this couldn't happen on a single CPU machine.
>
> What kernel were you running where you saw the bug on a non-SMP machine?

2.4.2 (The Red Hat 7.1 kernel.)