>  HZ may be defined on your machine, but it isn't on my (Xeon) machine.

Are you sure?  Please note that HZ will not show up in grep -w HZ 
/usr/include because the right header file further up the tree.

On Solaris:
/usr/include/sys/param.h:#define        HZ              
((clock_t)_sysconf(_SC_CLK_TCK))

On 32-bit Linux:
/usr/include/asm-i386/param.h:#define HZ sysconf(_SC_CLK_TCK)

On 64-bit Linux:
/usr/include/asm-x86_64/param.h:#define HZ 100

Did you try to run posixmodule.c through gcc -E on your system?

I should not play devil's advocate and argue against my own patch, but 
there are two issues:

1. If a system provides non-standard HZ, is it to be preferred to 
sysconf(..)?  Are there systems with correct HZ but no sysconf?

2. Is the added complexity of #ifdef dance justified for the performance 
improvements on some platforms?  I know it looks like I am flip-flopping 
here, but I just don't want to change anything on the platforms where 
os.times is not broken and use a solution that is know to work on some 
platforms to fix the bug where it shows up.