extern double dtime_now (void);