gettimeofday() fehlerhaft?

[hawkmaster1]

Hallo zusammen, ich habe gerade ein merkwürdiges Verhalten der gettimeofday() Funktion festgestellt.

Wenn ich den Code unten mehrmals hintereinander ausführe dann habe ich in den meisten Fällen die Mikrosekunden $mytime_arr['usec'] als sechstelligen Wert. Ab und zu aber nur fünfstellig.

$mytime_arr = gettimeofday();
$milliseconds = $mytime_arr['usec'] / 1000;
echo "1. die milliseconds sind " . $mytime_arr['usec'] . " und durch 1000 $milliseconds <br>";
$roundedmilliseconds = round($milliseconds);
echo "die rounded milliseconds sind $roundedmilliseconds <br>";
$millisecondstimestamp = $mytime_arr['sec'] . $roundedmilliseconds;

Ich brauche später einen 13 stelligen Zeitstempel. Aber so ist das ja nicht zuverlässig weil ab und zu Stellen fehlen bzw. zu wenig sind. Ist das ein Fehler von gettimeofday()?

vielen Dank Gruss hawk