26 lines
1.1 KiB
Diff
26 lines
1.1 KiB
Diff
--- src/kernel/sel4/src/arch/x86/kernel/vspace.c
|
|
+++ src/kernel/sel4/src/arch/x86/kernel/vspace.c
|
|
@@ -711,7 +711,6 @@ void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
|
|
{
|
|
findVSpaceForASID_ret_t find_ret;
|
|
lookupPTSlot_ret_t lu_ret;
|
|
- cap_t threadRoot;
|
|
lookupPDSlot_ret_t pd_ret;
|
|
pde_t *pde;
|
|
|
|
@@ -756,12 +756,8 @@ void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
|
|
break;
|
|
}
|
|
|
|
- /* check if page belongs to current address space */
|
|
- threadRoot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbVTable)->cap;
|
|
- if (config_set(CONFIG_SUPPORT_PCID) || (isValidNativeRoot(threadRoot) && (vspace_root_t*)pptr_of_cap(threadRoot) == find_ret.vspace_root)) {
|
|
- invalidateTranslationSingleASID(vptr, asid,
|
|
- SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
|
|
- }
|
|
+ invalidateTranslationSingleASID(vptr, asid,
|
|
+ SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
|
|
}
|
|
|
|
void unmapPageTable(asid_t asid, vptr_t vaddr, pte_t* pt)
|