Previously, these both used gettimeofday() which is both expensive
to call, and not monotonic.

This fixes system.clock_ticks in JS and various internal bits. for
when the UTC wall clock jumps.

While we're here, fix the documention of system.clock_ticks