value to be written into tick_compare in tick_hardclock(). While
we were taking care that the value to be written was at least TICK_GRACE
ticks in the future, a vector interrupt could happen between calculating
the value and writing it. If it took longer than TICK_GRACE to complete
(which is doubtful for a single device-triggered vector interrupt, but
quite likely for some IPIs), the value written would be in the past
and tick interrupts (which drive hardclock and statclock) would stop
until %tick wraps around, which takes a long time.
Also, increase TICK_GRACE from 1000 to 10000 for good measure.
Reported by: kris
Reviewed by: jake
Approved by: re (scottl)
9078f61c55