Fix floating-point noise in pg_stat_us_to_ms()

Hi hackers,

while reviewing [1], I noticed that the IO timings displayed in pg_stat_io can 
produce floating-point noise like:

postgres=# select read_time from pg_stat_io where read_time > 0;
      read_time
---------------------
  2.2640000000000002
 0.08700000000000001

That's because 0.001 cannot be represented exactly in binary floating
point. I think this output looks weird, even if understandable. Note that with
extra_float_digits set to 0 you don't see the noise (but 1 is the default).

The attached patch changes pg_stat_us_to_ms() so that it uses a division
by 1000.0 instead as it's correctly rounded, see for example:

postgres=# SELECT (9 * 0.001::float8)::text;
         text
----------------------
 0.009000000000000001
(1 row)

postgres=# SELECT (9::float8 / 1000.0)::text;
 text
-------
 0.009
(1 row)

Given that / 1000.0 is the most common way to do this kind of computation in the
code tree, I think that it makes sense to update pg_stat_us_to_ms() to do so.

Thoughts?

[1]: https://www.postgresql.org/message-id/akH0SxXlXPNjD%2BR5%40bdtpg

Regards,

-- 
Bertrand Drouvot
PostgreSQL Contributors Team
RDS Open Source Databases
Amazon Web Services: https://aws.amazon.com