diff --git a/hypervisor/arch/x86/Kconfig b/hypervisor/arch/x86/Kconfig
index 4dd2782fa..53c30f09d 100644
--- a/hypervisor/arch/x86/Kconfig
+++ b/hypervisor/arch/x86/Kconfig
@@ -34,6 +34,12 @@ config RELEASE
 
 config MAX_VM_NUM
 	int "Maximum number of VM"
+	range 1 8
+	default 4
+
+config MAX_VCPUS_PER_VM
+	int "Maximum number of VCPUS per VM"
+	range 1 8
 	default 4
 
 config NR_IOAPICS
diff --git a/hypervisor/arch/x86/guest/guest.c b/hypervisor/arch/x86/guest/guest.c
index be4835cf9..95bb77aeb 100644
--- a/hypervisor/arch/x86/guest/guest.c
+++ b/hypervisor/arch/x86/guest/guest.c
@@ -42,7 +42,6 @@ uint64_t vcpumask2pcpumask(struct vm *vm, uint64_t vdmask)
 		vcpu_id = ffs64(vdmask)) {
 		bitmap_clear_lock(vcpu_id, &vdmask);
 		vcpu = vcpu_from_vid(vm, vcpu_id);
-		ASSERT(vcpu != NULL, "vcpu_from_vid failed");
 		bitmap_set_lock(vcpu->pcpu_id, &dmask);
 	}
 
@@ -383,6 +382,9 @@ static inline int copy_gpa(struct vm *vm, void *h_ptr_arg, uint64_t gpa_arg,
 	return 0;
 }
 
+/*
+ * @pre vcpu != NULL && err_code != NULL
+ */
 static inline int copy_gva(struct vcpu *vcpu, void *h_ptr_arg, uint64_t gva_arg,
 	uint32_t size_arg, uint32_t *err_code, uint64_t *fault_addr,
 	bool cp_from_vm)
@@ -394,15 +396,6 @@ static inline int copy_gva(struct vcpu *vcpu, void *h_ptr_arg, uint64_t gva_arg,
 	uint64_t gva = gva_arg;
 	uint32_t size = size_arg;
 
-	if (vcpu == NULL) {
-		pr_err("guest virt addr copy need vcpu param");
-		return -EINVAL;
-	}
-	if (err_code == NULL) {
-		pr_err("guest virt addr copy need err_code param");
-		return -EINVAL;
-	}
-
 	while (size > 0U) {
 		ret = gva2gpa(vcpu, gva, &gpa, err_code);
 		if (ret < 0) {
diff --git a/hypervisor/arch/x86/guest/vcpu.c b/hypervisor/arch/x86/guest/vcpu.c
index c880c74de..476c02eff 100644
--- a/hypervisor/arch/x86/guest/vcpu.c
+++ b/hypervisor/arch/x86/guest/vcpu.c
@@ -311,15 +311,25 @@ void set_ap_entry(struct vcpu *vcpu, uint64_t entry)
 int create_vcpu(uint16_t pcpu_id, struct vm *vm, struct vcpu **rtn_vcpu_handle)
 {
 	struct vcpu *vcpu;
-
+	uint16_t vcpu_id;
 
 	pr_info("Creating VCPU working on PCPU%hu", pcpu_id);
 
+	/*
+	 * vcpu->vcpu_id = vm->hw.created_vcpus;
+	 * vm->hw.created_vcpus++;
+	 */
+	vcpu_id = atomic_xadd16(&vm->hw.created_vcpus, 1U);
+	if (vcpu_id >= CONFIG_MAX_VCPUS_PER_VM) {
+		pr_err("%s, vcpu id is invalid!\n", __func__);
+		return -EINVAL;
+	}
 	/* Allocate memory for VCPU */
-	vcpu = calloc(1U, sizeof(struct vcpu));
-	ASSERT(vcpu != NULL, "");
+	vcpu = &(vm->hw.vcpu_array[vcpu_id]);
+	(void)memset((void *)vcpu, 0U, sizeof(struct vcpu));
 
-	/* Initialize the physical CPU ID for this VCPU */
+	/* Initialize CPU ID for this VCPU */
+	vcpu->vcpu_id = vcpu_id;
 	vcpu->pcpu_id = pcpu_id;
 	per_cpu(ever_run_vcpu, pcpu_id) = vcpu;
 
@@ -334,19 +344,6 @@ int create_vcpu(uint16_t pcpu_id, struct vm *vm, struct vcpu **rtn_vcpu_handle)
 	 * needs revise.
 	 */
 
-	/*
-	 * vcpu->vcpu_id = vm->hw.created_vcpus;
-	 * vm->hw.created_vcpus++;
-	 */
-	vcpu->vcpu_id = atomic_xadd16(&vm->hw.created_vcpus, 1U);
-	/* vm->hw.vcpu_array[vcpu->vcpu_id] = vcpu; */
-	atomic_store64(
-		(uint64_t *)&vm->hw.vcpu_array[vcpu->vcpu_id],
-		(uint64_t)vcpu);
-
-	ASSERT(vcpu->vcpu_id < vm->hw.num_vcpus,
-			"Allocated vcpu_id is out of range!");
-
 	per_cpu(vcpu, pcpu_id) = vcpu;
 
 	pr_info("PCPU%d is working as VM%d VCPU%d, Role: %s",
@@ -384,6 +381,9 @@ int create_vcpu(uint16_t pcpu_id, struct vm *vm, struct vcpu **rtn_vcpu_handle)
 	return 0;
 }
 
+/*
+ *  @pre vcpu != NULL
+ */
 int run_vcpu(struct vcpu *vcpu)
 {
 	uint32_t instlen, cs_attr;
@@ -392,8 +392,6 @@ int run_vcpu(struct vcpu *vcpu)
 		&vcpu->arch_vcpu.contexts[vcpu->arch_vcpu.cur_context].run_ctx;
 	int64_t status = 0;
 
-	ASSERT(vcpu != NULL, "Incorrect arguments");
-
 	if (bitmap_test_and_clear_lock(CPU_REG_RIP, &vcpu->reg_updated))
 		exec_vmwrite(VMX_GUEST_RIP, ctx->rip);
 	if (bitmap_test_and_clear_lock(CPU_REG_RSP, &vcpu->reg_updated))
@@ -486,21 +484,15 @@ int shutdown_vcpu(__unused struct vcpu *vcpu)
 	return 0;
 }
 
-void destroy_vcpu(struct vcpu *vcpu)
+/*
+ *  @pre vcpu != NULL
+ */
+void offline_vcpu(struct vcpu *vcpu)
 {
-	ASSERT(vcpu != NULL, "Incorrect arguments");
-
-	/* vcpu->vm->hw.vcpu_array[vcpu->vcpu_id] = NULL; */
-	atomic_store64(
-		(uint64_t *)&vcpu->vm->hw.vcpu_array[vcpu->vcpu_id],
-		(uint64_t)NULL);
-
-	atomic_dec16(&vcpu->vm->hw.created_vcpus);
-
 	vlapic_free(vcpu);
 	per_cpu(ever_run_vcpu, vcpu->pcpu_id) = NULL;
 	free_pcpu(vcpu->pcpu_id);
-	free(vcpu);
+	vcpu->state = VCPU_OFFLINE;
 }
 
 /* NOTE:
@@ -602,7 +594,9 @@ int prepare_vcpu(struct vm *vm, uint16_t pcpu_id)
 	struct vcpu *vcpu = NULL;
 
 	ret = create_vcpu(pcpu_id, vm, &vcpu);
-	ASSERT(ret == 0, "vcpu create failed");
+	if (ret != 0) {
+		return ret;
+	}
 
 	if (!vm_sw_loader) {
 		vm_sw_loader = general_sw_loader;
diff --git a/hypervisor/arch/x86/guest/vlapic.c b/hypervisor/arch/x86/guest/vlapic.c
index 18a80cb13..60051979e 100644
--- a/hypervisor/arch/x86/guest/vlapic.c
+++ b/hypervisor/arch/x86/guest/vlapic.c
@@ -108,7 +108,6 @@ vm_lapic_from_vcpu_id(struct vm *vm, uint16_t vcpu_id)
 	struct vcpu *vcpu;
 
 	vcpu = vcpu_from_vid(vm, vcpu_id);
-	ASSERT(vcpu != NULL, "vm%d, vcpu%hu", vm->vm_id, vcpu_id);
 
 	return vcpu_vlapic(vcpu);
 }
@@ -119,7 +118,6 @@ vm_lapic_from_pcpuid(struct vm *vm, uint16_t pcpu_id)
 	struct vcpu *vcpu;
 
 	vcpu = vcpu_from_pid(vm, pcpu_id);
-	ASSERT(vcpu != NULL, "vm%d, pcpu%hu", vm->vm_id, pcpu_id);
 
 	return vcpu_vlapic(vcpu);
 }
@@ -1996,14 +1994,13 @@ int vlapic_create(struct vcpu *vcpu)
 	return 0;
 }
 
+/*
+ *  @pre vcpu != NULL
+ */
 void vlapic_free(struct vcpu *vcpu)
 {
 	struct acrn_vlapic *vlapic = NULL;
 
-	if (vcpu == NULL) {
-		return;
-	}
-
 	vlapic = vcpu_vlapic(vcpu);
 
 	del_timer(&vlapic->vtimer.timer);
diff --git a/hypervisor/arch/x86/guest/vm.c b/hypervisor/arch/x86/guest/vm.c
index 6caae6ce0..17e4b3e57 100644
--- a/hypervisor/arch/x86/guest/vm.c
+++ b/hypervisor/arch/x86/guest/vm.c
@@ -40,17 +40,6 @@ static inline bool is_vm_valid(uint16_t vm_id)
 	return bitmap_test(vm_id, &vmid_bitmap);
 }
 
-static void init_vm(struct vm_description *vm_desc,
-		struct vm *vm_handle)
-{
-	/* Populate VM attributes from VM description */
-	vm_handle->hw.num_vcpus = vm_desc->vm_hw_num_cores;
-
-#ifdef CONFIG_PARTITION_MODE
-	vm_handle->vm_desc = vm_desc;
-#endif
-}
-
 /* return a pointer to the virtual machine structure associated with
  * this VM ID
  */
@@ -87,25 +76,12 @@ int create_vm(struct vm_description *vm_desc, struct vm **rtn_vm)
 	vm = &vm_array[vm_id];
 	(void)memset((void *)vm, 0U, sizeof(struct vm));
 	vm->vm_id = vm_id;
-	/*
-	 * Map Virtual Machine to its VM Description
-	 */
-	init_vm(vm_desc, vm);
-
+#ifdef CONFIG_PARTITION_MODE
+	/* Map Virtual Machine to its VM Description */
+	vm->vm_desc = vm_desc;
+#endif
 	/* Init mmio list */
 	INIT_LIST_HEAD(&vm->mmio_list);
-
-	if (vm->hw.num_vcpus == 0U) {
-		vm->hw.num_vcpus = phys_cpu_num;
-	}
-	vm->hw.vcpu_array =
-		calloc(1U, sizeof(struct vcpu *) * vm->hw.num_vcpus);
-	if (vm->hw.vcpu_array == NULL) {
-		pr_err("%s, vcpu_array allocation failed\n", __func__);
-		status = -ENOMEM;
-		goto err;
-	}
-
 	atomic_store16(&vm->hw.created_vcpus, 0U);
 
 	/* gpa_lowtop are used for system start up */
@@ -211,9 +187,6 @@ err:
 		free(vm->arch_vm.nworld_eptp);
 	}
 
-	if (vm->hw.vcpu_array != NULL) {
-		free(vm->hw.vcpu_array);
-	}
 	return status;
 }
 
@@ -235,7 +208,7 @@ int shutdown_vm(struct vm *vm)
 
 	foreach_vcpu(i, vm, vcpu) {
 		reset_vcpu(vcpu);
-		destroy_vcpu(vcpu);
+		offline_vcpu(vcpu);
 	}
 
 	ptdev_release_all_entries(vm);
@@ -267,7 +240,6 @@ int shutdown_vm(struct vm *vm)
 #ifdef CONFIG_PARTITION_MODE
 	vpci_cleanup(vm);
 #endif
-	free(vm->hw.vcpu_array);
 
 	/* Return status to caller */
 	return status;
@@ -284,7 +256,6 @@ int start_vm(struct vm *vm)
 
 	/* Only start BSP (vid = 0) and let BSP start other APs */
 	vcpu = vcpu_from_vid(vm, 0U);
-	ASSERT(vcpu != NULL, "vm%d, vcpu0", vm->vm_id);
 	schedule_vcpu(vcpu);
 
 	return 0;
diff --git a/hypervisor/arch/x86/io.c b/hypervisor/arch/x86/io.c
index c97dd53d7..518877d8a 100644
--- a/hypervisor/arch/x86/io.c
+++ b/hypervisor/arch/x86/io.c
@@ -479,7 +479,7 @@ int register_mmio_emulation_handler(struct vm *vm,
 	int status = -EINVAL;
 	struct mem_io_node *mmio_node;
 
-	if ((vm->hw.created_vcpus > 0U) && vm->hw.vcpu_array[0]->launched) {
+	if ((vm->hw.created_vcpus > 0U) && vm->hw.vcpu_array[0].launched) {
 		ASSERT(false, "register mmio handler after vm launched");
 		return status;
 	}
diff --git a/hypervisor/arch/x86/virq.c b/hypervisor/arch/x86/virq.c
index 2f10adaf1..d1a1fabc8 100644
--- a/hypervisor/arch/x86/virq.c
+++ b/hypervisor/arch/x86/virq.c
@@ -563,6 +563,9 @@ void cancel_event_injection(struct vcpu *vcpu)
 	}
 }
 
+/*
+ * @pre vcpu != NULL
+ */
 int exception_vmexit_handler(struct vcpu *vcpu)
 {
 	uint32_t intinfo, int_err_code = 0U;
@@ -570,15 +573,6 @@ int exception_vmexit_handler(struct vcpu *vcpu)
 	uint32_t cpl;
 	int status = 0;
 
-	if (vcpu == NULL) {
-		TRACE_4I(TRACE_VMEXIT_EXCEPTION_OR_NMI, 0U, 0U, 0U, 0U);
-		status = -EINVAL;
-	}
-
-	if (status != 0) {
-		return status;
-	}
-
 	pr_dbg(" Handling guest exception");
 
 	/* Obtain VM-Exit information field pg 2912 */
diff --git a/hypervisor/arch/x86/vmx.c b/hypervisor/arch/x86/vmx.c
index dd9e6b19c..04562ded6 100644
--- a/hypervisor/arch/x86/vmx.c
+++ b/hypervisor/arch/x86/vmx.c
@@ -99,10 +99,8 @@ void exec_vmxon_instr(uint16_t pcpu_id)
 	vmxon_region_pa = hva2hpa(vmxon_region_va);
 	exec_vmxon(&vmxon_region_pa);
 
-	if (vcpu != NULL) {
-		vmcs_pa = hva2hpa(vcpu->arch_vcpu.vmcs);
-		exec_vmptrld(&vmcs_pa);
-	}
+	vmcs_pa = hva2hpa(vcpu->arch_vcpu.vmcs);
+	exec_vmptrld(&vmcs_pa);
 }
 
 void vmx_off(uint16_t pcpu_id)
@@ -111,10 +109,8 @@ void vmx_off(uint16_t pcpu_id)
 	struct vcpu *vcpu = get_ever_run_vcpu(pcpu_id);
 	uint64_t vmcs_pa;
 
-	if (vcpu != NULL) {
-		vmcs_pa = hva2hpa(vcpu->arch_vcpu.vmcs);
-		exec_vmclear((void *)&vmcs_pa);
-	}
+	vmcs_pa = hva2hpa(vcpu->arch_vcpu.vmcs);
+	exec_vmclear((void *)&vmcs_pa);
 
 	asm volatile ("vmxoff" : : : "memory");
 }
diff --git a/hypervisor/common/hypercall.c b/hypervisor/common/hypercall.c
index 7fb190a6a..2361482b1 100644
--- a/hypervisor/common/hypercall.c
+++ b/hypervisor/common/hypercall.c
@@ -43,7 +43,7 @@ int32_t hcall_sos_offline_cpu(struct vm *vm, uint64_t lapicid)
 			}
 			pause_vcpu(vcpu, VCPU_ZOMBIE);
 			reset_vcpu(vcpu);
-			destroy_vcpu(vcpu);
+			offline_vcpu(vcpu);
 		}
 	}
 
diff --git a/hypervisor/common/io_request.c b/hypervisor/common/io_request.c
index f05df9b5d..d4205030a 100644
--- a/hypervisor/common/io_request.c
+++ b/hypervisor/common/io_request.c
@@ -21,7 +21,6 @@ static void fire_vhm_interrupt(void)
 	vm0 = get_vm_from_vmid(0U);
 
 	vcpu = vcpu_from_vid(vm0, 0U);
-	ASSERT(vcpu != NULL, "vcpu_from_vid failed");
 
 	vlapic_intr_edge(vcpu, acrn_vhm_vector);
 }
@@ -56,6 +55,9 @@ static void acrn_print_request(uint16_t vcpu_id, struct vhm_request *req)
 	}
 }
 
+/*
+ * @pre vcpu != NULL && io_req != NULL
+ */
 int32_t
 acrn_insert_request_wait(struct vcpu *vcpu, struct io_request *io_req)
 {
@@ -63,8 +65,7 @@ acrn_insert_request_wait(struct vcpu *vcpu, struct io_request *io_req)
 	struct vhm_request *vhm_req;
 	uint16_t cur;
 
-	if ((vcpu == NULL) || (io_req == NULL) ||
-		(vcpu->vm->sw.io_shared_page == NULL)) {
+	if (vcpu->vm->sw.io_shared_page == NULL) {
 		return -EINVAL;
 	}
 
diff --git a/hypervisor/dm/vpic.c b/hypervisor/dm/vpic.c
index d32619943..6c0bd3aaa 100644
--- a/hypervisor/dm/vpic.c
+++ b/hypervisor/dm/vpic.c
@@ -190,8 +190,6 @@ static void vpic_notify_intr(struct acrn_vpic *vpic)
 		i8259->intr_raised = true;
 		if (vpic->vm->wire_mode == VPIC_WIRE_INTR) {
 			struct vcpu *vcpu = vcpu_from_vid(vpic->vm, 0U);
-
-			ASSERT(vcpu != NULL, "vm%d, vcpu0", vpic->vm->vm_id);
 			vcpu_inject_extint(vcpu);
 		} else {
 			vlapic_set_local_intr(vpic->vm, BROADCAST_CPU_ID, APIC_LVT_LINT0);
diff --git a/hypervisor/include/arch/x86/guest/guest.h b/hypervisor/include/arch/x86/guest/guest.h
index 54d720c2c..5efa0cb1a 100644
--- a/hypervisor/include/arch/x86/guest/guest.h
+++ b/hypervisor/include/arch/x86/guest/guest.h
@@ -18,11 +18,11 @@
 
 #include <mmu.h>
 
-#define foreach_vcpu(idx, vm, vcpu)					\
-	for ((idx) = 0U, vcpu = vm->hw.vcpu_array[(idx)];		\
-		(idx) < vm->hw.num_vcpus;				\
-		(idx)++, vcpu = vm->hw.vcpu_array[(idx)])		\
-		if (vcpu != NULL)
+#define foreach_vcpu(idx, vm, vcpu)				\
+	for ((idx) = 0U, vcpu = &(vm->hw.vcpu_array[(idx)]);	\
+		(idx) < vm->hw.created_vcpus;			\
+		(idx)++, vcpu = &(vm->hw.vcpu_array[(idx)])) \
+		if (vcpu->state != VCPU_OFFLINE)
 
 /* the index is matched with emulated msrs array*/
 #define IDX_TSC_DEADLINE		0U
diff --git a/hypervisor/include/arch/x86/guest/vcpu.h b/hypervisor/include/arch/x86/guest/vcpu.h
index a3bee0f54..0629e56a4 100644
--- a/hypervisor/include/arch/x86/guest/vcpu.h
+++ b/hypervisor/include/arch/x86/guest/vcpu.h
@@ -53,6 +53,7 @@ enum vcpu_state {
 	VCPU_RUNNING,
 	VCPU_PAUSED,
 	VCPU_ZOMBIE,
+	VCPU_OFFLINE,
 	VCPU_UNKNOWN_STATE,
 };
 
@@ -304,9 +305,15 @@ static inline bool is_pae(struct vcpu *vcpu)
 
 struct vcpu* get_ever_run_vcpu(uint16_t pcpu_id);
 int create_vcpu(uint16_t pcpu_id, struct vm *vm, struct vcpu **rtn_vcpu_handle);
+/*
+ *  @pre vcpu != NULL
+ */
 int run_vcpu(struct vcpu *vcpu);
 int shutdown_vcpu(struct vcpu *vcpu);
-void destroy_vcpu(struct vcpu *vcpu);
+/*
+ *  @pre vcpu != NULL
+ */
+void offline_vcpu(struct vcpu *vcpu);
 
 void reset_vcpu(struct vcpu *vcpu);
 void pause_vcpu(struct vcpu *vcpu, enum vcpu_state new_state);
diff --git a/hypervisor/include/arch/x86/guest/vlapic.h b/hypervisor/include/arch/x86/guest/vlapic.h
index 3b609d250..b861b2904 100644
--- a/hypervisor/include/arch/x86/guest/vlapic.h
+++ b/hypervisor/include/arch/x86/guest/vlapic.h
@@ -173,6 +173,9 @@ void vlapic_apicv_batch_set_tmr(struct acrn_vlapic *vlapic);
 uint32_t vlapic_get_id(struct acrn_vlapic *vlapic);
 uint8_t vlapic_get_apicid(struct acrn_vlapic *vlapic);
 int vlapic_create(struct vcpu *vcpu);
+/*
+ *  @pre vcpu != NULL
+ */
 void vlapic_free(struct vcpu *vcpu);
 void vlapic_init(struct acrn_vlapic *vlapic);
 void vlapic_reset(struct acrn_vlapic *vlapic);
diff --git a/hypervisor/include/arch/x86/guest/vm.h b/hypervisor/include/arch/x86/guest/vm.h
index 0764d86bd..aa1114177 100644
--- a/hypervisor/include/arch/x86/guest/vm.h
+++ b/hypervisor/include/arch/x86/guest/vm.h
@@ -21,11 +21,11 @@ enum vm_privilege_level {
 #define INVALID_VM_ID 0xffffU
 
 struct vm_hw_info {
-	uint16_t num_vcpus;	/* Number of total virtual cores */
+	/* vcpu array of this VM */
+	struct vcpu vcpu_array[CONFIG_MAX_VCPUS_PER_VM];
 	uint16_t created_vcpus;	/* Number of created vcpus */
-	struct vcpu **vcpu_array;	/* vcpu array of this VM */
 	uint64_t gpa_lowtop;    /* top lowmem gpa of this VM */
-};
+} __aligned(CPU_PAGE_SIZE);
 
 struct sw_linux {
 	void *ramdisk_src_addr;		/* HVA */
@@ -130,10 +130,10 @@ struct vcpuid_entry {
 
 struct vm {
 	struct vm_arch arch_vm; /* Reference to this VM's arch information */
-	uint16_t vm_id;		    /* Virtual machine identifier */
 	struct vm_hw_info hw;	/* Reference to this VM's HW information */
 	struct vm_sw_info sw;	/* Reference to SW associated with this VM */
 	struct vm_pm_info pm;	/* Reference to this VM's arch information */
+	uint16_t vm_id;		    /* Virtual machine identifier */
 	enum vm_state state;	/* VM state */
 	struct acrn_vuart vuart;		/* Virtual UART */
 	enum vpic_wire_mode wire_mode;
diff --git a/hypervisor/include/arch/x86/ioreq.h b/hypervisor/include/arch/x86/ioreq.h
index 5b3a1ade8..c4d06c331 100644
--- a/hypervisor/include/arch/x86/ioreq.h
+++ b/hypervisor/include/arch/x86/ioreq.h
@@ -126,7 +126,9 @@ void dm_emulate_mmio_post(struct vcpu *vcpu);
 
 int32_t emulate_io(struct vcpu *vcpu, struct io_request *io_req);
 void emulate_io_post(struct vcpu *vcpu);
-
+/*
+ * @pre vcpu != NULL && io_req != NULL
+ */
 int32_t acrn_insert_request_wait(struct vcpu *vcpu, struct io_request *io_req);
 
 #endif /* IOREQ_H */
diff --git a/hypervisor/include/arch/x86/irq.h b/hypervisor/include/arch/x86/irq.h
index 124c56340..be2df1fa9 100644
--- a/hypervisor/include/arch/x86/irq.h
+++ b/hypervisor/include/arch/x86/irq.h
@@ -110,7 +110,9 @@ void vcpu_inject_ac(struct vcpu *vcpu);
 void vcpu_inject_ss(struct vcpu *vcpu);
 void vcpu_make_request(struct vcpu *vcpu, uint16_t eventid);
 int vcpu_queue_exception(struct vcpu *vcpu, uint32_t vector, uint32_t err_code);
-
+/*
+ * @pre vcpu != NULL
+ */
 int exception_vmexit_handler(struct vcpu *vcpu);
 int interrupt_window_vmexit_handler(struct vcpu *vcpu);
 int external_interrupt_vmexit_handler(struct vcpu *vcpu);