diff --git a/proto/hypervisor.c b/proto/hypervisor.c
index 1070b1f9c7ec10c5c3858c76c8d01eef6249b925..502545d218cd7ae38bb479e032d8e8720a560ab5 100644
--- a/proto/hypervisor.c
+++ b/proto/hypervisor.c
@@ -3,6 +3,7 @@
 #include <asm/page.h>
 #include <asm/page_types.h>
 #include <asm/paravirt.h>
+#include <linux/errno.h>
 #include <linux/gfp_types.h>
 #include <linux/init.h> /* Needed for the macros */
 #include <linux/kern_levels.h>
@@ -11,7 +12,9 @@
 #include <linux/slab.h>
 
 /*============== my includes ==============*/
+#include "asm/smp.h"
 #include "asm/special_insns.h"
+#include "asm/tlbflush.h"
 #include "debug/debug.h"
 #include "msr/msr.h"
 #include "region/vxmon_reg.h"
@@ -26,15 +29,22 @@
 
 static struct vmxon_region_t vmxon_region;
 
-static void cr4_enable_vmx(void) {
+static int cr4_enable_vmx(void) {
     unsigned long cr4;
 
+    /*BUG: Need to somehow switch to a CPU whose VMXE bit hasn't be modified*/
+    if ((__read_cr4() >> 13) & 1) {
+        return -EBUSY;
+    }
+
     __asm__ volatile("mov %%cr4, %0" : "=r"(cr4));
     cr4 |= (1UL << 13);
     __asm__ volatile("mov %0, %%cr4" ::"r"(cr4));
 
     DEBUG_FMT("CR4[13].VMXE set? %s\n",
               (__read_cr4() >> 13) & 1 ? "true" : "false");
+
+    return 0;
 }
 
 static bool vmx_support_cpuid(void) {
@@ -102,15 +112,16 @@ static int my_init(void) {
     pr_info("Checking VMX support using CPUID\n");
     if (!vmx_support_cpuid()) {
         pr_err("VMX isn't supported\n");
-        return -1;
+        return -EPERM;
     }
 
     DEBUG_FMT("IA32_VMX_BASIC_MSR = 0x%llx\n", __rdmsr(IA32_VMX_BASIC));
 
     pr_info("Initializing VMXON region\n");
-    if (init_vmxon_reg(&vmxon_region) != 0) {
+    int ret_init_vmxon;
+    if ((ret_init_vmxon = init_vmxon_reg(&vmxon_region)) != 0) {
         pr_err("Failed to initialized the VMXON region\n");
-        return -1;
+        return -ret_init_vmxon;
     }
 
     pr_info("VA of the allocated region = 0x%px\n", vmxon_region.va);
@@ -124,13 +135,18 @@ static int my_init(void) {
     patch_control_registers();
 
     pr_info("Enabling VMX in CR4\n");
-    cr4_enable_vmx();
+    int ret_cr4_vmx;
+
+    if ((ret_cr4_vmx = cr4_enable_vmx()) != 0) {
+        pr_err("CPU not available, VMXE bit in CR4 has already been set\n");
+        return ret_cr4_vmx;
+    }
 
     pr_info("Checking the necessary flags of the IA32_FEATURE_CONTROL_MSR\n");
     if (!ia32_feature_control_flags()) {
         pr_err("The flags of the IA32_FEATURE_CONTROL MSR do not permit "
                "virtualization\n");
-        return -1;
+        return -EPERM;
     }
 
     pr_info("Executing VMXON with address = 0x%llx as its operand\n",
@@ -141,6 +157,7 @@ static int my_init(void) {
     if ((vmxon_ret = vmxon(vmxon_region.pa) != 0)) {
         /*unsigned long vm_err = __rdmsr(0x4400);*/
         /*pr_err("VM_ERR val = 0x%lx\n", vm_err);*/
+        cr4_clear_bits(13);
 
         kfree(vmxon_region.va);
         __asm__ volatile("vmxoff");
diff --git a/proto/region/vmxon_reg.c b/proto/region/vmxon_reg.c
index 1f568ac47505d2a4be58018c9b5fd60eae3e6215..e4ade30d1cca337b52042320773380305d7237ac 100644
--- a/proto/region/vmxon_reg.c
+++ b/proto/region/vmxon_reg.c
@@ -2,25 +2,26 @@
 #include "../msr/msr.h"
 #include "vxmon_reg.h"
 #include <asm/page.h>
+#include <linux/errno.h>
 #include <linux/printk.h>
 #include <linux/slab.h>
 
 static int alloc_vmxon_internals(struct vmxon_region_t *reg) {
     if (!reg) {
         DEBUG_FMT("vmxon_reg_t isn't allocated\n");
-        return -1;
+        return -EFAULT;
     }
 
     void *region = kzalloc(PAGE_SIZE, GFP_KERNEL);
 
     if (!region) {
         DEBUG_FMT("VMXON region allocation has failed\n");
-        return -1;
+        return -EFAULT;
     }
 
     if (((unsigned long long)region & 0xfff) != 0) {
         DEBUG_FMT("Region 0x%px isn't properly aligned\n", region);
-        return -1;
+        return -EFAULT;
     }
 
     DEBUG_FMT(
@@ -37,7 +38,7 @@ static int alloc_vmxon_internals(struct vmxon_region_t *reg) {
 static int write_vmcs_rev_id_to_vmxon(struct vmxon_region_t *reg) {
     if (!reg) {
         DEBUG_FMT("vmxon_reg_t isn't allocated\n");
-        return -1;
+        return -EFAULT;
     }
 
     DEBUG_FMT(
@@ -53,13 +54,15 @@ static int write_vmcs_rev_id_to_vmxon(struct vmxon_region_t *reg) {
 }
 
 int init_vmxon_reg(struct vmxon_region_t *reg) {
-    if (alloc_vmxon_internals(reg) != 0) {
-        return -1;
+    int ret;
+
+    if ((ret = alloc_vmxon_internals(reg)) != 0) {
+        return ret;
     }
 
-    if (write_vmcs_rev_id_to_vmxon(reg) != 0) {
+    if ((ret = write_vmcs_rev_id_to_vmxon(reg)) != 0) {
         kfree(reg->va);
-        return -1;
+        return ret;
     }
 
     return 0;