function ishtime()
{
static $startts=0;
if($startts==0) $startts=time();

$a=gettimeofday();
return (($a['sec']-$startts)+($a['usec']/1000000));
}