ehmry/genode
ehmry/genode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
ef130a3bf9
genode/repos/base-sel4/src/core/include/vm_space.h

507 lines
14 KiB
C
Raw Normal View History

sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/*
* \brief Virtual-memory space
* \author Norman Feske
* \date 2015-05-04
*/
/*
Adjust file headers to refer to the AGPLv3
2017-02-20 13:23:52 +01:00
* Copyright (C) 2015-2017 Genode Labs GmbH
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
*
* This file is part of the Genode OS framework, which is distributed
Adjust file headers to refer to the AGPLv3
2017-02-20 13:23:52 +01:00
* under the terms of the GNU Affero General Public License version 3.
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
*/
#ifndef _CORE__INCLUDE__VM_SPACE_H_
#define _CORE__INCLUDE__VM_SPACE_H_
/* Genode includes */
#include <util/bit_allocator.h>
base: rename 'Volatile_object' to 'Reconstructible' Fixes #2151
2016-12-01 17:37:08 +01:00
#include <util/reconstructible.h>
sel4: update to 3.1.0 - adjust syscall bindings to support -fPIC - read serial i/o ports from BIOS data area - use autoconf.h provided by sel4 -- to avoid ambiguity between sel4 kernel and user libraries -- remove manual set defines - remove debug messages - increase user virtual area to 3GB Issue #1720 Issue #2044
2016-06-17 15:15:48 +02:00
#include <base/log.h>
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
#include <base/thread.h>
sel4: show pd name if flushing page table Issue #2044
2016-07-08 14:03:43 +02:00
#include <base/session_label.h>
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/* core includes */
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
#include <base/internal/capability_space_sel4.h>
#include <base/internal/stack_area.h>
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
#include <page_table_registry.h>
#include <cnode.h>
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
#include <cap_sel_alloc.h>
#include <core_cspace.h>
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
namespace Genode { class Vm_space; }
class Genode::Vm_space
{
private:
sel4: show pd name if flushing page table Issue #2044
2016-07-08 14:03:43 +02:00
Session_label _pd_label;
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
Cap_sel_alloc &_cap_sel_alloc;
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
Page_table_registry &_page_table_registry;
unsigned const _id;
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
Cap_sel const _pd_sel;
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
Range_allocator &_phys_alloc;
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
enum {
/**
* Number of entries of 3rd-level VM CNode ('_vm_3rd_cnode')
*/
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
VM_3RD_CNODE_SIZE_LOG2 = (CONFIG_WORD_SIZE == 32) ? 8 : 7,
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
/**
* Number of entries of each leaf CNodes
*/
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
LEAF_CNODE_SIZE_LOG2 = (CONFIG_WORD_SIZE == 32) ? 8 : 7,
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
LEAF_CNODE_SIZE = 1UL << LEAF_CNODE_SIZE_LOG2,
/**
* Number of leaf CNodes
*/
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
NUM_LEAF_CNODES_LOG2 = (CONFIG_WORD_SIZE == 32) ? 6 : 5,
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
NUM_LEAF_CNODES = 1UL << NUM_LEAF_CNODES_LOG2,
/**
* Maximum number of page tables and page frames for the VM space
*/
NUM_VM_SEL_LOG2 = LEAF_CNODE_SIZE_LOG2 + NUM_LEAF_CNODES_LOG2,
/**
* Number of entries of the VM padding CNode ('_vm_pad_cnode')
*/
VM_PAD_CNODE_SIZE_LOG2 = 32 - Core_cspace::NUM_TOP_SEL_LOG2
- VM_3RD_CNODE_SIZE_LOG2 - LEAF_CNODE_SIZE_LOG2,
};
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
Cnode &_top_level_cnode;
Cnode &_phys_cnode;
/**
* 2nd-level CNode for aligning '_vm_cnode' with the LSB of the CSpace
*/
Cnode _vm_pad_cnode;
/**
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
* 3rd-level CNode that hosts the leaf CNodes
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
*/
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
Cnode _vm_3rd_cnode;
/***
* 4th-level CNode for storing page-table and page-frame capabilities
*/
class Leaf_cnode
{
private:
/*
* We leave the CNode unconstructed at the time of its
* instantiation to be able to create an array of 'Leaf_cnode'
* objects (where we cannot pass any arguments to the
* constructors of the individual objects).
*/
Follow practices suggested by "Effective C++" The patch adjust the code of the base, base-<kernel>, and os repository. To adapt existing components to fix violations of the best practices suggested by "Effective C++" as reported by the -Weffc++ compiler argument. The changes follow the patterns outlined below: * A class with virtual functions can no longer publicly inherit base classed without a vtable. The inherited object may either be moved to a member variable, or inherited privately. The latter would be used for classes that inherit 'List::Element' or 'Avl_node'. In order to enable the 'List' and 'Avl_tree' to access the meta data, the 'List' must become a friend. * Instead of adding a virtual destructor to abstract base classes, we inherit the new 'Interface' class, which contains a virtual destructor. This way, single-line abstract base classes can stay as compact as they are now. The 'Interface' utility resides in base/include/util/interface.h. * With the new warnings enabled, all member variables must be explicitly initialized. Basic types may be initialized with '='. All other types are initialized with braces '{ ... }' or as class initializers. If basic types and non-basic types appear in a row, it is nice to only use the brace syntax (also for basic types) and align the braces. * If a class contains pointers as members, it must now also provide a copy constructor and assignment operator. In the most cases, one would make them private, effectively disallowing the objects to be copied. Unfortunately, this warning cannot be fixed be inheriting our existing 'Noncopyable' class (the compiler fails to detect that the inheriting class cannot be copied and still gives the error). For now, we have to manually add declarations for both the copy constructor and assignment operator as private class members. Those declarations should be prepended with a comment like this: /* * Noncopyable */ Thread(Thread const &); Thread &operator = (Thread const &); In the future, we should revisit these places and try to replace the pointers with references. In the presence of at least one reference member, the compiler would no longer implicitly generate a copy constructor. So we could remove the manual declaration. Issue #465
2017-12-21 15:42:15 +01:00
Constructible<Cnode> _cnode { };
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
public:
void construct(Cap_sel_alloc &cap_sel_alloc,
Cap_sel core_cnode_sel,
Range_allocator &phys_alloc)
{
_cnode.construct(core_cnode_sel, cap_sel_alloc.alloc(),
LEAF_CNODE_SIZE_LOG2, phys_alloc);
}
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
void destruct(Cap_sel_alloc &cap_sel_alloc,
Range_allocator &phys_alloc)
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
{
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
_cnode->destruct(phys_alloc);
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
cap_sel_alloc.free(_cnode->sel());
}
Cnode &cnode() { return *_cnode; }
};
Leaf_cnode _vm_cnodes[NUM_LEAF_CNODES];
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/**
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
* Allocator for the selectors within '_vm_cnodes'
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
*/
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
using Selector_allocator = Bit_allocator<1UL << NUM_VM_SEL_LOG2>;
Selector_allocator _sel_alloc { };
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
/**
* Return leaf CNode that contains an index allocated from '_sel_alloc'
*/
Cnode &_leaf_cnode(unsigned idx)
{
return _vm_cnodes[idx >> LEAF_CNODE_SIZE_LOG2].cnode();
}
/**
* Return entry within leaf cnode
*/
Cnode_index _leaf_cnode_entry(unsigned idx) const
{
return Cnode_index(idx & (LEAF_CNODE_SIZE - 1));
}
Follow practices suggested by "Effective C++" The patch adjust the code of the base, base-<kernel>, and os repository. To adapt existing components to fix violations of the best practices suggested by "Effective C++" as reported by the -Weffc++ compiler argument. The changes follow the patterns outlined below: * A class with virtual functions can no longer publicly inherit base classed without a vtable. The inherited object may either be moved to a member variable, or inherited privately. The latter would be used for classes that inherit 'List::Element' or 'Avl_node'. In order to enable the 'List' and 'Avl_tree' to access the meta data, the 'List' must become a friend. * Instead of adding a virtual destructor to abstract base classes, we inherit the new 'Interface' class, which contains a virtual destructor. This way, single-line abstract base classes can stay as compact as they are now. The 'Interface' utility resides in base/include/util/interface.h. * With the new warnings enabled, all member variables must be explicitly initialized. Basic types may be initialized with '='. All other types are initialized with braces '{ ... }' or as class initializers. If basic types and non-basic types appear in a row, it is nice to only use the brace syntax (also for basic types) and align the braces. * If a class contains pointers as members, it must now also provide a copy constructor and assignment operator. In the most cases, one would make them private, effectively disallowing the objects to be copied. Unfortunately, this warning cannot be fixed be inheriting our existing 'Noncopyable' class (the compiler fails to detect that the inheriting class cannot be copied and still gives the error). For now, we have to manually add declarations for both the copy constructor and assignment operator as private class members. Those declarations should be prepended with a comment like this: /* * Noncopyable */ Thread(Thread const &); Thread &operator = (Thread const &); In the future, we should revisit these places and try to replace the pointers with references. In the presence of at least one reference member, the compiler would no longer implicitly generate a copy constructor. So we could remove the manual declaration. Issue #465
2017-12-21 15:42:15 +01:00
Lock _lock { };
sel4: bootstrap of init and page-fault handling
2015-05-12 12:48:03 +02:00
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/**
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
* Return selector for a capability slot within '_vm_cnodes'
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
*/
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
addr_t _idx_to_sel(addr_t idx) const { return (_id << 20) | idx; }
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
template <typename FN>
void _flush(bool const flush_support, FN const &fn)
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
{
if (!flush_support) {
warning("mapping cache full, but can't flush");
throw;
}
warning("flush page table entries - mapping cache full - PD: ",
_pd_label.string());
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
_page_table_registry.flush_pages(fn);
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
}
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
template <typename FN>
bool _map_frame(addr_t const from_phys, addr_t const to_dest,
sel4: add Wandboard Quad (iMX6) support Issue #2451
2017-07-04 14:17:38 +02:00
Cache_attribute const cacheability,
sel4: enable nx bit handling for ARM Issue #1723
2017-10-17 11:51:13 +02:00
bool const writable, bool const executable,
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
bool const flush_support, bool guest, FN const &fn)
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
{
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
if (_page_table_registry.page_frame_at(to_dest)) {
sel4: add Wandboard Quad (iMX6) support Issue #2451
2017-07-04 14:17:38 +02:00
/*
* Valid behaviour if multiple threads concurrently
* causing the same page-fault. For the first thread the
* fault will be resolved, and the next thread will/would do
* it again. We just skip this attempt in order to avoid
* wasting of resources (idx selectors, creating kernel
* capabilities, causing kernel warning ...).
*/
return false;
}
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
/* allocate page-table-entry selector */
addr_t pte_idx;
try { pte_idx = _sel_alloc.alloc(); }
catch (Selector_allocator::Out_of_indices) {
/* free all page-table-entry selectors and retry once */
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
_flush(flush_support, fn);
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
pte_idx = _sel_alloc.alloc();
}
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/*
* Copy page-frame selector to pte_sel
*
* This is needed because each page-frame selector can be
* inserted into only a single page table.
*/
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
_leaf_cnode(pte_idx).copy(_phys_cnode,
Cnode_index(from_phys >> get_page_size_log2()),
Cnode_index(_leaf_cnode_entry(pte_idx)));
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/* remember relationship between pte_sel and the virtual address */
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
try { _page_table_registry.insert_page_frame(to_dest, Cap_sel(pte_idx)); }
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
catch (Page_table_registry::Mapping_cache_full) {
sel4: flush page table allocator if full Issue #2044
2016-07-08 13:44:52 +02:00
base-sel4: handle PTE selectors exceeded In Vm_space::map when allocating a new page-table-entry selector, the allocator may throw an exception that there are no selecztors left which was not caught by now. Now, we catch this exception, flush the mapping cache to free all selectors again and retry to allocate. Fixes #2781
2018-04-19 15:09:30 +02:00
/* free all entries of mapping cache and re-try once */
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
_flush(flush_support, fn);
_page_table_registry.insert_page_frame(to_dest, Cap_sel(pte_idx));
sel4: flush page table allocator if full Issue #2044
2016-07-08 13:44:52 +02:00
}
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/*
* Insert copy of page-frame selector into page table
*/
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
long ret = _map_page(Cap_sel(pte_idx), to_dest, cacheability,
writable, executable, guest);
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
if (ret != seL4_NoError) {
error("seL4_*_Page_Map ", Hex(from_phys), "->",
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
Hex(to_dest), " returned ", ret);
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
return false;
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
}
sel4: quirk for vanishing page table Issue #2044
2016-07-15 18:43:37 +02:00
return true;
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
}
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
/**
* Platform specific map/unmap of a page frame
*/
sel4: add Wandboard Quad (iMX6) support Issue #2451
2017-07-04 14:17:38 +02:00
long _map_page(Genode::Cap_sel const &idx, Genode::addr_t const virt,
sel4: enable nx bit handling for ARM Issue #1723
2017-10-17 11:51:13 +02:00
Cache_attribute const cacheability, bool const write,
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
bool const writable, bool guest);
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
long _unmap_page(Genode::Cap_sel const &idx);
sel4: invalidate ram if used uncached later on Fixes #2665
2018-03-28 14:06:18 +02:00
long _invalidate_page(Genode::Cap_sel const &, seL4_Word const,
seL4_Word const);
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
class Alloc_page_table_failed : Exception { };
/**
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
* Allocate and install page structures for the protection domain.
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
*
* \throw Alloc_page_table_failed
*/
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
template <typename KOBJ>
Cap_sel _alloc_and_map(addr_t const virt,
long (&map_fn)(Cap_sel, Cap_sel, addr_t),
addr_t &phys)
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
{
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
/* allocate page-* selector */
addr_t const idx = _sel_alloc.alloc();
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
sel4: add include/kernel_object.h utilties
2015-05-08 12:18:09 +02:00
try {
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
phys = Untyped_memory::alloc_page(_phys_alloc);
seL4_Untyped const service = Untyped_memory::untyped_sel(phys).value();
create<KOBJ>(service, _leaf_cnode(idx).sel(),
_leaf_cnode_entry(idx));
sel4: workaround deadlock in core Issue #2044
2016-07-25 14:44:36 +02:00
} catch (...) {
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
/* XXX free idx, revert untyped memory, phys_addr, */
sel4: workaround deadlock in core Issue #2044
2016-07-25 14:44:36 +02:00
throw Alloc_page_table_failed();
}
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
Cap_sel const pt_sel(_idx_to_sel(idx));
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
long const result = map_fn(pt_sel, _pd_sel, virt);
if (result != seL4_NoError)
error("seL4_*_Page*_Map(,", Hex(virt), ") returned ",
result);
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
return Cap_sel(idx);
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
}
public:
/**
* Constructor
*
sel4: bootstrap of init and page-fault handling
2015-05-12 12:48:03 +02:00
* \param pd_sel selector for page directory
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
* \param cap_sel_alloc capability-selector allocator used for
* VM CNodes
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
* \param phys_alloc backing store for the CNodes
* \param top_level_cnode top-level CNode to insert 'vm_pad_cnode_sel'
* \param id ID used as index in 'top_level_cnode'
* \param page_table_registry association of VM CNode selectors with
* with virtual addresses
*/
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
Vm_space(Cap_sel pd_sel,
Cap_sel_alloc &cap_sel_alloc,
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
Range_allocator &phys_alloc,
Cnode &top_level_cnode,
Cnode &core_cnode,
Cnode &phys_cnode,
unsigned id,
sel4: show pd name if flushing page table Issue #2044
2016-07-08 14:03:43 +02:00
Page_table_registry &page_table_registry,
const char * label)
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
:
sel4: show pd name if flushing page table Issue #2044
2016-07-08 14:03:43 +02:00
_pd_label(label),
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
_cap_sel_alloc(cap_sel_alloc),
sel4: bootstrap of init and page-fault handling
2015-05-12 12:48:03 +02:00
_page_table_registry(page_table_registry),
_id(id), _pd_sel(pd_sel),
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
_phys_alloc(phys_alloc),
_top_level_cnode(top_level_cnode),
_phys_cnode(phys_cnode),
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
_vm_pad_cnode(core_cnode.sel(),
Cnode_index(_cap_sel_alloc.alloc().value()),
VM_PAD_CNODE_SIZE_LOG2, phys_alloc),
_vm_3rd_cnode(core_cnode.sel(),
Cnode_index(_cap_sel_alloc.alloc().value()),
VM_3RD_CNODE_SIZE_LOG2, phys_alloc)
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
{
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
Cnode_base const cspace(Cap_sel(seL4_CapInitThreadCNode), 32);
for (unsigned i = 0; i < NUM_LEAF_CNODES; i++) {
/* init leaf VM CNode */
_vm_cnodes[i].construct(_cap_sel_alloc, core_cnode.sel(), phys_alloc);
/* insert leaf VM CNode into 3nd-level VM CNode */
_vm_3rd_cnode.copy(cspace, _vm_cnodes[i].cnode().sel(), Cnode_index(i));
}
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/* insert 3rd-level VM CNode into 2nd-level VM-pad CNode */
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
_vm_pad_cnode.copy(cspace, _vm_3rd_cnode.sel(), Cnode_index(0));
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
/* insert 2nd-level VM-pad CNode into 1st-level CNode */
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
_top_level_cnode.copy(cspace, _vm_pad_cnode.sel(), Cnode_index(_id));
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
}
~Vm_space()
{
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
/* delete copy of the mapping's page-frame selectors */
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
_page_table_registry.flush_all([&] (Cap_sel const &idx, addr_t const virt) {
long err = _unmap_page(idx);
if (err != seL4_NoError)
error("unmap ", Hex(virt), " failed, ", idx, " res=", err);
_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
_sel_alloc.free(idx.value());
return true;
}, [&] (Cap_sel const &idx, addr_t const paddr) {
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
_leaf_cnode(idx.value()).remove(idx);
_sel_alloc.free(idx.value());
Untyped_memory::free_page(_phys_alloc, paddr);
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
});
for (unsigned i = 0; i < NUM_LEAF_CNODES; i++) {
_vm_3rd_cnode.remove(Cnode_index(i));
_vm_cnodes[i].destruct(_cap_sel_alloc, _phys_alloc);
}
_vm_pad_cnode.remove(Cnode_index(0));
_top_level_cnode.remove(Cnode_index(_id));
_vm_3rd_cnode.destruct(_phys_alloc);
_vm_pad_cnode.destruct(_phys_alloc);
sel4: update to version 2.1 This patch updates seL4 from the experimental branch of one year ago to the master branch of version 2.1. The transition has the following implications. In contrast to the experimental branch, the master branch has no way to manually define the allocation of kernel objects within untyped memory ranges. Instead, the kernel maintains a built-in allocation policy. This policy rules out the deallocation of once-used parts of untyped memory. The only way to reuse memory is to revoke the entire untyped memory range. Consequently, we cannot share a large untyped memory range for kernel objects of different protection domains. In order to reuse memory at a reasonably fine granularity, we need to split the initial untyped memory ranges into small chunks that can be individually revoked. Those chunks are called "untyped pages". An untyped page is a 4 KiB untyped memory region. The bootstrapping of core has to employ a two-stage allocation approach now. For creating the initial kernel objects for core, which remain static during the entire lifetime of the system, kernel objects are created directly out of the initial untyped memory regions as reported by the kernel. The so-called "initial untyped pool" keeps track of the consumption of those untyped memory ranges by mimicking the kernel's internal allocation policy. Kernel objects created this way can be of any size. For example the phys CNode, which is used to store page-frame capabilities is 16 MiB in size. Also, core's CSpace uses a relatively large CNode. After the initial setup phase, all remaining untyped memory is turned into untyped pages. From this point on, new created kernel objects cannot exceed 4 KiB in size because one kernel object cannot span multiple untyped memory regions. The capability selectors for untyped pages are organized similarly to those of page-frame capabilities. There is a new 2nd-level CNode (UNTYPED_CORE_CNODE) that is dimensioned according to the maximum amount of physical memory (1M entries, each entry representing 4 KiB). The CNode is organized such that an index into the CNode directly corresponds to the physical frame number of the underlying memory. This way, we can easily determine a untyped page selector for any physical addresses, i.e., for revoking the kernel objects allocated at a specific physical page. The downside is the need for another 16 MiB chunk of meta data. Also, we need to keep in mind that this approach won't scale to 64-bit systems. We will eventually need to replace the PHYS_CORE_CNODE and UNTYPED_CORE_CNODE by CNode hierarchies to model a sparsely populated CNode. The size constrain of kernel objects has the immediate implication that the VM CSpaces of protection domains must be organized via several levels of CNodes. I.e., as the top-level CNode of core has a size of 2^12, the remaining 20 PD-specific CSpace address bits are organized as a 2nd-level 2^4 padding CNode, a 3rd-level 2^8 CNode, and several 4th-level 2^8 leaf CNodes. The latter contain the actual selectors for the page tables and page-table entries of the respective PD. As another slight difference from the experimental branch, the master branch requires the explicit assignment of page directories to an ASID pool. Besides the adjustment to the new seL4 version, the patch introduces a dedicated type for capability selectors. Previously, we just used to represent them as unsigned integer values, which became increasingly confusing. The new type 'Cap_sel' is a PD-local capability selector. The type 'Cnode_index' is an index into a CNode (which is not generally not the entire CSpace of the PD). Fixes #1887
2016-02-03 14:50:44 +01:00
_cap_sel_alloc.free(_vm_3rd_cnode.sel());
sel4: handle platform_pd destruction Issue #2044
2016-07-13 16:03:21 +02:00
_cap_sel_alloc.free(_vm_pad_cnode.sel());
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
}
sel4/arm: make alignment faults visible Fixes #2993
2018-09-21 08:44:23 +02:00
bool map(addr_t const from_phys, addr_t const to_virt,
sel4: add Wandboard Quad (iMX6) support Issue #2451
2017-07-04 14:17:38 +02:00
size_t const num_pages, Cache_attribute const cacheability,
sel4: enable nx bit handling for ARM Issue #1723
2017-10-17 11:51:13 +02:00
bool const writable, bool const executable, bool flush_support)
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
{
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
auto fn_unmap = [&] (Cap_sel const &idx, addr_t const v_addr)
{
/* XXX - INITIAL_IPC_BUFFER can't be re-mapped currently */
if (v_addr == 0x1000)
return false;
/* XXX - UTCB can't be re-mapped currently */
if (stack_area_virtual_base() <= v_addr
&& (v_addr < stack_area_virtual_base() +
stack_area_virtual_size())
&& !((v_addr + 0x1000) & (stack_virtual_size() - 1)))
return false;
long err = _unmap_page(idx);
if (err != seL4_NoError)
error("unmap failed, idx=", idx, " res=", err);
_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
_sel_alloc.free(idx.value());
return true;
};
sel4: allocate vm-space meta data statically This patch removes the dynamically growing slab allocator from the page-table registry. This has two benefits. First, we alleviate the corner cases where the slab allocator needed to extend its backing store while establishing a core-local memory mapping, thereby triggering a nested core-local mapping. Without this corner case, no reentrant lock is needed any longer. Second, it removes the dependency from the overly large old API of the slab allocator. So we can tighten the slab interface.
2016-04-05 15:16:39 +02:00
Lock::Guard guard(_lock);
sel4: bootstrap of init and page-fault handling
2015-05-12 12:48:03 +02:00
sel4/arm: make alignment faults visible Fixes #2993
2018-09-21 08:44:23 +02:00
bool ok = true;
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
for (size_t i = 0; i < num_pages; i++) {
off_t const offset = i << get_page_size_log2();
sel4: fix vm_space has_page_table_at Issue #2044
2016-07-15 13:44:40 +02:00
sel4/arm: make alignment faults visible Fixes #2993
2018-09-21 08:44:23 +02:00
if (_map_frame(from_phys + offset, to_virt + offset,
cacheability, writable, executable,
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
flush_support, false /* host page table */,
fn_unmap))
sel4/arm: make alignment faults visible Fixes #2993
2018-09-21 08:44:23 +02:00
continue;
ok = false;
warning("mapping failed ", Hex(from_phys + offset),
" -> ", Hex(to_virt + offset), " ",
!flush_support ? "core" : "");
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
}
sel4/arm: make alignment faults visible Fixes #2993
2018-09-21 08:44:23 +02:00
return ok;
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
}
sel4: unmapping of virtual memory
2015-05-07 15:47:15 +02:00
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
void map_guest(addr_t const from_phys, addr_t const guest_phys,
size_t const num_pages, Cache_attribute const cacheability,
bool const writable, bool const executable, bool flush_support)
{
auto fn_unmap = [&] (Cap_sel const &idx, addr_t const) {
long err = _unmap_page(idx);
if (err != seL4_NoError)
error("unmap failed, idx=", idx, " res=", err);
_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
_sel_alloc.free(idx.value());
return true;
};
Lock::Guard guard(_lock);
for (size_t i = 0; i < num_pages; i++) {
off_t const offset = i << get_page_size_log2();
_map_frame(from_phys + offset, guest_phys + offset,
cacheability, writable, executable,
flush_support, true /* guest page table */,
fn_unmap);
}
}
sel4: invalidate ram if used uncached later on Fixes #2665
2018-03-28 14:06:18 +02:00
bool unmap(addr_t const virt, size_t const num_pages,
bool const invalidate = false)
sel4: unmapping of virtual memory
2015-05-07 15:47:15 +02:00
{
sel4: handle unmap error more gracefully Issue #2505
2017-08-24 11:53:19 +02:00
bool unmap_success = true;
sel4: allocate vm-space meta data statically This patch removes the dynamically growing slab allocator from the page-table registry. This has two benefits. First, we alleviate the corner cases where the slab allocator needed to extend its backing store while establishing a core-local memory mapping, thereby triggering a nested core-local mapping. Without this corner case, no reentrant lock is needed any longer. Second, it removes the dependency from the overly large old API of the slab allocator. So we can tighten the slab interface.
2016-04-05 15:16:39 +02:00
Lock::Guard guard(_lock);
sel4: bootstrap of init and page-fault handling
2015-05-12 12:48:03 +02:00
sel4: handle unmap error more gracefully Issue #2505
2017-08-24 11:53:19 +02:00
for (size_t i = 0; unmap_success && i < num_pages; i++) {
sel4: unmapping of virtual memory
2015-05-07 15:47:15 +02:00
off_t const offset = i << get_page_size_log2();
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
_page_table_registry.flush_page(virt + offset, [&] (Cap_sel const &idx, addr_t) {
sel4: invalidate ram if used uncached later on Fixes #2665
2018-03-28 14:06:18 +02:00
if (invalidate) {
long result = _invalidate_page(idx, virt + offset,
virt + offset + 4096);
if (result != seL4_NoError)
error("invalidating ", Hex(virt + offset),
" failed, idx=", idx, " result=", result);
}
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
long result = _unmap_page(idx);
if (result != seL4_NoError) {
error("unmap ", Hex(virt + offset), " failed, idx=",
idx, " result=", result);
sel4: handle unmap error more gracefully Issue #2505
2017-08-24 11:53:19 +02:00
unmap_success = false;
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
}
_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
_sel_alloc.free(idx.value());
});
sel4: unmapping of virtual memory
2015-05-07 15:47:15 +02:00
}
sel4: handle unmap error more gracefully Issue #2505
2017-08-24 11:53:19 +02:00
return unmap_success;
sel4: unmapping of virtual memory
2015-05-07 15:47:15 +02:00
}
sel4: update to 5.2.0 Issue #2451
2017-06-12 12:41:38 +02:00
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
void unsynchronized_alloc_page_tables(addr_t const start,
addr_t const size);
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
void unsynchronized_alloc_guest_page_tables(addr_t, addr_t);
sel4: update to 5.2.0 Issue #2451
2017-06-12 12:41:38 +02:00
void alloc_page_tables(addr_t const start, addr_t const size)
{
Lock::Guard guard(_lock);
sel4: add x86_64 support Issue #2451
2017-06-22 18:47:02 +02:00
unsynchronized_alloc_page_tables(start, size);
sel4: update to 5.2.0 Issue #2451
2017-06-12 12:41:38 +02:00
}
sel4: add Wandboard Quad (iMX6) support Issue #2451
2017-07-04 14:17:38 +02:00
sel4/x86: implement vm_session interface Issue #3111 - enable vt-x in kernel configuration Kernel patches: - add unrestricted guest support - avoid kernel boot failure when vt-x is not available - avoid nullpointer in kernel when vcpu is not fully setup - avoid vcpu scheduling bug which causes starvation on same/below prio level - save efer register correctly from guest
2018-09-26 11:00:01 +02:00
void alloc_guest_page_tables(addr_t const start, addr_t const size)
{
Lock::Guard guard(_lock);
unsynchronized_alloc_guest_page_tables(start, size);
}
sel4: add Wandboard Quad (iMX6) support Issue #2451
2017-07-04 14:17:38 +02:00
Session_label const & pd_label() const { return _pd_label; }
sel4: management of core's virtual memory
2015-05-05 00:15:50 +02:00
};
#endif /* _CORE__INCLUDE__VM_SPACE_H_ */
Reference in New Issue Copy Permalink