// unsigned int service_clock ();