save_host_regs
+ restore_vgic_state
+
@ Store hardware CP15 state and load guest state
read_cp15_state store_to_vcpu = 0
write_cp15_state read_from_vcpu = 1
read_cp15_state store_to_vcpu = 1
write_cp15_state read_from_vcpu = 0
+ save_vgic_state
+
restore_host_regs
clrex @ Clear exclusive monitor
mov r0, r1 @ Return the return code