Merge branch 'devel' of ssh://palacios@newskysaw.cs.northwestern.edu/home/palacios...

diff --cc palacios/src/palacios/svm.c
Simple merge

diff --cc palacios/src/palacios/vmx.c
index 1a23de7,106239f..f26a1ea
--- 1/palacios/src/palacios/vmx.c
--- 2/palacios/src/palacios/vmx.c
+++ b/palacios/src/palacios/vmx.c
@@@ -748,16 -749,15 +749,15 @@@ int v3_vmx_enter(struct guest_info * in
      // disable global interrupts for vm state transition
      v3_disable_ints();
  
 +    // Update timer devices prior to entering VM.  Doing it here 
 +    // makes sure the guest sees any timers that fired while it 
 +    // was in the VMM
 +    v3_update_timers(info);
  
-     if (active_vmcs_ptrs[V3_Get_CPU()] != vmx_info->vmcs_ptr_phys) {
+     if (vmcs_store() != vmx_info->vmcs_ptr_phys) {
        vmcs_load(vmx_info->vmcs_ptr_phys);
-       active_vmcs_ptrs[V3_Get_CPU()] = vmx_info->vmcs_ptr_phys;
      }
  
 -
      v3_vmx_restore_vmcs(info);