Re: Choosing the timer to use in benchmarking