portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

x86: Refactor tlb_bitmap to be mode generic

Browse source 
Refactors the TLB bitmap code to be generic across ia32 and x86-64.
This commit is contained in:
Adrian Danis 2016-11-09 15:22:09 +11:00
parent 9c91fc8f42
commit 2c49729da5
9 changed files with 108 additions and 110 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
include/arch/x86/arch/32/mode/fastpath/fastpath.h
View file

@ -18,7 +18,7 @@
#include <api/syscall.h>
#include <benchmark/benchmark_track.h>
#include <mode/stack.h>
#include <mode/kernel/tlb_bitmap.h>
#include <arch/kernel/tlb_bitmap.h>
static inline void
switchToThread_fp(tcb_t *thread, vspace_root_t *pd, pde_t stored_hw_asid)

77
include/arch/x86/arch/32/mode/kernel/tlb_bitmap.h
View file

@ -1,77 +0,0 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(D61_GPL)
*/
#ifndef __ARCH_MODE_KERNEL_TLB_BITMAP_H_
#define __ARCH_MODE_KERNEL_TLB_BITMAP_H_
#include <kernel/vspace.h>
#include <plat_mode/machine/hardware.h>
#include <machine.h>
#if CONFIG_MAX_NUM_NODES > 1
/* Bit zero for entries in PD are present bits and should always be 0 */
#define TLBBITMAP_ENTRIES_PER_PD 31
/* Number of entries in PD reserved for TLB bitmap */
#define TLBBITMAP_PD_ENTRIES (((CONFIG_MAX_NUM_NODES - 1) / TLBBITMAP_ENTRIES_PER_PD) + 1)
#define TLBBITMAP_PD_RESERVED (TLBBITMAP_PD_ENTRIES * BIT(LARGE_PAGE_BITS))
#define TLBBITMAP_PD_INDEX (TLBBITMAP_PPTR >> LARGE_PAGE_BITS)
/* Total number of usable bits in TLBbitmap */
#define TLBBITMAP_PD_BITS (TLBBITMAP_ENTRIES_PER_PD * TLBBITMAP_PD_ENTRIES)
#define TLBBITMAP_PD_MAKE_INDEX(_cpu) (TLBBITMAP_PD_INDEX + ((_cpu) / (wordBits - 1)))
#define TLBBITMAP_PD_MAKE_BIT(_cpu) BIT(((_cpu) % (wordBits - 1)) + 1)
static inline void
tlb_bitmap_init(pde_t *pd)
{
for (int i = 0; i < TLBBITMAP_PD_ENTRIES; i++) {
pd[TLBBITMAP_PD_INDEX + i] = makeUserPDEPageTableInvalid();
}
}
static inline void
tlb_bitmap_set(pde_t *pd, word_t cpu)
{
assert(cpu < TLBBITMAP_PD_BITS && cpu <= wordBits);
pd[TLBBITMAP_PD_MAKE_INDEX(cpu)].words[0] |= TLBBITMAP_PD_MAKE_BIT(cpu);
}
static inline void
tlb_bitmap_unset(pde_t *pd, word_t cpu)
{
assert(cpu < TLBBITMAP_PD_BITS && cpu <= wordBits);
pd[TLBBITMAP_PD_MAKE_INDEX(cpu)].words[0] &= ~TLBBITMAP_PD_MAKE_BIT(cpu);
}
static inline word_t
tlb_bitmap_get(pde_t *pd)
{
word_t bitmap = 0;
for (int i = 0; i < TLBBITMAP_PD_ENTRIES; i++) {
word_t entry = pd[TLBBITMAP_PD_INDEX + i].words[0];
// skip present bit
entry >>= 1;
int shift = i * TLBBITMAP_ENTRIES_PER_PD;
bitmap |= entry << shift;
}
return bitmap;
}
#else
#define TLBBITMAP_PD_RESERVED 0
#endif /* CONFIG_MAX_NUM_NODES */
#endif /* __ARCH_MODE_KERNEL_TLB_BITMAP_H_ */

2
include/arch/x86/arch/32/mode/object/structures.h
View file

@ -43,6 +43,8 @@ typedef pdpte_t vspace_root_t;
typedef pde_t vspace_root_t;
#endif
#define GET_VSPACE_ROOT_INDEX(x) ((x) >> (seL4_PageBits + PT_INDEX_BITS))
#define PDPTE_PTR(r) ((pdpte_t *)(r))
#define PDPTE_PTR_PTR(r) ((pdpte_t**)(r))
#define PDPTE_REF(p) ((word_t)(p))

18
include/arch/x86/arch/64/mode/kernel/tlb_bitmap.h
View file

@ -1,18 +0,0 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(D61_GPL)
*/
#ifndef __ARCH_MODE_KERNEL_TLB_BITMAP_H_
#define __ARCH_MODE_KERNEL_TLB_BITMAP_H_
/* This is placeholder file for 64 bit TLB bitmap implementation */
#endif /* __ARCH_MODE_KERNEL_TLB_BITMAP_H_ */

1
include/arch/x86/arch/64/mode/object/structures.h
View file

@ -61,6 +61,7 @@ compile_assert(uint64_t_size_64,
typedef pml4e_t vspace_root_t;
#define GET_PML4_INDEX(x) ( ((x) >> (PML4_INDEX_OFFSET)) & MASK(PML4_INDEX_BITS))
#define GET_VSPACE_ROOT_INDEX GET_PML4_INDEX
#define GET_PDPT_INDEX(x) ( ((x) >> (PDPT_INDEX_OFFSET)) & MASK(PDPT_INDEX_BITS))
#define GET_PD_INDEX(x) ( ((x) >> (PD_INDEX_OFFSET)) & MASK(PD_INDEX_BITS))
#define GET_PT_INDEX(x) ( ((x) >> (PT_INDEX_OFFSET)) & MASK(PT_INDEX_BITS))

78
include/arch/x86/arch/kernel/tlb_bitmap.h Normal file
View file

@ -0,0 +1,78 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(D61_GPL)
*/
#ifndef __ARCH_KERNEL_TLB_BITMAP_H_
#define __ARCH_KERNEL_TLB_BITMAP_H_
#include <config.h>
#include <types.h>
#include <plat_mode/machine/hardware.h>
#include <mode/kernel/vspace.h>
#if CONFIG_MAX_NUM_NODES > 1
/* Bit zero for entries in PD are present bits and should always be 0 */
#define TLBBITMAP_ENTRIES_PER_ROOT (wordBits - 1)
/* Number of entries in PD reserved for TLB bitmap */
#define TLBBITMAP_ROOT_ENTRIES (((CONFIG_MAX_NUM_NODES - 1) / TLBBITMAP_ENTRIES_PER_ROOT) + 1)
#define TLBBITMAP_RESERVED_VSPACE (TLBBITMAP_ROOT_ENTRIES * BIT(TLBBITMAP_ROOT_ENTRY_SIZE))
#define TLBBITMAP_ROOT_INDEX GET_VSPACE_ROOT_INDEX(TLBBITMAP_PPTR)
/* Total number of usable bits in TLBbitmap */
#define TLBBITMAP_ROOT_BITS (TLBBITMAP_ENTRIES_PER_ROOT * TLBBITMAP_ROOT_ENTRIES)
#define TLBBITMAP_ROOT_MAKE_INDEX(_cpu) (TLBBITMAP_ROOT_INDEX + ((_cpu) / TLBBITMAP_ENTRIES_PER_ROOT))
#define TLBBITMAP_ROOT_MAKE_BIT(_cpu) BIT(((_cpu) % TLBBITMAP_ENTRIES_PER_ROOT) + 1)
static inline void
tlb_bitmap_init(vspace_root_t *root)
{
for (int i = 0; i < TLBBITMAP_ROOT_ENTRIES; i++) {
root[TLBBITMAP_ROOT_INDEX + i] = x86_make_empty_root_mapping();
}
}
static inline void
tlb_bitmap_set(vspace_root_t *root, word_t cpu)
{
assert(cpu < TLBBITMAP_ROOT_BITS && cpu <= wordBits);
root[TLBBITMAP_ROOT_MAKE_INDEX(cpu)].words[0] |= TLBBITMAP_ROOT_MAKE_BIT(cpu);
}
static inline void
tlb_bitmap_unset(vspace_root_t *root, word_t cpu)
{
assert(cpu < TLBBITMAP_ROOT_BITS && cpu <= wordBits);
root[TLBBITMAP_ROOT_MAKE_INDEX(cpu)].words[0] &= ~TLBBITMAP_ROOT_MAKE_BIT(cpu);
}
static inline word_t
tlb_bitmap_get(vspace_root_t *root)
{
word_t bitmap = 0;
for (int i = 0; i < TLBBITMAP_ROOT_ENTRIES; i++) {
word_t entry = root[TLBBITMAP_ROOT_INDEX + i].words[0];
// skip present bit
entry >>= 1;
int shift = i * TLBBITMAP_ENTRIES_PER_ROOT;
bitmap |= entry << shift;
}
return bitmap;
}
#else
#define TLBBITMAP_ROOT_ENTRIES 0
#endif /* CONFIG_MAX_NUM_NODES */
#endif /* __ARCH_KERNEL_TLB_BITMAP_H_ */

34
include/plat/pc99/plat/32/plat_mode/machine/hardware.h
View file

@ -11,28 +11,40 @@
#ifndef __PLAT_MODE_MACHINE_HARDWARE_H
#define __PLAT_MODE_MACHINE_HARDWARE_H
#include <config.h>
/* WARNING: some of these constants are also defined in linker.lds */
#define PADDR_BASE 0x00000000
#define PADDR_LOAD 0x00100000
#define PPTR_BASE 0xe0000000
#ifdef CONFIG_PAE_PAGING
#define PPTR_USER_TOP (PPTR_BASE & (~MASK(seL4_HugePageBits)))
#else
#define PPTR_USER_TOP (PPTR_BASE & (~MASK(seL4_LargePageBits)))
#endif
/* Calculate virtual address space reserved for TLB Bitmap. ROOT_ENTRIES
* will be zero in the case where the bitmap is unused */
#define TLBBITMAP_PD_RESERVED (TLBBITMAP_ROOT_ENTRIES * BIT(seL4_LargePageBits))
/* Calculate virtual address space reserved for dynamic log buffer mapping */
#ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER
#define PPTR_TOP (-BIT(LARGE_PAGE_BITS + 1) - TLBBITMAP_PD_RESERVED)
#define KS_LOG_PPTR PPTR_TOP
#if CONFIG_MAX_NUM_NODES > 1
/* The start address which is unusable and reserved for TLBBitmap */
#define TLBBITMAP_PPTR (PPTR_TOP + BIT(LARGE_PAGE_BITS))
#endif /* CONFIG_MAX_NUM_NODES */
#define LOGBUFFER_PD_RESERVED BIT(seL4_LargePageBits)
#else
#define PPTR_TOP (-BIT(LARGE_PAGE_BITS) - TLBBITMAP_PD_RESERVED)
#if CONFIG_MAX_NUM_NODES > 1
#define TLBBITMAP_PPTR PPTR_TOP
#endif /* CONFIG_MAX_NUM_NODES */
#endif /* CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER */
#define LOGBUFFER_PD_RESERVED 0
#endif
/* There is a page table (where the kernel devices will go) in the last
* slot in memory */
#define PPTR_KERNEL_PT_BASE (-BIT(LARGE_PAGE_BITS))
/* TLB bitmap is next after the PT */
#define TLBBITMAP_PPTR (PPTR_KERNEL_PT_BASE - TLBBITMAP_PD_RESERVED)
/* After TLB bitmap is the log buffer */
#define KERNEL_LOG_PPTR (TLBBITMAP_PPTR - LOGBUFFER_PD_RESERVED)
/* This then marks the end of where physical memory gets mapped */
#define PPTR_TOP KERNEL_LOG_PPTR
#define PPTR_KDEV 0xffff0000
#define BASE_OFFSET (PPTR_BASE - PADDR_BASE)
#define kernelBase PPTR_USER_TOP

4
src/arch/x86/32/kernel/vspace.c
View file

@ -17,7 +17,7 @@
#include <arch/kernel/boot.h>
#include <arch/api/invocation.h>
#include <benchmark/benchmark_track.h>
#include <mode/kernel/tlb_bitmap.h>
#include <arch/kernel/tlb_bitmap.h>
#include <mode/kernel/tlb.h>
/* 'gdt_idt_ptr' is declared globally because of a C-subset restriction.
@ -287,7 +287,7 @@ map_kernel_window(
tlb_bitmap_init(ia32KSGlobalPD);
phys += TLBBITMAP_PD_RESERVED;
idx += TLBBITMAP_PD_ENTRIES;
idx += TLBBITMAP_ROOT_ENTRIES;
#endif /* CONFIG_MAX_NUM_NODES */
/* map page table of last 4M of virtual address space to page directory */

2
src/arch/x86/kernel/vspace.c
View file

@ -15,7 +15,7 @@
#include <model/statedata.h>
#include <arch/kernel/vspace.h>
#include <arch/api/invocation.h>
#include <mode/kernel/tlb_bitmap.h>
#include <arch/kernel/tlb_bitmap.h>
#include <mode/kernel/tlb.h>
#include <mode/kernel/vspace.h>