I'm reposting my own summarizing response at the official forum.
I've dived more deeply into the BCM2836 document today https://www.raspberrypi.org/documentation/hardware/raspberrypi/bcm2836/QA7_rev3.4.pdf. There is a crystal oscillator running at 19.2 MHz on the board. It can be the source of the ARM clocks. Another clock, the peripheral bus clock (APB), which is running at half of the CPU frequency, can also be the source of the timers. The latter is not recommended because the CPU frequency is variable, but I have not tested if GPU would adjust the divider when it changes the CPU's frequency to keep the clock rate constant. Despite that, the source of the clock can be configured by setting bit 8 of the register mapped to physical address 0x40000000.
The value of the timer's divider can also be set by writing 0x40000008. However, the default value set by the firmware is 0x06AAAAAB, which divided by 2^31 is 19. Therefore, effectively, in bare metal environment, the ARM timers are running at 1 MHz, not 19.2 MHz indicated by dmesg. I doubt Linux at some point sets the divider to 1 to get higher precision, but I've not verified that.
Also, I notice in that document, there is a formula calculating the timer's frequency.
timer_frequency = (2^31/prescaler) * input frequency (Pre-scaler <= 231)
Sadly, it's misleading, as the divider should divide the input frequency instead of multiplying.