RFC 1589: A Kernel Model for Precision Timekeeping