diff --git a/docs/re.md b/docs/re.md
index 73ffeaa3c4cb868254767476752dde5a69aaea04..09e54e7b4113c8e9d48bd2f68c369efef5f9375a 100644
--- a/docs/re.md
+++ b/docs/re.md
@@ -95,6 +95,11 @@ static bool vmx_supported(void) {
 
 ### Enabling VMX in CR4
 
+> [!IMPORTANT]
+> Looks like, when virtualization has been activated through the BIOS, the 13th
+> bit of CR4 is **always** set. Thus, setting this bit manually seems to be a
+> no-op.
+
 In order to enter VMX operation, the software (our hypervisor) has to firstly
 enable VMX by setting the 13th bit of the CR4 register to 1. This will of course
 throw an exception if this code is being executed from user-space. That's why
diff --git a/proto/.clang-format b/proto/.clang-format
new file mode 100644
index 0000000000000000000000000000000000000000..6590de88c72f3208d4cb7f144fde7cfb49ea608d
--- /dev/null
+++ b/proto/.clang-format
@@ -0,0 +1,5 @@
+---
+BasedOnStyle: LLVM
+IndentWidth: 4
+ColumnLimit: 80
+...
diff --git a/proto/Makefile b/proto/Makefile
index 0a72d0c291adab958b9164602112c76b4cc9fd38..9d291ed8bb0b30eb1a88ec78acf174bb12e904e5 100644
--- a/proto/Makefile
+++ b/proto/Makefile
@@ -1,6 +1,6 @@
 # https://sysprog21.github.io/lkmpg/
 obj-m += vmbr.o
-vmbr-objs := hypervisor.o ./msr/msr.o ./region/vmxon_reg.o
+vmbr-objs := hypervisor.o ./msr/msr.o ./region/vmxon.o ./vcpu/vcpu.o
 
 PWD := $(CURDIR) 
 
diff --git a/proto/hypervisor.c b/proto/hypervisor.c
index 1070b1f9c7ec10c5c3858c76c8d01eef6249b925..6423599fd70fa67b9576dd7896ac90f0122ae724 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,10 +12,14 @@
 #include <linux/slab.h>
 
 /*============== my includes ==============*/
+#include "asm/smp.h"
 #include "asm/special_insns.h"
+#include "asm/tlbflush.h"
 #include "debug/debug.h"
+#include "linux/threads.h"
 #include "msr/msr.h"
-#include "region/vxmon_reg.h"
+#include "region/vxmon.h"
+#include "vcpu/vcpu.h"
 
 #define NULL ((void *)0)
 
@@ -24,17 +29,25 @@
 /*    : clobbered registers list          (optional)*/
 /*    );*/
 
-static struct vmxon_region_t vmxon_region;
+static struct vcpu_t vcpus[1];
 
-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*/
+    /*NOTE: seems like this bit is always set on every processor, weird..*/
+    /*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) {
@@ -72,7 +85,7 @@ static unsigned char vmxon(unsigned long long pa) {
 
     /*asm goto("1: vmxon %[vmxon_pointer]\n\t" _ASM_EXTABLE(1b, % l[fault])*/
     /*         :*/
-    /*         : [vmxon_pointer] "m"(vmxon_pointer)*/
+    /*         : [vmxon_pointer] "m"(pa)*/
     /*         :*/
     /*         : fault);*/
 
@@ -82,6 +95,65 @@ static unsigned char vmxon(unsigned long long pa) {
     DEBUG_FMT("RFLAGS: 0x%llx\n", rflags);
 
     return ret;
+
+    /*    unsigned long long msr;*/
+    /**/
+    /*    cr4_set_bits(X86_CR4_VMXE);*/
+    /**/
+    /*    __asm__ goto("1: vmxon %[vmxon_pointer]\n\t" _ASM_EXTABLE(1b,
+     * %l[fault])*/
+    /*                 :*/
+    /*                 : [vmxon_pointer] "m"(vmxon_pointer)*/
+    /*                 :*/
+    /*                 : fault);*/
+    /*    return 0;*/
+    /**/
+    /*fault:*/
+    /*    WARN_ONCE(1, "VMXON faulted, MSR_IA32_FEAT_CTL (0x3a) = 0x%llx\n",*/
+    /*              rdmsrl_safe(MSR_IA32_FEAT_CTL, &msr) ? 0xdeadbeef : msr);*/
+    /*    cr4_clear_bits(X86_CR4_VMXE);*/
+    /**/
+    /*    return -EFAULT;*/
+}
+
+/*NOTE: arch/x86/kvm/vmx/vmx.c:2824 v6.12.10*/
+static int kvm_cpu_vmxon(unsigned long long vmxon_pointer) {
+    unsigned long long msr;
+
+    cr4_set_bits(X86_CR4_VMXE);
+
+    // clang-format off
+    asm goto("1: vmxon %[vmxon_pointer]\n\t" _ASM_EXTABLE(1b, %l[fault])
+             :
+             : [vmxon_pointer] "m"(vmxon_pointer)
+             :
+             : fault);
+
+    // clang-format on
+    return 0;
+
+fault:
+    WARN_ONCE(1, "VMXON faulted, MSR_IA32_FEAT_CTL (0x3a) = 0x%llx\n",
+              rdmsrl_safe(MSR_IA32_FEAT_CTL, &msr) ? 0xdeadbeef : msr);
+    cr4_clear_bits(X86_CR4_VMXE);
+
+    return -EFAULT;
+}
+
+/*NOTE: arch/x86/kvm/vmx/vmx.c:742 v6.12.10*/
+static int kvm_cpu_vmxoff(void) {
+    // clang-format off
+    asm goto("1: vmxoff\n\t" _ASM_EXTABLE(1b, %l[fault])::
+                 : "cc", "memory"
+             : fault);
+
+    // clang-format on
+    cr4_clear_bits(X86_CR4_VMXE);
+    return 0;
+
+fault:
+    cr4_clear_bits(X86_CR4_VMXE);
+    return -EIO;
 }
 
 static int my_init(void) {
@@ -102,48 +174,63 @@ 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) {
-        pr_err("Failed to initialized the VMXON region\n");
-        return -1;
+    pr_info("Allocating VMXON region\n");
+
+    struct vmxon_t *vmxon_reg = alloc_vmxon();
+
+    if (!vmxon_reg) {
+        pr_err("VMXON region allocation failed\n");
+        return -ENOMEM;
     }
 
-    pr_info("VA of the allocated region = 0x%px\n", vmxon_region.va);
-    pr_info("PA of the allocated region = 0x%llx\n", vmxon_region.pa);
+    if (init_vcpu(&vcpus[0], vmxon_reg) != 0) {
+        pr_err("VCPU initialization failed\n");
+        return -EFAULT;
+    }
+
+    pr_info("VA of the allocated region = 0x%px\n", vmxon_reg);
+    pr_info("PA of the allocated region = 0x%lx\n", __pa(vmxon_reg));
 
-    pr_info("Reading VMXON region for VMCS ID: 0x%lx\n",
-            (*(unsigned long *)vmxon_region.va));
+    pr_info("Reading VMXON region for VMCS ID: 0x%x\n",
+            vmxon_reg->header.vmcs_rev_id);
 
     pr_info("Patching CR0 and CR4 depending on the value of their respective "
             "MSRs\n");
     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",
-            vmxon_region.pa);
+    pr_info("Executing VMXON with address = 0x%lx as its operand\n",
+            __pa(vmxon_reg));
 
     unsigned char vmxon_ret = 0;
 
-    if ((vmxon_ret = vmxon(vmxon_region.pa) != 0)) {
+    /*if ((vmxon_ret = vmxon(vmxon_region.pa) != 0)) {*/
+    if ((vmxon_ret = kvm_cpu_vmxon(__pa(vmxon_reg)) != 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");
+        kfree(vmxon_reg);
+        /*__asm__ volatile("vmxoff");*/
         pr_err("`vmxon` failed with return code %d\n", vmxon_ret);
         return -1;
     }
@@ -155,10 +242,16 @@ static int my_init(void) {
 
 static void my_exit(void) {
     pr_info("Executing VMXOFF\n");
-    __asm__ volatile("vmxoff");
+    /*__asm__ volatile("vmxoff");*/
+    int vmxoff;
+
+    if ((vmxoff = kvm_cpu_vmxoff()) != 0) {
+        pr_err("Failed to execute VMXOFF\n");
+        return;
+    }
 
     pr_info("Freeing memory of the VMXON region\n");
-    kfree(vmxon_region.va);
+    kfree(vcpus[0].vmxon);
 
     pr_info("vmbr.ko has exited\n");
 }
diff --git a/proto/region/vmxon.c b/proto/region/vmxon.c
new file mode 100644
index 0000000000000000000000000000000000000000..d4cd85f53d28bea45ef9bc207210527e9a7ba6ad
--- /dev/null
+++ b/proto/region/vmxon.c
@@ -0,0 +1,21 @@
+#include "../debug/debug.h"
+#include "../msr/msr.h"
+#include "vxmon.h"
+#include <asm/page.h>
+#include <linux/errno.h>
+#include <linux/printk.h>
+#include <linux/slab.h>
+
+struct vmxon_t *alloc_vmxon(void) {
+    struct vmxon_t *vmxon = kzalloc(sizeof(struct vmxon_t), GFP_KERNEL);
+
+    if (!vmxon) {
+        DEBUG_FMT("VMXON region allocation has failed\n");
+        return NULL;
+    }
+
+    vmxon->header.vmcs_rev_id = VMCS_REVISION_ID;
+    vmxon->header.shadow_vmcs = 0;
+
+    return vmxon;
+}
diff --git a/proto/region/vmxon_reg.c b/proto/region/vmxon_reg.c
deleted file mode 100644
index 1f568ac47505d2a4be58018c9b5fd60eae3e6215..0000000000000000000000000000000000000000
--- a/proto/region/vmxon_reg.c
+++ /dev/null
@@ -1,66 +0,0 @@
-#include "../debug/debug.h"
-#include "../msr/msr.h"
-#include "vxmon_reg.h"
-#include <asm/page.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;
-    }
-
-    void *region = kzalloc(PAGE_SIZE, GFP_KERNEL);
-
-    if (!region) {
-        DEBUG_FMT("VMXON region allocation has failed\n");
-        return -1;
-    }
-
-    if (((unsigned long long)region & 0xfff) != 0) {
-        DEBUG_FMT("Region 0x%px isn't properly aligned\n", region);
-        return -1;
-    }
-
-    DEBUG_FMT(
-        "Reading IA32_VMX_BASIC MSR for allocation size (in bytes) = %llu \n",
-        REGION_SIZE);
-
-    reg->size = REGION_SIZE;
-    reg->va = region;
-    reg->pa = __pa(region);
-
-    return 0;
-}
-
-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;
-    }
-
-    DEBUG_FMT(
-        "Reading IA32_VMX_BASIC MSR for VMCS revision identifier = 0x%llx\n",
-        VMCS_REVISION_ID);
-
-    DEBUG_FMT("Writing VMCS Revision ID to VMXON region\n");
-
-    (*(unsigned long *)reg->va) = VMCS_REVISION_ID;
-    (*(unsigned long *)reg->va) &= ~(1UL << 31);
-
-    return 0;
-}
-
-int init_vmxon_reg(struct vmxon_region_t *reg) {
-    if (alloc_vmxon_internals(reg) != 0) {
-        return -1;
-    }
-
-    if (write_vmcs_rev_id_to_vmxon(reg) != 0) {
-        kfree(reg->va);
-        return -1;
-    }
-
-    return 0;
-}
diff --git a/proto/region/vxmon.h b/proto/region/vxmon.h
new file mode 100644
index 0000000000000000000000000000000000000000..c75c5d440fb1a56ece367638a5a8cd72a269c1f0
--- /dev/null
+++ b/proto/region/vxmon.h
@@ -0,0 +1,11 @@
+#pragma once
+
+struct vmxon_t {
+    struct {
+        unsigned long vmcs_rev_id : 31;
+        unsigned long shadow_vmcs : 1;
+    } header;
+    char state[0x1000 - sizeof(unsigned long)];
+};
+
+struct vmxon_t *alloc_vmxon(void);
diff --git a/proto/region/vxmon_reg.h b/proto/region/vxmon_reg.h
deleted file mode 100644
index e080b028ea6c1584f929382b353e8e3d12e85e62..0000000000000000000000000000000000000000
--- a/proto/region/vxmon_reg.h
+++ /dev/null
@@ -1,9 +0,0 @@
-#pragma once
-
-struct vmxon_region_t {
-    unsigned long size;
-    void *va;
-    unsigned long long pa;
-};
-
-int init_vmxon_reg(struct vmxon_region_t *reg);
diff --git a/proto/vcpu/vcpu.c b/proto/vcpu/vcpu.c
new file mode 100644
index 0000000000000000000000000000000000000000..8f367a4b47af25d51c5b07958fbdce3a5314d82d
--- /dev/null
+++ b/proto/vcpu/vcpu.c
@@ -0,0 +1,21 @@
+#include "vcpu.h"
+#include "../debug/debug.h"
+#include "../region/vxmon.h"
+#include "linux/string.h"
+#include <linux/errno.h>
+
+int init_vcpu(struct vcpu_t *vcpu, struct vmxon_t *vmxon) {
+    if (!vcpu) {
+        DEBUG_FMT("vcpu isn't allocated\n");
+        return -EFAULT;
+    }
+
+    if (!vmxon) {
+        DEBUG_FMT("vmxon region isn't allocated\n");
+        return -EFAULT;
+    }
+
+    vcpu->vmxon = vmxon;
+
+    return 0;
+}
diff --git a/proto/vcpu/vcpu.h b/proto/vcpu/vcpu.h
new file mode 100644
index 0000000000000000000000000000000000000000..a61e34dc079cf8e14cec14bc9c7f745120f20bf0
--- /dev/null
+++ b/proto/vcpu/vcpu.h
@@ -0,0 +1,12 @@
+#pragma once
+
+#include "../region/vxmon.h"
+
+struct vcpu_t {
+    struct vmxon_t *vmxon;
+    /*NOTE: prolly should store the PAs of pointers to avoid unnecessary
+     * address translations, although they should reside in the TLB by that
+     * point*/
+};
+
+int init_vcpu(struct vcpu_t *vcpu, struct vmxon_t *vmxon);