Choosing the timer to use in benchmarking