88 	uint32_t first_mid, first_low;  in read_elapsedtime_counter()  local
92 		first_low = (uint32_t)read_rtc1(ETIMELREG);  in read_elapsedtime_counter()
98 	} while (first_low != second_low || first_mid != second_mid ||  in read_elapsedtime_counter()
101 	return (first << 32) | (uint64_t)((first_mid << 16) | first_low);  in read_elapsedtime_counter()
126 	uint32_t first_high, first_low;  in vr41xx_read_rtclong1_counter()  local
130 		first_low = (uint32_t)read_rtc1(RTCL1CNTLREG);  in vr41xx_read_rtclong1_counter()
134 	} while (first_low != second_low || first_high != second_high);  in vr41xx_read_rtclong1_counter()
136 	return (first_high << 16) | first_low;  in vr41xx_read_rtclong1_counter()
147 	uint32_t first_high, first_low;  in vr41xx_read_rtclong2_counter()  local
151 		first_low = (uint32_t)read_rtc1(RTCL2CNTLREG);  in vr41xx_read_rtclong2_counter()
155 	} while (first_low != second_low || first_high != second_high);  in vr41xx_read_rtclong2_counter()
157 	return (first_high << 16) | first_low;  in vr41xx_read_rtclong2_counter()
168 	uint32_t first_high, first_low;  in vr41xx_read_tclock_counter()  local
172 		first_low = (uint32_t)read_rtc2(TCLKCNTLREG);  in vr41xx_read_tclock_counter()
176 	} while (first_low != second_low || first_high != second_high);  in vr41xx_read_tclock_counter()
178 	return (first_high << 16) | first_low;  in vr41xx_read_tclock_counter()