1

I am using GNU time for benchmarking and would like to measure real, user and sys time to the nearest millisecond. That is, I want to measure seconds to 3 decimal places, not the default 2. Does GNU time offer such an option?

Jacob Baird
  • 11
  • Are you using the built-in/keyword time or the external time? – muru Aug 16 '19 at 15:50
  • I'm using the build-in time, I believe. It is /usr/bin/time. – Jacob Baird Aug 16 '19 at 15:53
  • Sorry, I believe I am using GNU time. I am executing the command from a Node.js Child Process, which itself is running inside a Docker container. The default behaviour is to print:

    %Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k %Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps

     – Jacob Baird Aug 16 '19 at 15:58
  • Related: https://unix.stackexchange.com/questions/70653/increase-e-precision-with-usr-bin-time-shell-command – Arkadiusz Drabczyk Aug 16 '19 at 17:13
  • Good find. Read that earlier but I wasn't able to get much from it. – Jacob Baird Aug 16 '19 at 18:11

1 Answers1

0

It doesn't look like you could, the man page does list a number of formatting options, but there's no provision for setting the accuracy. For example, %e, %S and %U seem to always give the output with two decimal places.

On the other hand, Bash's builtin time does support setting the number of digits after the decimal point, up to 3, so you might be able to use it to get what you wanted. The TIMEFORMAT environment variable controls the output format:

$ TIMEFORMAT='real: %3R user: %3U sys: %3S cpu: %P' bash -c 'time sleep 1.233'
real: 1.234 user: 0.000 sys: 0.000 cpu: 0.00

Or just without setting TIMEFORMAT, since the default output also shows three digits. It does separate minutes though:

$ bash -c 'time sleep 1.233'

real    0m1.234s
user    0m0.000s
sys     0m0.000s

The getrusage() system call gives the times as struct timeval, so up to microseconds, so I suppose you could make your own implementation of time to get more accuracy. A whole another thing is how accurate the numbers actually are.

ilkkachu
  • 138,973
  • Thanks! I was calling time from a Node.js child_process instance which enforced use of GNU time for some reason or another. I was finally able to enforce bash time using /bin/bash -c "time <my command>". Shame about GNU time not allowing formatting, though. – Jacob Baird Aug 16 '19 at 18:10
  • @JacobBaird, oh, right, the default format already shows three digits, so it's not even necessary to modify it. Setting TIMEFORMAT to %3R %3U %3S might make the output easier to parse, since there would be less to parse and you'd get raw seconds instead of seconds + minutes. – ilkkachu Aug 16 '19 at 19:12