X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=palacios%2Finclude%2Fpalacios%2Fvmm_time.h;h=33ffa2c0fc06996505798a20324c0b4285fe5feb;hb=0e26b3738daf436ba2d9a088ba620a3583d40de3;hp=3255acaee6495c8084973d100b5fcbbd05d7249d;hpb=e02cc15e36e8f5d7ee66390986351748dd9a16a1;p=palacios.git

diff --git a/palacios/include/palacios/vmm_time.h b/palacios/include/palacios/vmm_time.h
index 3255aca..33ffa2c 100644
--- a/palacios/include/palacios/vmm_time.h
+++ b/palacios/include/palacios/vmm_time.h
@@ -91,21 +91,26 @@ static inline uint64_t v3_get_host_time(struct vm_time *t) {
 }
 
 // Returns *monotonic* guest time.
-static inline uint64_t v3_get_guest_time(struct vm_time *t) {
-#ifdef CONFIG_TIME_HIDE_VM_COST
-    if (t->exit_time) {
-        return t->exit_time + t->guest_host_offset;
-    } else {
-        return v3_get_host_time(t) + t->guest_host_offset;
-    }
+static inline uint64_t v3_compute_guest_time(struct vm_time *t, uint64_t ht) {
+#ifdef V3_CONFIG_TIME_HIDE_VM_COST
+    V3_ASSERT(t->exit_time);
+    return t->exit_time + t->guest_host_offset;
 #else
     return v3_get_host_time(t) + t->guest_host_offset;
 #endif
 }
 
+static inline uint64_t v3_get_guest_time(struct vm_time *t) {
+    return v3_compute_guest_time(t, v3_get_host_time(t));
+}
+
 // Returns the TSC value seen by the guest
+static inline uint64_t v3_compute_guest_tsc(struct vm_time *t, uint64_t ht) {
+    return v3_compute_guest_time(t, ht) + t->tsc_guest_offset;
+}
+
 static inline uint64_t v3_get_guest_tsc(struct vm_time *t) {
-    return v3_get_guest_time(t) + t->tsc_guest_offset;
+    return v3_compute_guest_tsc(t, v3_get_host_time(t));
 }
 
 // Returns offset of guest TSC from host TSC