1/* SPDX-License-Identifier: GPL-2.0 */
 2#ifndef _S390_VTIME_H
 3#define _S390_VTIME_H
 4
 5#define __ARCH_HAS_VTIME_TASK_SWITCH
 6
 7static inline void update_timer_sys(void)
 8{
 9	S390_lowcore.system_timer += S390_lowcore.last_update_timer - S390_lowcore.exit_timer;
10	S390_lowcore.user_timer += S390_lowcore.exit_timer - S390_lowcore.sys_enter_timer;
11	S390_lowcore.last_update_timer = S390_lowcore.sys_enter_timer;
12}
13
14static inline void update_timer_mcck(void)
15{
16	S390_lowcore.system_timer += S390_lowcore.last_update_timer - S390_lowcore.exit_timer;
17	S390_lowcore.user_timer += S390_lowcore.exit_timer - S390_lowcore.mcck_enter_timer;
18	S390_lowcore.last_update_timer = S390_lowcore.mcck_enter_timer;
19}
20
21#endif /* _S390_VTIME_H */