Commit Graph

75 Commits

Author SHA1 Message Date
Norman Feske
62b1c55399 Integrate CAP session into PD session
This patch integrates the functionality of the former CAP session into
the PD session and unifies the approch of supplementing the generic PD
session with kernel-specific functionality. The latter is achieved by
the new 'Native_pd' interface. The kernel-specific interface can be
obtained via the Pd_session::native_pd accessor function. The
kernel-specific interfaces are named Nova_native_pd, Foc_native_pd, and
Linux_native_pd.

The latter change allowed for to deduplication of the
pd_session_component code among the various base platforms.

To retain API compatibility, we keep the 'Cap_session' and
'Cap_connection' around. But those classes have become mere wrappers
around the PD session interface.

Issue #1841
2016-03-07 12:34:44 +01:00
Norman Feske
b1910cdd54 Integrate SIGNAL session into PD session
This patch removes the SIGNAL service from core and moves its
functionality to the PD session. Furthermore, it unifies the PD service
implementation and terminology across the various base platforms.

Issue #1841
2016-03-07 12:34:44 +01:00
Christian Helmuth
0d6dc46bbb sel4: use O3 optimization level
This is the default optimization level in the original seL4 SDK. By
adapting to O3, we work around a bug [1] in version 2.1.0 that only
shows on low optimization levels.

[1] https://github.com/seL4/seL4/issues/20
2016-03-07 12:34:43 +01:00
Martin Stein
ff10687a6c toolchain: report missing ports at once
Previously, ports that were needed for a scenario and that were not
prepared or outdated, triggered one assertion each during the second
build stage. The commit slots a mechanism in ahead that gathers all
these ports during the first build stage and reports them in form of a
list before the second build stage is entered.  This list can be used
directly as argument for tool/ports/prepare_port to prepare respectively
update the ports. If, however, this mechanism is not available, for
example because a target is build without the first build stage, the old
assertion still prevents the target from running into troubles with a
missing port.

Fixes #1872
2016-03-07 12:34:43 +01:00
Norman Feske
9e6f3be806 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-26 11:36:55 +01:00
Norman Feske
aaea28ae85 Fix build and execution of test/sel4 2015-10-06 12:18:56 +02:00
Stefan Kalkowski
ed52d5a211 Introduce 'spec' subdirectories to outline aspects
Instead of holding SPEC-variable dependent files and directories inline
within the repository structure, move them into 'spec' subdirectories
at the corresponding levels, e.g.:

  repos/base/include/spec
  repos/base/mk/spec
  repos/base/lib/mk/spec
  repos/base/src/core/spec
  ...

Moreover, this commit removes the 'platform' directories. That term was
used in an overloaded sense. All SPEC-relative 'platform' directories are
now named 'spec'. Other files, like for instance those related to the
kernel/architecture specific startup library, where moved from 'platform'
directories to explicit, more meaningful places like e.g.: 'src/lib/startup'.

Fix #1673
2015-09-16 13:58:50 +02:00
Stefan Kalkowski
eafe5e81e3 core: unify and simplify paging code (Fix #1641)
For most platforms except of NOVA a distinction between pager entrypoint
and pager activation is not needed, and only exists due to historical
reasons. Moreover, the pager thread's execution path is almost identical
between most platforms excluding NOVA, HW, and Fisco.OC. Therefore,
this commit unifies the pager loop for the other platforms, and removes
the pager activation class.
2015-08-21 10:58:59 +02:00
Norman Feske
66dd065163 sel4: use LOG console for non-core components 2015-05-26 09:40:01 +02:00
Norman Feske
3259185bfc sel4: import parent cap into non-core components 2015-05-26 09:40:01 +02:00
Norman Feske
d6e3e47348 sel4: use core_printf for non-core components
This allows us to see debug messages printed at the eary initialization
of init (before init is able to obtain the regular LOG session). This
will be reverted as soon as the initialziation of the non-core base
environment works.
2015-05-26 09:40:00 +02:00
Norman Feske
5a05521e0f sel4: bootstrap of init and page-fault handling 2015-05-26 09:40:00 +02:00
Norman Feske
f19f454ae5 sel4: move core to a libaray, add boot_modules.s 2015-05-26 09:39:59 +02:00
Norman Feske
51f02340b6 sel4: avoid superfluous header re-generation 2015-05-26 09:39:59 +02:00
Norman Feske
56ec0ad172 sel4: add base.mk lib to build and link init 2015-05-26 09:39:59 +02:00
Norman Feske
ff46d02c48 sel4: capability lifetime management 2015-05-26 09:39:59 +02:00
Norman Feske
262f52723b sel4: block on first call if Ipc_istream::_wait 2015-05-26 09:39:58 +02:00
Norman Feske
41b99a6b51 sel4: use yielding spinlock for 'Genode::Lock' 2015-05-26 09:39:58 +02:00
Norman Feske
65a74cf5e0 sel4: complement base-common.mk
This patch extends the base-common library with the symbols needed to
link core.
2015-05-26 09:39:57 +02:00
Norman Feske
c73b6e9c0d sel4: move core console to core_printf library 2015-05-26 09:39:56 +02:00
Norman Feske
e3cb8d48f7 sel4: never compile syscall-using code with -fPIC 2015-05-26 09:39:56 +02:00
Norman Feske
52c4dc8ec8 sel4: print boot info 2015-05-26 09:39:54 +02:00
Norman Feske
29f58dbd70 sel4: first syscall invokation 2015-05-26 09:39:54 +02:00
Norman Feske
2b24593758 sel4: minimalistic roottask 2015-05-26 09:39:54 +02:00
Norman Feske
456d81f517 New base-sel4 repository 2015-05-26 09:39:53 +02:00