teaching/moslab-code
2
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

l4re-base-25.08.0

Browse Source
This commit is contained in:
Viktor Reusch
2025-09-12 15:55:45 +02:00
commit d959eaab98
37938 changed files with 9382688 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
src/l4/doc/Makefile Normal file
View File

@@ -0,0 +1,9 @@
L4DIR ?= ..
TARGET = bid-spec bid-tut building-howto dev-overview l4env-concept html
TARGET = source
doc: $(TARGET)
html: bid-spec bid-tut building-howto dev-overview
include $(L4DIR)/mk/subdir.mk

BIN
src/l4/doc/source/L4Re_rgb_logo_quer_hg_h55.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 1.9 KiB

22
src/l4/doc/source/Makefile Normal file
View File

@@ -0,0 +1,22 @@
PKGDIR = .
L4DIR ?= ../..
SRC_DOX_REF = l4re.cfg
ADD_FILES_TO_HTML = $(SRC_DIR)/images/header-bg.png
include $(L4DIR)/mk/doc.mk
export L4DIR
export OBJ_BASE
PHONY += regen regen_cfg regen_html
regen: regen_cfg regen_html
regen_cfg:
doxygen -u l4re.cfg
rm -f l4re.cfg.bak
regen_html: regen_cfg
doxygen -w html l4re-header.html l4re-footer.html l4re.css l4re.cfg
rm -r l4re-footer.html.bak l4re-header.html.bak l4re.css.bak

664
src/l4/doc/source/build_system.dox Normal file
View File

@@ -0,0 +1,664 @@
// vi:ft=c
/**
\page l4re_build_system L4Re Build System
L4Re uses a custom make-based build system, often simply referred to as *BID*.
This section explains how to use BID when writing applications and libraries
for L4Re.
\section l4re_build_system_using Building L4Re
Setting up the Build Directory
------------------------------
L4Re must be built out-of-source. Therefore the first mandatory step is
creating and populating a build directory. From the root of the
L4Re source tree run
make B=<builddir>
Other targets that can be executed in the source directory are
\par update
Update the source directory from svn. Only makes sense when you have
downloaded L4Re from the official subversion repository.
\par help
Show a short help with the most important targets.
Invoking Make
-------------
Once the build directory is set up, BID make can be invoked in one of two ways:
1. Go to the build directory and invoke make without special options.
2. Go to a source directory with a BID make file and invoke
`make O=<builddir> ...`.
The default target builds the source (as you would expect),
other targets that are available in build mode are
\par cleanfast
Quickly cleans the build directory by removing all subdirectories that
contain generated files. The configuration will remain untouched.
\par clean
Remove generated files. Slower than `make cleanfast` but can be used
on selected packages. Use `S=...` to select the target package.
In addition to these targets, there are a number of targets to
generate images which are explained elsewhere.
\section l4re_build_system_writing Writing BID Make Files
The BID build system exports different roles that define what should
be done in the subdirectory. So a BID make file essentially consists
of defining the role and a number of role-dependent make
variables. The basic layout should look like this:
~~~
PKGDIR ?= <path to package's root directory> # e.g., '.' or '..'
L4DIR ?= <path to L4Re source directory> # e.g. '$(PKGDIR)/../..'
<various definitions>
include $(L4DIR)/mk/<role>.mk
~~~
`PKGDIR` in the first line defines the root directory of the current
package. `L4DIR` in the next line must be pointed to the root of the
L4Re source tree the package should be built against. After this
custom variable definitions for the role follow. In the final line
of the file, the make file with the role-specific rules must be sourced.
The following roles are currently defined:
- project.mk - Sub-project Role
- subdir.mk - Directory Role
- \subpage bid_role_prog "prog.mk - Application Role"
- lib.mk - Library Role
- \subpage bid_role_include "include.mk - Header File Role"
- doc.mk - Documentation Role
- \subpage bid_role_test "test.mk - Test Application Role"
- idl.mk - IDL File Role (currently unused)
- runux.mk - Tests in FiascoUX Role
BID-global Variables
--------------------
This section lists variables that configure how the BID build system
behaves. They are applicable for all roles.
Variable | Description
---------|----------------------
CC | C compiler for target
CXX | C++ compiler for target
HOST_CC | C compiler for host
HOST_CXX | C++ compiler for host
*/
/** \page bid_role_prog prog.mk - Application Role
The prog role is used to build executable programs.
General Configuration Variables
-------------------------------
The following variables can only be set globally for the Makefile:
\par `MODE`
Kind of target to build for. The following values are possible:
- `static` - build a statically linked binary (default)
- `shared` - build a dynamically linked binary
- `l4linux` - build a binary for running on L4Linux on the target platform
- `host` - build for host system
- `targetsys` - build a binary for the target platform with the compiler's
default settings
\par `SYSTEMS`
List of architectures the target can be built for. The entries must be
space-separated entries either naming an architecture (e.g. amd64) or
an architecture and ABI (e.g, arm-l4f). When not defined, the target
will be built for all possible platforms.
\par `TARGET`
Name or names of the binaries to compile. This variable may also be
postfixed with a specific architecture.
Target-specific Configuration Variables
---------------------------------------
The following variables may either be used with or without a description
suffix. Without suffix they will be used for all operations. With a
specific description their use is restricted to a subset.
These specifications include a target file and
the architecture, both optional but in this order, separated by
underscores. The specific variables will be used in addition to the
more general ones.
\par `SRC_C` / `SRC_CC` / `SRC_F` / `SRC_S`
.c, .cc, .f90, .S source files.
\par `REQUIRES_LIBS`
List of libraries the binary depends on. This works only with libraries
that export a pkg_config configuration file. Automatically adds any required
include and link options.
\par `DEPENDS_PKGS`
List of packages this binary depends on. If one these packages is missing
then building of the binary will be skipped.
\par `CPPFLAGS` / `CFLAGS` / `CXXFLAGS` / `FFLAGS` / `ASFLAGS`
Options for the C preprocessor, C compiler, C++ compiler, Fortran compiler
and assembler. When used with suffix, the referred element is the source file,
not the target file.
\par `LDFLAGS`
Options for the linker ld.
\par `LIBS`
Additional libraries to link against (with -l).
\par `PRIVATE_LIBDIR`
Additional directories to search for libraries.
\par `CRT0` / `CRTN`
(expert use only) Files containing custom startup and finish code.
\par `LDSCRIPT`
(expert use only) Custom link script to use.
*/
/** \page bid_role_include include.mk - Header File Role
The header file role is responsible for installing header file at the
appropriate location. The following variables can be used for customizing
the process:
\par `INCSRC_DIR`
Source directory where the headers can be found. Default is the directory
where the Makefile resides.
\par `TARGET`
List of header files to install. If left undefined, then `INCSRC_DIR` will
be scanned for files with suffix `.h` or `.i`.
Supports the specification of special filenames to allow for different source
and target filenames to be installed. The syntax is `TARGET<SRC`, where a
filename including the path of `SRC` is installed as `TARGET`. An example is
`libfoo.h<contrib/libfoo_linux.h`
which installs the header from the contrib directory under the name without that
contrib directory and without the platform specific suffix.
\par `EXTRA_TARGET`
When TARGET is undefined, then add these files to the headers found by
scanning the source directory. Has no effect if `TARGET` has been defined.
The filenames specified allow for the same rule specifications as supported by
`TARGET`.
\par `CONTRIB_HEADERS`
When set, the headers will be installed in
`${BUILDDIR}/include/contrib/${PKGNAME}`
rather than `${BUILDDIR}/include/l4/${PKGNAME}`.
\par `INSTALL_INC_PREFIX`
Base directory where to install the headers. Overwrites `CONTRIB_HEADERS`.
The headers will then be found under
`${BUILDDIR}/include/${INSTALL_INC_PREFIX}`.
\par `PC_FILENAME`
When set, a pkg_config configuration file is created with the given name.
*/
/** \page bid_role_test test.mk - Test Application Role
The test role is very similar to the application role, it also builds an
executable binary. The difference is that is also builds for each target
a test script that executes the test target either on the host (MODE=host)
or a target platform (currently only qemu).
The role accepts all make variables that are accepted by the
application role. The only difference
is that the `TARGET` variable is not required. If it is missing, the
source directory will be scanned for source files that fit the pattern
`test_*.c[c]` and create one target for each of them.
\note It is possible to still use SRC_C[C] when targets are determined
automatically. In that case the specified sources will be used
*in addition* to the main `test_*.c[c]` source.
In addition to the variables above, there are a number of variables that
control how the test is executed. All these variables may be used as
a global variable that applies to all test or, if the target name is
added as a suffix, set for a specific target only.
\par `TEST_TARGET`
Name of binary containing the test (default: same as `TARGET`).
\par `TARGET_$(ARCH)`
When TARGET is undefined, these targets are added to the list of targets for
the specified architecture. For all targets `SRC_C[C]` files must be
defined separately.
\par `TEST_KERNEL_ARGS`
Arguments to append to the kernel command line. These are also appended when
specifying custom ones via a .t-file's -f parameter or when using -d.
\par `TEST_EXPECTED`
File containing expected output.
By default the variable is empty, which means the test binary
is expected to produce TAP test output, that can be directly
processed.
When the `TEST_TAP_PLUGINS` variable is given, `TEST_EXPECTED` is ignored.
\par `TEST_EXPECTED_REPEAT`
Number of times the expected output should be repeated, by default 1.
When set to 0 then output is expected to repeat forever. This is particularly
useful to make sure that stress tests that are meant to run in an endless
loop are still alive. Note that such endless tests can only be run by
directly executing the test script. They will be skipped when run in a
test harness like `prove`.
\par `TEST_TAP_PLUGINS`
Specify the plugins that are used to process the output of the test run.
The syntax is of the values is:
plugin1:arg1=a,arg2=b plugin2:arg=foo
Multiple plugins separated by a space are loaded in order. Spaces are not
allowed inside a plugin specification. One or more arguments are optionally
passed to the plugin separated by commas and delimited by a colon.
If the variable is not specified the plugins for TAPOutput and OutputMatching
(depending on the TEST_EXPECTED variable) are automatically loaded.
For the supported plugins and their options please refer to their in-line
documentation in tool/lib/L4/TapWrapper/Plugin/. The plugin name corresponds to
the file stem name in that directory.
\par `TEST_TIMEOUT`
Non-standard timeout after which the test run is aborted
(useful for tests involving sleep).
\par `NED_CFG`
LUA configuration file for startup to give to Ned
\par `REQUIRED_MODULES`
Additional modules needed to run the test. By adding `[opts]` to the name of a
module you can add module options that are reflected in the generated
modules.list.
\par `BOOTSTRAP_ARGS`
Additional parameters to supply to bootstrap.
\par `QEMU_ARGS`
Additional parameters to supply to QEMU.
\par `MOE_ARGS`
Additional parameters to supply to moe.
\par `TEST_ARGS`
Additional arguments for the `TEST_STARTER` (tapper-wrapper per default).
\par `TEST_ROOT_TASK`
Alternative root task to be used during a test instead of moe.
\par `TEST_ROOT_TASK_ARGS`
Arguments passed to `TEST_ROOT_TASK` if `TEST_ROOT_TASK` is different from moe.
\par `KERNEL_CONF`
Features the L4Re Microkernel must have been compiled with.
A space-separated list of config options as used by
Kconfig. `run_test` looks for a `globalconfig.out` file
in the same directory as the kernel and checks that all
options are enabled. If not, the test is skipped.
Has only an effect if the `globalconfig.out` file is present.
\par `L4RE_CONF`
Features the L4Re userland must have been compiled with. A
space-separated list of config options as used by Kconfig. `run_test`
will look for these in the `.kconfig` file in the L4Re build
directory.
\par `L4LINUX_CONF`
Features the L4Linux kernel must have been compiled with.
Similar to `KERNEL_CONF` but checks for a `.config` file
in the directory of the L4Linux kernel.
\par `TEST_SETUP`
Command to execute before the test is run.
The test will only be executed if the command returns 0.
If the exit code is 69, the test is marked as skipped
with the reason provided in the final line of stdout.
\par `TEST_LOGFILE`
Append output of test execution to the given file unless
TEST_WORKDIR is given.
\par `TEST_WORKDIR`
Create logs, temp and other files below the given directory. That
directory is taken as base dir for more automatically created subdir
levels using the current test path, in order to guarantee conflict-free
usage when running many different tests with a common workdir. When
TEST_WORKDIR is provided then TEST_LOGFILE is ignored as it is
organized below workdir.
\par `TEST_TAGS`
\parblock
List of conditions for tags provided during execution of a test. A tag
can be set to 1, set to 0 or be unspecified via TEST_RUN_TAGS during
execution. Therefore there are 4 possible conditions for a tag that can
be specified in TEST_TAGS: tag, !tag, +tag and -tag. The following table
shows the conditions they represent.
|TEST_RUN_TAGS \ TEST_TAGS | tag | !tag | +tag | -tag|
|--------------------------|-----|------|------|-----|
|tag or tag=1 | y | | y | |
|unspecified | | y | y | |
|tag=0 | | y | | y|
_Example usage:_
The tag `long-running` is used by tests which take a long time and should
be skipped by default. These tests are marked with the tag long-running
unprefixed.
The tag `hardware` is set to 1 at runtime when the tests will run on real
hardware. Tests that must not run on real hardware are marked with
`!hardware`.
The tag `+impl-def` is used by tests that test implementation details.
Due to the nature of this flag we require the "+" prefix to be used, so
they are run by default but can be excluded from execution by setting
TEST_RUN_TAGS to impl-def=0 at runtime.
If you want to specify multiple tag conditions they need to be separated
with a comma.
\endparblock
\par `TEST_PLATFORM_ALLOW` and `TEST_PLATFORM_DENY`
\parblock
Deny and allow lists of platforms a test is banned from or limited to.
If you list platforms in the TEST_PLATFORM_ALLOW variable the test will
only be run on these listed platforms and will be skipped on any other
platform. If you list platforms in the TEST_PLATFORM_DENY variable the
test will be skipped on the listed platforms and will be run on any other
platform. You can only use one of these variables per test, not both.
See mk/platforms/ for the various identifiers.
_Example usage:_
# Do not run this test on the Raspberry Pi platform
TEST_PLATFORM_DENY_test_xyz := rpi
# Only run this test on this test on the RCar3 platform.
TEST_PLATFORM_ALLOW_test_abc := rcar3
\endparblock
\par `TAPARCHIVE`
Filename for an archive file to store the resulting TAP output.
In addition to compiled tests, it is also possible to create tests
where the test binary or script comes from a different source. These
tests must be listed in `EXTRA_TARGET` and for each target a
custom `TEST_TARGET` must be provided.
Running Tests
-------------
The make role creates a test script which can be found in
`<builddir>/test/t/<arch>/<api>`. It is possible to organise
the tests further in subdirectories below by specifying a
TEST_GROUP.
To be able to execute the test, a minimal test environment needs
to be set up by exporting the following environment variables:
\par `KERNEL_<arch>`, `KERNEL`
L4Re Microkernel binary to use. The test runner is able to check if the
kernel has all features necessary for the test and skip tests accordingly.
In order for this to work, the `globalconfig.out` config file from the
build directory needs to be available in the same directory as the
kernel.
\par `L4LX_KERNEL_<arch>`, `L4LX_KERNEL`
L4Linux binary to use. This is only required to run tests in
`mode=l4linux`. If no L4Linux kernel is set then these tests
will simply be skipped.
The test runner is also able to check if the kernel has all features
compiled in that are required to run the test successfully (see make
variable `L4LINUX_CONF` above). For this to work, the `.config` configuration
file from the build directory needs to be available in the same
directory as the kernel.
\par `LINUX_RAMDISK_<arch>`, `LINUX_RAMDISK`
Ramdisk to mount as root in L4Linux. This is only required to run tests in
`mode=l4linux`. If not supplied, L4Linux tests will be skipped.
The ramdisk must be set up to start the test directly after the
initial startup is finished. The name of the test binary is supplied
via the kernel command line option `l4re_testprog`. The `tool/test`
directory contains an example script `launch-l4linux-test`. which can
be copied onto the ramdisk and started by the init script.
\par `TEST_HWCONFIG` and `TEST_FIASCOCONFIG`
\parblock
Some userland tests rely on external information about the underlying platform
and the configuration of the L4Re Microkernel to decide whether or not to test
specific features or to determine which and how much resources are available.
Some examples for this are whether or not virtualization is supported by the
platform, how many cores the platform has, how many cores the kernel supports or
how much memory the platform provides. To convey this information to these tests
you can set the two environment variables `TEST_HWCONFIG` and
`TEST_FIASCOCONFIG`.
Using `TEST_HWCONFIG` requires a plain text document containing key-value
pairs separated by a `=` symbol. On top of that comment lines starting with `#`
are supported. Simply create a plain text file such as the following and set
`TEST_HWCONFIG` to its absolute path.
VIRTUALIZATION=y
MP=y
NUM_CORES=4
MEMORY=2048
Using `TEST_FIASCOCONFIG` is easier since it only needs to contain the absolute
path of the globalconfig.out file in the L4Re Microkernel's build directory. The
build system will then extract the information when a test is started.
When starting a test the build system will read both files and provide their
content as a lua table to the test. A ned script can then make decisions based
on them. To simplify some decisions the build system merges some information by
itself, e.g. virtualization is only available if both the platform and the L4Re
Microkernel support this feature. More details can be obtain from the perl
module in `tool/lib/L4/TestEnvLua.pm`.
\endparblock
In addition to these variables, the following BID variables can be
overwritten at runtime: `PT` (for the plaform type) and `TEST_TIMEOUT`.
You may also supply `QEMU_ARGS` and `MOE_ARGS` which will be appended
to the parameters specified in the BID test make file.
Once the environment is set up, the tests can be run either by simply
executing all of them from the build directory with
make test
or executing them directly, like
test/t/amd64_amdfam10/l4f/l4re-core/moe/test_namespace.t
or running one or more tests through the test harness
[prove](http://perldoc.perl.org/prove.html), like
prove test/t/amd64_amdfam10/l4f/l4re-core/moe/test_namespace.t
prove -r test/t/amd64_amdfam10/l4f/l4re-core/
prove -rv test/t/amd64_amdfam10/l4f/l4re-core/
TEST_TAGS allow for a way to include or exclude whole groups of tests
during execution, primarily with prove. You can specify which tests to
run at runtime using one of the following ways:
$ test/t/amd64_amdfam10/l4f/l4re-core/test_one.t --run-tags slow,gtest-shuffle=0
$ test/t/amd64_amdfam10/l4f/l4re-core/test_one.t -T slow,gtest-shuffle=0
$ prove -r test/t/amd64_amdfam10/l4f/l4re-core/ :: -T slow,gtest-shuffle=0
$ TEST_RUN_TAGS=slow,gtest-shuffle=0 prove -r test/t/amd64_amdfam10/l4f/l4re-core/
For each test tag requirements defined in the corresponding TEST_TAGS
Makefile variable are tested. If the requirements for tags do not match
the test is skipped. The SKIP message will provide insight why the test
was skipped:
$ make test
...
test/t/amd64_amdfam10/test_one.t .... ok
test/t/amd64_amdfam10/test_two.t .... skipped: Running this test requires tag slow to be set to 1.
test/t/amd64_amdfam10/test_three.t .. ok
When tags are provided, the tests requiring those tags are now also
executed while the tests that forbid them are skipped:
$ TEST_RUN_TAGS=slow,gtest-shuffle
$ make test
...
test/t/amd64_amdfam10/test_one.t .... ok
test/t/amd64_amdfam10/test_two.t .... ok
test/t/amd64_amdfam10/test_three.t .. skipped: Running this test requires tag gtest-shuffle to be set to 0 or not specified.
For further details on how values in TEST_TAGS and TEST_RUN_TAGS interact, see the help text for TEST_TAGS.
Running Tests in External Programs
----------------------------------
You can hand-over test execution to an external program by setting the
environment variable `EXTERNAL_TEST_STARTER` to the full path of that
program:
export EXTERNAL_TEST_STARTER=/path/to/external/test-starter
make test
\par `EXTERNAL_TEST_STARTER`
This variable is evaluated by `tool/bin/run_test` (the backend behind
`make test`) and contains the full path to the tool which actually
starts the test instead of the test itself.
The `EXTERNAL_TEST_STARTER` can be any program instead of the default
execution via `make qemu E=maketest`. Its output is taken by
`run_test` as the test output.
Usually it is just a bridge to prepare the test execution, e.g., it
could create the test as image and start that image via a simulator.
### Running Tests in a Simulator
Based on above mechanism there is a dedicated external test starter
`tool/bin/teststarter-image-telnet.pl` shipped in BID which assumes an
image to be started with another program which provides test execution
output on a network port.
This can be used to execute tests in a simulator, like this:
export EXTERNAL_TEST_STARTER=$L4RE_SRC/tool/bin/teststarter-image-telnet.pl
export SIMULATOR_START=/path/to/configured/simulator-exe
make test
After building the image and starting the simulator it contacts the
simulator via a network port (sometimes called "telnet" port) to
pass-through its execution output as its own output so it gets
captured by `run_test` as usual.
The following variables control `teststarter-image-telnet.pl`:
\par `SIMULATOR_START`
This points to the full path of the program that actually starts the
prepared test image. Most often this is the frontend script of your
simulator environment which is pre-configured so that it actually
works in the way that `teststarter-image-telnet.pl` expects from the
following settings.
\par `SIMULATOR_IMAGETYPE`
The image type to be generated via `make $SIMULATOR_IMAGETYPE
E=maketest`. Default is `elfimage`.
\par `SIMULATOR_HOST`
The simulator will be contacted via socket on that host to read its
output. Default is `localhost`.
\par `SIMULATOR_PORT`
The simulator will be contacted via socket on that port to read its
output. Default is `11111`.
\par `SIMULATOR_START_SLEEPTIME`
After starting the simulator it waits that many seconds before reading
from the port. Default is `1` (second).
Running tests without tapper-wrapper
------------------------------------
In case you want to replace the tapper-wrapper test starter, you can
replace the default one by setting the environment variable
`TEST_STARTER` to the path of your test starter. Then your test starter
can use the same environment which is normally set up for the default
starter, which includes environment variables provided by the build
system as well as the test itself. Among these are `SEARCHPATH`, `MODE`,
`ARCH`, `MOE_CFG`, `MOE_ARGS`, `TEST_TIMEOUT`, `TEST_TARGET`,
`TEST_EXPECTED`, `QEMU_ARGS` and many more.
Debugging Tests
---------------
The test script is only a thin wrapper that sets up the test
environment as it was defined in the make file and then executes
two scripts: `tapper-wrapper` and `run_test`.
The main work horse of the two is `tool/bin/run_test`. It collects
the necessary files and starts qemu to execute the test. This script
is always required.
There is then a second script wrapped around the test runner:
`tool/bin/tapper-wrapper`. This tool inspects the output of the test
runner and reformats it, so that it can be read by tools like `prove`.
If the test produces tap output, then the script scans for this output
and filters away all the debug output. If `TEST_EXPECTED` was defined,
then the script scans the output for the expected lines and prints a
suitable TAP message with success or failure. It also makes sure that
qemu is killed as soon as the test is finished.
There are a number of command-line parameters that allow to quickly
change test parameters for debugging purposes. Run the test with
'--help' for more information about available parameters.
*/

417
src/l4/doc/source/concepts.dox Normal file
View File

@@ -0,0 +1,417 @@
// vi:ft=c
/**
\page l4re_concepts Programming for L4Re
This part of the documentation discusses the concept of microkernel-based
programming in more detail. You should already have a basic understanding
of the L4Re programming environment from the tutorial.
\todo All subpages need cleaning. Level of detail here?
- \subpage l4re_concepts_ipc
- \subpage l4re_concepts_abi
- \subpage l4re_concepts_naming
- \subpage l4re_concepts_mapping
- \subpage l4re_concepts_env_and_start
- \subpage l4re_concepts_ds_rm
- \subpage l4re_concepts_stdio
- \subpage l4re_concepts_memalloc
- \subpage l4re_concepts_apps_svr
- \subpage l4re_pthreads
- tasks and threads
- communication channels
- server loops
- \subpage l4_cxx_ipc_iface
- hardware access
- \subpage l4re_build_system
\page l4re_concepts_ds_rm Memory management - Data Spaces and the Region Map
\section l4re_concept_pagers User-level paging
Memory management in L4-based systems is done by user-level applications, the
role is usually called \em pager. Tasks can give other tasks full or
restricted access rights to parts of their own memory. The kernel offers means
to give access to memory in a secure way, often referred to as *memory* mapping.
The mapping mechanism allows one task to resolve page faults of another: A
thread usually has a pager assigned to it. When the thread causes a page fault,
the kernel sends an IPC message to the pager with information about the page
fault. The pager answers this IPC by either providing a backing page, or with an
error. The kernel will map the backing page into the address space of the
faulting thread's task.
These mechanisms can be used to construct a memory and paging hierarchy among
tasks. The root of the hierarchy is `sigma0`, which initially gets all
system resources and hands them out once on a first-come-first-served basis.
Memory resources can be mapped between tasks at a page-size granularity. This
size is predetermined by the CPU's memory management unit and is commonly set
to 4 kB.
\subsection l4re_concept_data_spaces Data spaces
A data space is the L4Re abstraction for objects which may be
accessed in a memory mapped fashion (i.e., using normal memory
read and write instructions). Examples include the sections of a
binary which the loader attaches to the application's address
space, files in the ROM or on disk provided by a file server, the
registers of memory-mapped devices and anonymous memory such as
the heap or the stack.
Anonymous memory data spaces in particular (but in general all
data spaces except memory mapped IO) can either be constructed
entirely from a portion of the RAM or the current working set may
be multiplexed on some portion of the RAM. In the first case it
is possible to eagerly insert all pages (more precisely
page-frame capabilities) into the application's address space
such that no further page faults occur when this data space is
accessed. In general, however, only the pages for some
portion are provided and further pages are inserted by the pager
as a result of page faults.
\subsection l4re_concept_regions Virtual Memory Handling
The virtual memory of each task is constructed from data spaces backing
virtual memory regions (VMRs). The management of the VMRs is provided by an
object called *region map*. A dedicated region-map object is associated
with each task; it allows attaching and detaching data spaces to an address space
as well as reserving areas of virtual memory. Since the region-map object
possesses all knowledge about the virtual memory layout of a task, it also serves
as an application's default pager.
\subsection l4re_concept_mem_alloc Memory Allocation
Operating systems commonly use anonymous memory for implementing dynamic
memory allocation (e.g., using `malloc` or `new`). In an
L4Re-based system, each task gets assigned a memory allocator providing
anonymous memory using data spaces.
\see L4Re::Dataspace and L4Re::Rm.
\page l4re_concepts_naming Capabilities and Naming
The L4Re system is a capability based system which uses and offers
capabilities to implement fine-grained access control.
Generally, owning a capability means to be allowed to communicate with the
object the capability points to. All user-visible kernel objects, such as
tasks, threads, and IRQs, can only be accessed through a capability.
Please refer to the \ref l4_kernel_object_api
documentation for details. Capabilities are stored in per-task capability
tables (the object space) and are referenced by capability selectors or
object flexpages. In a simplified view, a capability selector is a natural
number indexing into the capability table of the current task.
As a matter of fact, a system designed solely based on capabilities uses
so-called 'local names' because each task can only access those objects made
available to this task. Other objects are not visible to and accessible by the
task.
\image html l4-caps-basic.png "Capabilities and Local Naming in L4"
\image latex l4-caps-basic.pdf "Capabilities and Local Naming in L4
So how does an application get access to a service?
In general all applications are started with an initial set of available
objects. This set of objects is predetermined by the creator of a new
application process and granted directly to the new task before starting
the first application thread. The application can then use these initial objects
to request access to further objects or to transfer capabilities to its own objects
to other applications. A central L4Re object for exchanging capabilities at
runtime is the name-space object, implementing a store of named capabilities.
From a security perspective, the set of initial capabilities (access rights to
objects) completely define the execution environment of an application.
Mandatory security policies can be defined by well known properties of the
initial objects and carefully handled access rights to them.
\page l4re_concepts_mapping Spaces and Mappings
Each task in the L4Re system has access to two resource spaces (three on IA32)
which are maintained by the kernel. These are the
-# object space,
-# memory space, and
-# IO-port space (only on IA32).
The entities addressed in each space are capabilities to objects, virtual memory
pages, and IO ports. The addresses are unsigned integers and the largest valid
address depends on which space is referenced, the hardware, and the
configuration of the kernel. Although a program can access memory at byte
granularity, from the kernel's point of view the address granularity in the
memory space is not bytes but pages, as determined by the hardware. The address
of a capability is also called its "capability slot".
Flexpages describe a range in any of the spaces that has a power-of-two length
and is also aligned to this length. They additionally hold access rights
information and further space specific information.
When a resource is present at some address in a task's corresponding resource
space, then we say that resource is mapped to that task. For example, a
capability to the task's main thread may be mapped to capability slot 5, or the
first page of the code segment a thread executes is mapped to virtual memory
page 12345. However, there need not be any resource mapped to an address.
Tasks can exchange resources through a process called "mapping" during IPC and
using the L4::Task::map() method. The sending task specifies a send flexpage and
the receiving task a receive flexpage. The resources mapped to the send flexpage
will then be mapped to the receive flexpage by the kernel.
Memory mappings and IO port mappings are hierarchical: If a resource of such a
type is subject of a map operation, the received mapping is a child mapping of
the corresponding mapping in the sending task (parent mapping). The kernel
usually respects the relationship between these two mappings (granting is an
exception; see below): If rights of a parent mapping are revoked using
L4::Task::unmap(), these rights are also removed from its child mappings. Also,
if a mapping is completely removed (via L4::Task::unmap() or by mapping
something else at its place), then also all child mappings are removed. In
contrast, revoking rights of a child mapping leaves the rights of its parent
mapping untouched.
The mapping of a resource can be performed as \em grant operation (see
#L4_MAP_ITEM_GRANT): Such an operation includes the removal of all involved
mappings from the send flexpage (basically a move operation). While with a map
operation without grant the mapping in the send flexpage remains the parent of
all child mappings (including the new child mapping in the receive flexpage), a
grant operation moves the mappings covered by the send flexpage to the
corresponding addresses from the receive flexpage while leaving the
parent/child relationship of the moved mappings with other mappings untouched.
During a map operation at most the access rights of the source mapping(s) can
be transferred but no additional rights can be added. So only rights that are
present in the source mapping and that are specified in the send item/flexpage
are transferred. This also holds for grant mappings, however, rights revocation
is *not* guaranteed to be applied to descendant mappings in case of grant.
There are cases where a grant operation is not or cannot be performed as
requested; see #L4_MAP_ITEM_GRANT for details.
Object capabilities are not hierarchical -- they have no children. The result
of the map operation on an object capability is a copy of that capability in
the object space of the destination task.
\page l4re_concepts_env_and_start Initial Environment and Application Bootstrapping
New applications that are started by a loader conforming to L4Re get
provided an \ref api_l4re_env. This environment
comprises a set of capabilities to initial L4Re objects that are
required to bootstrap and run this application. These
capabilities include:
- A capability to an initial memory allocator for obtaining memory in the
form of data spaces
- A capability to a factory which can be used to create additional kernel
objects
- A capability to a Vcon object for debugging output and maybe input
- A set of named capabilities to application specific objects
During the bootstrapping of the application, the loader establishes data
spaces for each individual region in the ELF binary. These include data spaces
for the code and data sections, and a data space backed with RAM for the stack
of the program's first thread.
One loader implementation is the `moe` root task. Moe usually starts an *init*
process that is responsible for coordinating the further boot
process. The default *init* process is `ned`, which implements a
script-based configuration and startup of other processes. Ned uses Lua
(http://www.lua.org) as its scripting language, see \ref l4re_servers_ned
"Ned Script example" for more details.
\section l4re_ns_config Configuring an application before startup
The default L4Re init process (Ned) provides a Lua script based configuration
of initial capabilities and application startup. Ned itself also has a set of
initial objects available that can be used to create the environment for an
application. The most important object is a kernel object factory that allows
creation of kernel objects such as IPC gates (communication channels), tasks,
threads, etc. Ned uses Lua tables (associative arrays) to represent sets of
capabilities that shall be granted to application processes.
~~~
local caps = {
name = some_capability
}
~~~
The L4 Lua package in Ned also has support functions to create application
tasks, region-map objects, etc. to start an ELF binary in a new task.
The package also contains Lua bindings for basic L4Re objects, for example, to
generic factory objects, which are used to create kernel objects and also
user-level objects provided by user-level servers.
~~~
L4.default_loader:start({ caps = { some_service = service } }, "rom/program --arg");
~~~
\section l4re_config_connection Connecting clients and servers
In general, a connection between a client and a server is represented by a
communication channel (IPC gate) that is available to both of them.
You can see the simplest connection between a client and a server
in the following example.
~~~
local loader = L4.default_loader; -- which is Moe
local svc = loader:new_channel(); -- create an IPC gate
loader:start({ caps = { service = svc:svr() }}, "rom/my_server");
loader:start({ caps = { service = svc:m("rw") }}, "rom/my_client");
~~~
As you can see in the snippet, the first action is to create a new channel
(IPC gate) using `loader:new_channel()`. The capability to the gate is stored
in the variable `svc`. Then the binary `my_server` is started in a new task,
and full (`:svr()`) access to the IPC gate is granted to the server as initial
object. The gate is accessible to the server application as "service" in the set of
its initial capabilities. Virtually in parallel a second task, running the client
application, is started and also given access to the IPC gate with less rights
(`:m("rw")`, note, this is essential). The server can now receive messages via the
IPC gate and provide some service and the client can call operations on the IPC gate
to communicate with the server.
Services that keep client specific state need to implement per-client server
objects. Usually it is the responsibility of some authority (e.g., Ned) to
request such an object from the service via a generic factory object that the
service provides initially.
~~~
local loader = L4.default_loader; -- which is Moe
local svc = loader:new_channel():m("rws"); -- create an IPC gate with rws rights
loader:start({ caps = { service = svc:svr() } }, "rom/my-service");
loader:start({ caps = { foo_service = svc:create(object_to_create, "param") }}, "rom/client");
~~~
This example is quite similar to the first one, however, the difference is that
Ned itself calls the create method on the factory object provided by the server and
passes the returned capability of that request as "foo_service" to the client process.
\note The `svc:create(..)` call blocks on the server. This means the script execution
blocks until the my-service application handles the create request.
\page l4re_concepts_stdio Program Input and Output
The initial environment provides a Vcon capability used as the standard
input/output stream. Output is usually connected to the parent of the
program and displayed as debugging output. The standard output is also used
as a back end to the C-style printf functions and the C++ streams.
Vcon services are implemented in Moe and the loader as well as by the L4Re
Microkernel and connected either to the serial line or to the screen if
available.
\see \ref l4_vcon_api
\page l4re_concepts_memalloc Initial Memory Allocator and Factory
The purpose of the memory allocator and of the factory is to provide
the application with the means to allocate memory (in the form of data spaces)
and kernel objects respectively.
An initial memory allocator and an initial factory are accessible via the
initial L4Re environment.
\see L4Re::Mem_alloc
The factory is a kernel object that provides the ability to create new
kernel objects dynamically. A factory imposes a resource limit for
kernel memory, and is thus a means to prevent denial of service attacks on
kernel resources. A factory can also be used to create new factory objects.
\see \ref l4_factory_api
\page l4re_concepts_apps_svr Application and Server Building Blocks
So far we have discussed the environment of applications in which a single
thread runs and which may invoke services provided through their initial objects.
In the following we describe some building blocks to extend the
application in various dimensions and to eventually implement a server which
implements user-level objects that may in turn be accessed by other
applications and servers.
\section l4re_concepts_app_thread Creating Additional Application Threads
To create application threads, one must allocate a stack on which
this thread may execute, create a thread kernel object and setup
the information required at startup time (instruction pointer,
stack pointer, etc.). In L4Re this functionality is encapsulated in the
pthread library.
\section l4re_concepts_service Providing a Service
In capability systems, services are typically provided by
transferring a capability to those applications that are
authorised to access the object to which the capability refers to.
Let us discuss an example to illustrate how two parties can communicate with
each other:
Assume a simple file server, which implements an interface for accessing
individual files: read(pos, buf, length) and write(pos, data, length).
L4Re provides support for building servers based on the class
L4::Server_object. L4::Server_object provides an abstract interface to be
used with the L4::Server class. Specific server objects such as, in our
case, files inherit from L4::Server_object. Let us call this class
File_object. When invoked upon receiving a message, the L4::Server will
automatically identify the corresponding server object based on the
capability that has been provided to its clients and invoke this object's
\em dispatch function with the incoming message as a parameter. Based on
this message, the server must then decide which of the protocols it
implements was invoked (if any). Usually, it will evaluate a protocol
specific opcode that clients are required to transmit as one of the first
words in the message. For example, assume our server assigns the following
opcodes: Read = 0 and Write = 1. The `dispatch` function calls the
corresponding server function (i.e., `File_object::read()` or
`File_object::write()`), which will in turn parse additional
parameters given to the function. In our case, this would be the position
and the amount of data to be read or written. In case the write function was
called the server will now update the contents of the file with the data
supplied. In case of a read it will store the requested part of the file in
the message buffer. A reply to the client finishes the client request.
*/
/* This is some text we currently do not use:
\link api_l4re_dataspace Data spaces\endlink and the purpose of the \link
api_l4re_rm Region Map\endlink are explained in more detail in the following
section.
In the L4Re Microkernel capabilities are addressed in two different
ways.
A capability can be addressed with the help of a capability
descriptor \XXX Ref which identifies the position of one single
capability in the application's address space.
The second means to address a bunch of capabilities at once are
flexpages. A flexpage describes a region of the application's
address space that is of a power 2 size and size aligned. Thus
the name flexpage. When capabilities are to be transferred (see
IPC / MapItem) the flexpage declared by the sender --- the send
flexpage --- specifies which capabilities are to be transferred.
These are at most those capabilities that are located within the
region described by the flexpage and precisely those in the
region that results from adjusting the flexpage with a possibly
smaller flexpage on the receiver side (see \XXX for more details
on how sender and receiver declared flexpages are adjusted). The
receiver declared flexpage --- the receive flexpage --- defines
where in the address space of the application capabilities are to
be received.
The key insight here is that applications are able to restrict
an invoked server such that it can only modify a part of the
applications address space --- the receive flexpage.
When invoking servers and when creating new objects one is faced
with the task to find not yet used parts in the address space of
the application at which the kernel or other servers may insert
capabilities. L4Re assists this task with the help of a capability
allocator.
*/

157
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-darkmode-toggle.js Normal file
View File

@@ -0,0 +1,157 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2021 - 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
class DoxygenAwesomeDarkModeToggle extends HTMLElement {
// SVG icons from https://fonts.google.com/icons
// Licensed under the Apache 2.0 license:
// https://www.apache.org/licenses/LICENSE-2.0.html
static lightModeIcon = `<svg xmlns="http://www.w3.org/2000/svg" enable-background="new 0 0 24 24" height="24px" viewBox="0 0 24 24" width="24px" fill="#FCBF00"><rect fill="none" height="24" width="24"/><circle cx="12" cy="12" opacity=".3" r="3"/><path d="M12,9c1.65,0,3,1.35,3,3s-1.35,3-3,3s-3-1.35-3-3S10.35,9,12,9 M12,7c-2.76,0-5,2.24-5,5s2.24,5,5,5s5-2.24,5-5 S14.76,7,12,7L12,7z M2,13l2,0c0.55,0,1-0.45,1-1s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S1.45,13,2,13z M20,13l2,0c0.55,0,1-0.45,1-1 s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S19.45,13,20,13z M11,2v2c0,0.55,0.45,1,1,1s1-0.45,1-1V2c0-0.55-0.45-1-1-1S11,1.45,11,2z M11,20v2c0,0.55,0.45,1,1,1s1-0.45,1-1v-2c0-0.55-0.45-1-1-1C11.45,19,11,19.45,11,20z M5.99,4.58c-0.39-0.39-1.03-0.39-1.41,0 c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0s0.39-1.03,0-1.41L5.99,4.58z M18.36,16.95 c-0.39-0.39-1.03-0.39-1.41,0c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0c0.39-0.39,0.39-1.03,0-1.41 L18.36,16.95z M19.42,5.99c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06c-0.39,0.39-0.39,1.03,0,1.41 s1.03,0.39,1.41,0L19.42,5.99z M7.05,18.36c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06 c-0.39,0.39-0.39,1.03,0,1.41s1.03,0.39,1.41,0L7.05,18.36z"/></svg>`
static darkModeIcon = `<svg xmlns="http://www.w3.org/2000/svg" enable-background="new 0 0 24 24" height="24px" viewBox="0 0 24 24" width="24px" fill="#FE9700"><rect fill="none" height="24" width="24"/><path d="M9.37,5.51C9.19,6.15,9.1,6.82,9.1,7.5c0,4.08,3.32,7.4,7.4,7.4c0.68,0,1.35-0.09,1.99-0.27 C17.45,17.19,14.93,19,12,19c-3.86,0-7-3.14-7-7C5,9.07,6.81,6.55,9.37,5.51z" opacity=".3"/><path d="M9.37,5.51C9.19,6.15,9.1,6.82,9.1,7.5c0,4.08,3.32,7.4,7.4,7.4c0.68,0,1.35-0.09,1.99-0.27C17.45,17.19,14.93,19,12,19 c-3.86,0-7-3.14-7-7C5,9.07,6.81,6.55,9.37,5.51z M12,3c-4.97,0-9,4.03-9,9s4.03,9,9,9s9-4.03,9-9c0-0.46-0.04-0.92-0.1-1.36 c-0.98,1.37-2.58,2.26-4.4,2.26c-2.98,0-5.4-2.42-5.4-5.4c0-1.81,0.89-3.42,2.26-4.4C12.92,3.04,12.46,3,12,3L12,3z"/></svg>`
static title = "Toggle Light/Dark Mode"
static prefersLightModeInDarkModeKey = "prefers-light-mode-in-dark-mode"
static prefersDarkModeInLightModeKey = "prefers-dark-mode-in-light-mode"
static _staticConstructor = function() {
DoxygenAwesomeDarkModeToggle.enableDarkMode(DoxygenAwesomeDarkModeToggle.userPreference)
// Update the color scheme when the browsers preference changes
// without user interaction on the website.
window.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => {
DoxygenAwesomeDarkModeToggle.onSystemPreferenceChanged()
})
// Update the color scheme when the tab is made visible again.
// It is possible that the appearance was changed in another tab
// while this tab was in the background.
document.addEventListener("visibilitychange", visibilityState => {
if (document.visibilityState === 'visible') {
DoxygenAwesomeDarkModeToggle.onSystemPreferenceChanged()
}
});
}()
static init() {
$(function() {
$(document).ready(function() {
const toggleButton = document.createElement('doxygen-awesome-dark-mode-toggle')
toggleButton.title = DoxygenAwesomeDarkModeToggle.title
toggleButton.updateIcon()
window.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => {
toggleButton.updateIcon()
})
document.addEventListener("visibilitychange", visibilityState => {
if (document.visibilityState === 'visible') {
toggleButton.updateIcon()
}
});
$(document).ready(function(){
document.getElementById("MSearchBox").parentNode.appendChild(toggleButton)
})
$(window).resize(function(){
document.getElementById("MSearchBox").parentNode.appendChild(toggleButton)
})
})
})
}
constructor() {
super();
this.onclick=this.toggleDarkMode
}
/**
* @returns `true` for dark-mode, `false` for light-mode system preference
*/
static get systemPreference() {
return window.matchMedia('(prefers-color-scheme: dark)').matches
}
/**
* @returns `true` for dark-mode, `false` for light-mode user preference
*/
static get userPreference() {
return (!DoxygenAwesomeDarkModeToggle.systemPreference && localStorage.getItem(DoxygenAwesomeDarkModeToggle.prefersDarkModeInLightModeKey)) ||
(DoxygenAwesomeDarkModeToggle.systemPreference && !localStorage.getItem(DoxygenAwesomeDarkModeToggle.prefersLightModeInDarkModeKey))
}
static set userPreference(userPreference) {
DoxygenAwesomeDarkModeToggle.darkModeEnabled = userPreference
if(!userPreference) {
if(DoxygenAwesomeDarkModeToggle.systemPreference) {
localStorage.setItem(DoxygenAwesomeDarkModeToggle.prefersLightModeInDarkModeKey, true)
} else {
localStorage.removeItem(DoxygenAwesomeDarkModeToggle.prefersDarkModeInLightModeKey)
}
} else {
if(!DoxygenAwesomeDarkModeToggle.systemPreference) {
localStorage.setItem(DoxygenAwesomeDarkModeToggle.prefersDarkModeInLightModeKey, true)
} else {
localStorage.removeItem(DoxygenAwesomeDarkModeToggle.prefersLightModeInDarkModeKey)
}
}
DoxygenAwesomeDarkModeToggle.onUserPreferenceChanged()
}
static enableDarkMode(enable) {
if(enable) {
DoxygenAwesomeDarkModeToggle.darkModeEnabled = true
document.documentElement.classList.add("dark-mode")
document.documentElement.classList.remove("light-mode")
} else {
DoxygenAwesomeDarkModeToggle.darkModeEnabled = false
document.documentElement.classList.remove("dark-mode")
document.documentElement.classList.add("light-mode")
}
}
static onSystemPreferenceChanged() {
DoxygenAwesomeDarkModeToggle.darkModeEnabled = DoxygenAwesomeDarkModeToggle.userPreference
DoxygenAwesomeDarkModeToggle.enableDarkMode(DoxygenAwesomeDarkModeToggle.darkModeEnabled)
}
static onUserPreferenceChanged() {
DoxygenAwesomeDarkModeToggle.enableDarkMode(DoxygenAwesomeDarkModeToggle.darkModeEnabled)
}
toggleDarkMode() {
DoxygenAwesomeDarkModeToggle.userPreference = !DoxygenAwesomeDarkModeToggle.userPreference
this.updateIcon()
}
updateIcon() {
if(DoxygenAwesomeDarkModeToggle.darkModeEnabled) {
this.innerHTML = DoxygenAwesomeDarkModeToggle.darkModeIcon
} else {
this.innerHTML = DoxygenAwesomeDarkModeToggle.lightModeIcon
}
}
}
customElements.define("doxygen-awesome-dark-mode-toggle", DoxygenAwesomeDarkModeToggle);

85
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-fragment-copy-button.js Normal file
View File

@@ -0,0 +1,85 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2022 - 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
class DoxygenAwesomeFragmentCopyButton extends HTMLElement {
constructor() {
super();
this.onclick=this.copyContent
}
static title = "Copy to clipboard"
static copyIcon = `<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" width="24" height="24"><path d="M0 0h24v24H0V0z" fill="none"/><path d="M16 1H4c-1.1 0-2 .9-2 2v14h2V3h12V1zm3 4H8c-1.1 0-2 .9-2 2v14c0 1.1.9 2 2 2h11c1.1 0 2-.9 2-2V7c0-1.1-.9-2-2-2zm0 16H8V7h11v14z"/></svg>`
static successIcon = `<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" width="24" height="24"><path d="M0 0h24v24H0V0z" fill="none"/><path d="M9 16.17L4.83 12l-1.42 1.41L9 19 21 7l-1.41-1.41L9 16.17z"/></svg>`
static successDuration = 980
static init() {
$(function() {
$(document).ready(function() {
if(navigator.clipboard) {
const fragments = document.getElementsByClassName("fragment")
for(const fragment of fragments) {
const fragmentWrapper = document.createElement("div")
fragmentWrapper.className = "doxygen-awesome-fragment-wrapper"
const fragmentCopyButton = document.createElement("doxygen-awesome-fragment-copy-button")
fragmentCopyButton.innerHTML = DoxygenAwesomeFragmentCopyButton.copyIcon
fragmentCopyButton.title = DoxygenAwesomeFragmentCopyButton.title
fragment.parentNode.replaceChild(fragmentWrapper, fragment)
fragmentWrapper.appendChild(fragment)
fragmentWrapper.appendChild(fragmentCopyButton)
}
}
})
})
}
copyContent() {
const content = this.previousSibling.cloneNode(true)
// filter out line number from file listings
content.querySelectorAll(".lineno, .ttc").forEach((node) => {
node.remove()
})
let textContent = content.textContent
// remove trailing newlines that appear in file listings
let numberOfTrailingNewlines = 0
while(textContent.charAt(textContent.length - (numberOfTrailingNewlines + 1)) == '\n') {
numberOfTrailingNewlines++;
}
textContent = textContent.substring(0, textContent.length - numberOfTrailingNewlines)
navigator.clipboard.writeText(textContent);
this.classList.add("success")
this.innerHTML = DoxygenAwesomeFragmentCopyButton.successIcon
window.setTimeout(() => {
this.classList.remove("success")
this.innerHTML = DoxygenAwesomeFragmentCopyButton.copyIcon
}, DoxygenAwesomeFragmentCopyButton.successDuration);
}
}
customElements.define("doxygen-awesome-fragment-copy-button", DoxygenAwesomeFragmentCopyButton)

81
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-interactive-toc.js Normal file
View File

@@ -0,0 +1,81 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2022 - 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
class DoxygenAwesomeInteractiveToc {
static topOffset = 38
static hideMobileMenu = true
static headers = []
static init() {
window.addEventListener("load", () => {
let toc = document.querySelector(".contents > .toc")
if(toc) {
toc.classList.add("interactive")
if(!DoxygenAwesomeInteractiveToc.hideMobileMenu) {
toc.classList.add("open")
}
document.querySelector(".contents > .toc > h3")?.addEventListener("click", () => {
if(toc.classList.contains("open")) {
toc.classList.remove("open")
} else {
toc.classList.add("open")
}
})
document.querySelectorAll(".contents > .toc > ul a").forEach((node) => {
let id = node.getAttribute("href").substring(1)
DoxygenAwesomeInteractiveToc.headers.push({
node: node,
headerNode: document.getElementById(id)
})
document.getElementById("doc-content")?.addEventListener("scroll", () => {
DoxygenAwesomeInteractiveToc.update()
})
})
DoxygenAwesomeInteractiveToc.update()
}
})
}
static update() {
let active = DoxygenAwesomeInteractiveToc.headers[0]?.node
DoxygenAwesomeInteractiveToc.headers.forEach((header) => {
let position = header.headerNode.getBoundingClientRect().top
header.node.classList.remove("active")
header.node.classList.remove("aboveActive")
if(position < DoxygenAwesomeInteractiveToc.topOffset) {
active = header.node
active?.classList.add("aboveActive")
}
})
active?.classList.add("active")
active?.classList.remove("aboveActive")
}
}

51
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-paragraph-link.js Normal file
View File

@@ -0,0 +1,51 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2022 - 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
class DoxygenAwesomeParagraphLink {
// Icon from https://fonts.google.com/icons
// Licensed under the Apache 2.0 license:
// https://www.apache.org/licenses/LICENSE-2.0.html
static icon = `<svg xmlns="http://www.w3.org/2000/svg" height="20px" viewBox="0 0 24 24" width="20px"><path d="M0 0h24v24H0V0z" fill="none"/><path d="M17 7h-4v2h4c1.65 0 3 1.35 3 3s-1.35 3-3 3h-4v2h4c2.76 0 5-2.24 5-5s-2.24-5-5-5zm-6 8H7c-1.65 0-3-1.35-3-3s1.35-3 3-3h4V7H7c-2.76 0-5 2.24-5 5s2.24 5 5 5h4v-2zm-3-4h8v2H8z"/></svg>`
static title = "Permanent Link"
static init() {
$(function() {
$(document).ready(function() {
document.querySelectorAll(".contents a.anchor[id], .contents .groupheader > a[id]").forEach((node) => {
let anchorlink = document.createElement("a")
anchorlink.setAttribute("href", `#${node.getAttribute("id")}`)
anchorlink.setAttribute("title", DoxygenAwesomeParagraphLink.title)
anchorlink.classList.add("anchorlink")
node.classList.add("anchor")
anchorlink.innerHTML = DoxygenAwesomeParagraphLink.icon
node.parentElement.appendChild(anchorlink)
})
})
})
}
}

40
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-sidebar-only-darkmode-toggle.css Normal file
View File

@@ -0,0 +1,40 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2021 - 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
@media screen and (min-width: 768px) {
#MSearchBox {
width: calc(var(--side-nav-fixed-width) - calc(2 * var(--spacing-medium)) - var(--searchbar-height) - 1px);
}
#MSearchField {
width: calc(var(--side-nav-fixed-width) - calc(2 * var(--spacing-medium)) - 66px - var(--searchbar-height));
}
}

116
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-sidebar-only.css Normal file
View File

@@ -0,0 +1,116 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2021 - 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
html {
/* side nav width. MUST be = `TREEVIEW_WIDTH`.
* Make sure it is wide enough to contain the page title (logo + title + version)
*/
--side-nav-fixed-width: 335px;
--menu-display: none;
--top-height: 120px;
--toc-sticky-top: -25px;
--toc-max-height: calc(100vh - 2 * var(--spacing-medium) - 25px);
}
#projectname {
white-space: nowrap;
}
@media screen and (min-width: 768px) {
html {
--searchbar-background: var(--page-background-color);
}
#side-nav {
min-width: var(--side-nav-fixed-width);
max-width: var(--side-nav-fixed-width);
top: var(--top-height);
overflow: visible;
}
#nav-tree, #side-nav {
height: calc(100vh - var(--top-height)) !important;
}
#nav-tree {
padding: 0;
}
#top {
display: block;
border-bottom: none;
height: var(--top-height);
margin-bottom: calc(0px - var(--top-height));
max-width: var(--side-nav-fixed-width);
overflow: hidden;
background: var(--side-nav-background);
}
#main-nav {
float: left;
padding-right: 0;
}
.ui-resizable-handle {
cursor: default;
width: 1px !important;
background: var(--separator-color);
box-shadow: 0 calc(-2 * var(--top-height)) 0 0 var(--separator-color);
}
#nav-path {
position: fixed;
right: 0;
left: var(--side-nav-fixed-width);
bottom: 0;
width: auto;
}
#doc-content {
height: calc(100vh - 31px) !important;
padding-bottom: calc(3 * var(--spacing-large));
padding-top: calc(var(--top-height) - 80px);
box-sizing: border-box;
margin-left: var(--side-nav-fixed-width) !important;
}
#MSearchBox {
width: calc(var(--side-nav-fixed-width) - calc(2 * var(--spacing-medium)));
}
#MSearchField {
width: calc(var(--side-nav-fixed-width) - calc(2 * var(--spacing-medium)) - 65px);
}
#MSearchResultsWindow {
left: var(--spacing-medium) !important;
right: auto;
}
}

90
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome-tabs.js Normal file
View File

@@ -0,0 +1,90 @@
/**
Doxygen Awesome
https://github.com/jothepro/doxygen-awesome-css
MIT License
Copyright (c) 2023 jothepro
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/
class DoxygenAwesomeTabs {
static init() {
window.addEventListener("load", () => {
document.querySelectorAll(".tabbed:not(:empty)").forEach((tabbed, tabbedIndex) => {
let tabLinkList = []
tabbed.querySelectorAll(":scope > ul > li").forEach((tab, tabIndex) => {
tab.id = "tab_" + tabbedIndex + "_" + tabIndex
let header = tab.querySelector(".tab-title")
let tabLink = document.createElement("button")
tabLink.classList.add("tab-button")
tabLink.appendChild(header)
header.title = header.textContent
tabLink.addEventListener("click", () => {
tabbed.querySelectorAll(":scope > ul > li").forEach((tab) => {
tab.classList.remove("selected")
})
tabLinkList.forEach((tabLink) => {
tabLink.classList.remove("active")
})
tab.classList.add("selected")
tabLink.classList.add("active")
})
tabLinkList.push(tabLink)
if(tabIndex == 0) {
tab.classList.add("selected")
tabLink.classList.add("active")
}
})
let tabsOverview = document.createElement("div")
tabsOverview.classList.add("tabs-overview")
let tabsOverviewContainer = document.createElement("div")
tabsOverviewContainer.classList.add("tabs-overview-container")
tabLinkList.forEach((tabLink) => {
tabsOverview.appendChild(tabLink)
})
tabsOverviewContainer.appendChild(tabsOverview)
tabbed.before(tabsOverviewContainer)
function resize() {
let maxTabHeight = 0
tabbed.querySelectorAll(":scope > ul > li").forEach((tab, tabIndex) => {
let visibility = tab.style.display
tab.style.display = "block"
maxTabHeight = Math.max(tab.offsetHeight, maxTabHeight)
tab.style.display = visibility
})
tabbed.style.height = `${maxTabHeight + 10}px`
}
resize()
new ResizeObserver(resize).observe(tabbed)
})
})
}
static resize(tabbed) {
}
}

2677
src/l4/doc/source/doxygen-awesome-css/doxygen-awesome.css Normal file
View File

File diff suppressed because it is too large Load Diff

23
src/l4/doc/source/images/Makefile Normal file
View File

@@ -0,0 +1,23 @@
INKSCAPE ?= inkscape
PNGWIDTH ?= 640
PNGOPTS ?= --export-area-drawing
PDFOPTS ?= --export-text-to-path
IMAGES := l4-caps-basic l4re-basic io-overview
SVG_PATH ?= ../../../../doc/l4-clipart
vpath %.svg $(SVG_PATH)
PDF_IMAGES := $(addsuffix .pdf,$(IMAGES))
PNG_IMAGES := $(addsuffix .png,$(IMAGES))
all: $(PDF_IMAGES) $(PNG_IMAGES)
%.png: %.svg
$(INKSCAPE) $(PNGOPTS) --export-width=$(PNGWIDTH) --export-png=$@ -f $<
%.pdf: %.svg
$(INKSCAPE) $(PDFOPTS) -A $@ -f $<

BIN
src/l4/doc/source/images/header-bg.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 715 B

BIN
src/l4/doc/source/images/io-overview.pdf Normal file
View File

Binary file not shown.

BIN
src/l4/doc/source/images/io-overview.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 47 KiB

BIN
src/l4/doc/source/images/l4-caps-basic.pdf Normal file
View File

Binary file not shown.

BIN
src/l4/doc/source/images/l4-caps-basic.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 26 KiB

BIN
src/l4/doc/source/images/l4re-basic.pdf Normal file
View File

Binary file not shown.

BIN
src/l4/doc/source/images/l4re-basic.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 27 KiB

165
src/l4/doc/source/intro.dox Normal file
View File

@@ -0,0 +1,165 @@
// vi:set ft=c: -*- Mode: C -*-
/**
\mainpage Overview
Welcome to the documentation of the %L4Re Operating System Framework, or %L4Re
for short. There are two parts to this documentation: a user manual, which
provides a birds eye view of %L4Re and its environment, and a reference
section which documents the complete programming API.
### User Manual #####
1. \ref l4re_intro shortly explains the concept of microkernels and
introduces the basic terminology.
2. \ref l4re_tutorial helps you getting started with setting up
the development environment and writing your own first %L4Re application.
3. \ref l4re_concepts explains in detail the most important
programming concepts.
4. \ref l4re_servers provides a quick overview over standard services running
on the %L4Re operating system.
### Reference #####
The second part provides the complete reference of all classes and functions
of the %L4Re Operating System Framework as well as a list of example code.
*/
/**
\page l4re_intro Introduction
The intention of this section is to provide a short overview about the
L4Re Operating System Framework. The general structure of a
microkernel-based system will be introduced and the principal functionality
of the servers in the basic environment outlined.
\section fiasco_intro L4Re Microkernel
The L4Re Microkernel is the lowest-level component of software running in an
L4Re-based system. The microkernel is the only component that runs in privileged
processor mode. It does not include complex services such as program loading,
device drivers, or file systems; those are implemented in user-level programs on
top of it (a basic set of these services and abstractions is provided by the L4
Runtime Environment).
Microkernel services are implemented in kernel objects. Tasks hold
references to kernel objects in their respective \em "object space", which is a
kernel-protected table.
These references are called \em capabilities. System calls to the microkernel are function
invocations on kernel objects through the corresponding capabilities. These
can be thought of as function invocations on object references in an
object-oriented programming environment. Furthermore, if a task owns a
capability, it may grant other tasks the same (or fewer) rights on this object
by passing the capability from its own to the other task's object space.
From a design perspective, capabilities are a concept that enables flexibility
in the system structure. A thread that invokes an object through a capability
does not need to care about where this object is implemented. In fact, it is
possible to implement all objects either in the kernel or in a user-level
server and replace one implementation with the other transparently for clients.
\subsection l4re_concepts_fiasco_ipc Communication
The basic communication mechanism in L4-based systems is called
\em "Inter Process Communication (IPC)". It is always synchronous, i.e. both
communication partners need to actively rendezvous for IPC. In addition to
transmitting arbitrary data between threads, IPC is also used to resolve
hardware exceptions, faults and for virtual memory management.
\subsection l4re_concepts_fiasco_kobjects Kernel Objects
The following list gives a short overview of the kernel objects provided by
the L4Re Microkernel:
\li <b>Task</b> A task comprises a memory address space (represented by the
task's page table), an object space (holding the kernel protected
capabilities), and on x86 an IO-port address space.
\li <b>Thread</b> A thread is bound to a task and executes code. Multiple
threads can coexist in one task and are scheduled by the microkernel's scheduler.
\li <b>Factory</b> A factory is used by applications to create new kernel
objects. Access to a factory is required to create any new kernel object.
Factories can control and restrict object creation.
\li <b>IPC Gate</b> An IPC gate is used to create a secure communication
channel between different tasks. It embeds a label (kernel protected payload)
that securely identifies the gate through which a message is received.
The gate label is not visible to and cannot be altered by the sender.
\li <b>IRQ</b> IRQ objects provide access to hardware interrupts. Additionally,
programs can create new virtual interrupt objects and trigger them. This
allows to implement a signaling mechanism. The receiver cannot decide whether
the interrupt is a physical or virtual one.
\li <b>Vcon</b> Provides access to the in-kernel debugging console (input and output).
There is only one such object in the kernel and it is only available, if the
kernel is built with debugging enabled. This object is typically interposed
through a user-level service or without debugging in the kernel can be
completely based on user-level services.
\li <b>Scheduler</b> Implements scheduling policy and assignment of threads
to CPUs, including CPU statistics.
\section l4re_system_structure L4Re System Structure
The system has a multi-tier architecture consisting of the
following layers depicted in the figure below:
\li <b>Microkernel</b> The microkernel is the component at the lowest level of
the software stack. It is the only piece of software that is running in the
privileged mode of the processor.
\li <b>Tasks</b> Tasks are the basic containers (address spaces) in which system
services and applications are executed. They run in the processor's deprivileged
user mode.
\image html l4re-basic.png "Basic Structure of an L4Re based system"
\image latex l4re-basic.pdf "Basic Structure of an L4Re based system"
In terms of functionality, the system is structured as follows:
\li <b>Microkernel</b> The kernel provides primitives to execute programs in tasks,
to enforce isolation among them, and to provide means of secure communication in
order to let them cooperate. As the kernel is the most privileged, security-critical
software component in the system, it is a general design goal to make it as small
as possible in order to reduce its attack surface. It provides only a minimal set of
mechanisms that are necessary to support applications.
\li <b>Runtime Environment</b> The small kernel offers a concise set of interfaces,
but these are not necessarily suited for building applications directly on top of
it. The L4Re Runtime Environment aims at providing more convenient abstractions for
application development. It comprises low-level software components that interface
directly with the microkernel. The root pager \em sigma0 and the root task \em Moe
are the most basic components of the L4Re Runtime Environment. Other
services (e.g., for device enumeration) use interfaces provided by them.
\li \b Applications Applications run on top of the system and use services
provided by the runtime environment -- or by other applications. There may be
several types of applications in the system and even virtual machine monitors
and device drivers are considered applications in the terminology used in this
document. They are running alongside other applications on the system.
Lending terminology from the distributed systems area, applications offering
services to other applications are usually called \em servers, whereas
applications using those services are named \em clients. Being in both
roles is also common, for instance, a file system server may be viewed as a
server with respect to clients using the file system, while the server itself
may also act as a client of a hard disk driver.
\section main_l4re_sec L4Re Runtime Environment
The L4Re Runtime Environment provides a basic set of services and
abstractions, which are useful to implement and run user-level applications on
top of the L4Re Microkernel. They form the L4Re Operating System Framework.
The L4Re Operating System Framework consists of a set of libraries and
servers. L4Re follows an object-oriented design. Server interfaces are
object-oriented, and the implementation is also object-oriented.
A minimal L4Re-based application needs 3 components to be booted beforehand:
the L4Re Microkernel, the root pager (Sigma0), and the root task (Moe). The
Sigma0 root pager initially owns all system resources, but is usually used
only to resolve page faults for the Moe root task. Moe provides the essential
services to normal user applications such as an initial program loader, a
region-map service for virtual memory management, and a memory (data space)
allocator.
*/

444
src/l4/doc/source/l4_abi.dox Normal file
View File

@@ -0,0 +1,444 @@
// vi:set ft=c: -*- Mode: C -*-
/**
\page l4re_concepts_abi Kernel ABI
This section details the binary representation of the IPC interface of the
kernel. It accompanies the [L4 Inter-Process Communication
(IPC)](#l4re_concepts_ipc) section. The details presented here are usually not
relevant when developing %L4Re applications and can therefore be skipped by many
readers.
\note The kernel ABI is subject to change. Please use the API instead of relying
on particular binary representations.
The following notation is used to indicate how particular data fields are used:
- [in]: The kernel reads and interprets this field.
- [out]: The kernel writes this field with information provided by the kernel.
- [cpy]: The kernel copies this field from sender to receiver (without
interpretation if [in] is not listed as well).
The above indications may be combined.
\section l4re_concepts_abi_capsel Capability selector and flags
See [partner capability selector](#l4re_concepts_descr_capidx) and [IPC
flags](#l4re_concepts_descr_flags).
The kernel reads and interprets all the fields ([in]).
MSB 12 11 10 [7] 4 3 2 1 0 bits
┌───────────┬─────────┬─────────┬─────────┬─────────┬─────────┬─────────┐
│ [in] │ [in] │ │ [in] │ [in] │ [in] │ [in] │
│(see below)│ special │ SBZ │ reply │open wait│ recv │ send │
└───────────┴─────────┴─────────┴─────────┴─────────┴─────────┴─────────┘
┌───────────┬─────────┬─
│ cap idx │ 0 │ if special is 0
└───────────┴─────────┴─
┌───────────┬─────────┬─
│ 1...1 │ 1 │ if special is 1
└───────────┴─────────┴─
- Bits 0…3 [in]: These bits correspond to the flags defined in
#l4_syscall_flags_t. The individual bits correspond to #L4_SYSF_REPLY,
#L4_SYSF_OPEN_WAIT, #L4_SYSF_RECV, #L4_SYSF_SEND. Note that not all
combinations of those bits are defined; see #l4_syscall_flags_t.
- Bits 4…10 [in] `SBZ`: should be zero
- Bit 11 [in] `special`: Set when using #L4_INVALID_CAP, otherwise unset.
- Bits 12…MSB [in]: Capability index if `special` is unset, otherwise all those
bits should be one (see #L4_INVALID_CAP, [partner capability
selector](#l4re_concepts_descr_capidx) and #l4_cap_idx_t).
\section l4re_concepts_abi_label Label
See [IPC label](#l4re_concepts_descr_label).
When IPC is sent via a thread capability, the label is copied to the receiver
unchanged ([cpy]).
When IPC is sent via an IPC gate, the sent label is ignored and the kernel
provides the bitwise OR (`|`) of the IPC gate label and the sender’s write and
special permissions (see #L4_CAP_FPAGE_W and #L4_CAP_FPAGE_S) of the used
capability ([out]):
MSB 2 1 0 bits
┌───────────────────┬─────────────────┬─────────────────┐
│ [out] │ [out] │ [out] │
│ label │ label | special │ label | write │
│ │ right │ right │
└───────────────────┴─────────────────┴─────────────────┘
\section l4re_concepts_abi_msgtag Message tag
See [IPC message tag](#l4re_concepts_descr_msgtag). Note that, for a message tag
returned by the kernel, if the error flag is set, all other contents of the
message tag is undefined.
MSB 16 15 14 13 12 11 [6] 6 5 [6] 0 bits
┌─────────────────┬──────────┬──────────┬──────────┬──────────┬─────────────┬─────────────┐
│ [cpy] │ [out] │ │ [in,cpy] │ [in,cpy] │ [in,cpy] │ [in,cpy] │
│ payload │ error │ SBZ │ schedule │ transfer │ items │ words │
│ │ flag │ │ flag │ FPU flag │ │ │
└─────────────────┴──────────┴──────────┴──────────┴──────────┴─────────────┴─────────────┘
- Bits 0…5 [in,cpy] `words`: Number of (untyped) message words in the UTCB’s
message registers. See #l4_msgtag_words() and #l4_msgtag_t::words().
- Bits 6…11 [in,cpy] `items`: Number of typed message items in the UTCB’s
message registers. See #l4_msgtag_items() and #l4_msgtag_t::items().
- Bit 12 [in,cpy] `transfer FPU flag`: See #L4_MSGTAG_TRANSFER_FPU.
- Bit 13 [in,cpy] `schedule flag`: See #L4_MSGTAG_SCHEDULE.
- Bit 14 `SBZ`: should be zero
- Bit 15 [out] `error`: See #L4_MSGTAG_ERROR, #l4_msgtag_has_error() and
#l4_msgtag_t::has_error().
- Bits 16…MSB [cpy] `payload`: Transferred to receiver unchanged; not
interpreted by kernel (unless it is the communication partner). For IPC calls
or send-only IPC, this is usually the protocol. For replies, this is usually
used for return values and server error signaling. See #l4_msgtag_label() and
#l4_msgtag_t::label().
\section l4re_concepts_abi_timeouts Timeouts
See [IPC timeouts](#l4re_concepts_descr_timeouts) and #l4_timeout_t.
The kernel reads and interprets all the fields ([in]).
31 [16] 16 15 [16] 0 bits
┌─────────────────┬─────────────────┐
│ [in] │ [in] │
│ send timeout │ receive timeout │
└─────────────────┴─────────────────┘
A timeout has the following format. There are two special timeout values:
- *Zero timeout:* Only bit 10 is set. See #L4_IPC_TIMEOUT_0.
15 [5] 11 10 9 [10] 0 bits
┌───────────┬─────┬──────────────────────┐
│ 0 │ 1 │ 0 │
└───────────┴─────┴──────────────────────┘
- *Infinite timeout:* All bits are unset. See #L4_IPC_TIMEOUT_NEVER.
15 [16] 0 bits
┌────────────────────────────────────────┐
│ 0 │
└────────────────────────────────────────┘
Otherwise, the timeout is either relative or absolute, which is specified by
bit 15.
- *Relative timeout:* If bit 15 is unset, the timeout is `mantissa * 2 ^
exponent` micro seconds relative to the current time. The `mantissa` must not
be zero:
15 14 [5] 10 9 [10] 0 bits
┌─────┬───────────┬──────────────────────┐
│ 0 │ exponent │ mantissa ≠ 0 │
└─────┴───────────┴──────────────────────┘
- *Absolute timeout:* If bit 15 is set, an absolute timeout is specified in the
UTCB’s buffer registers starting at `buf reg idx` (the particular number of
registers depends on the architecture; see #l4_timeout_s):
15 14 [9] 6 5 [6] 0 bits
┌─────┬────────────────────┬─────────────┐
│ 1 │ SBZ │ buf reg idx │
└─────┴────────────────────┴─────────────┘
\section l4re_concepts_abi_utcb User-level thread control block (UTCB)
See [User-level thread control block (UTCB)](#l4re_concepts_descr_utcb).
l4_utcb_mr() l4_utcb_br() l4_utcb_tcr()
l4_msg_regs_t l4_buf_regs_t l4_thread_regs_t
┌─────────────────┐ ┌────────┐ ┌───────────────────────────┐ ┌───────────────────────────────────┐
0 [63] 62 63 64 65 [58] 122 123 124 125 [3] 128 words
┌───────────────────┬──────────┬──────────┬──────────────────┬──────────┬──────────┬───────────────┐
│ │ [(out)] │ [in] │ [in] │ [out] │ [(out)] │ │
│ message registers │ arch │ BDR │ buffer registers │ error │ free │ thread‐local │
│ (MRs) │ specific │ │ (BRs) │ code │ marker │ storage (TLS) │
└───────────────────┴──────────┴──────────┴──────────────────┴──────────┴──────────┴───────────────┘
│ └────────────────────┐
│0 [words] [2 * items] 62│ words
┌───────────────┬───────────────┬────────┐
│ [cpy] │ [in,out] │ │
│ (untyped) │ typed │ unused │
│ message words │ message items │ │
└───────────────┴───────────────┴────────┘
- Words 0…62 `MRs`: See [IPC Message registers](#l4re_concepts_descr_mrs) and
#l4_utcb_mr(). The number of message registers is defined by
#L4_UTCB_GENERIC_DATA_SIZE. The actually used message registers are defined by
`words` and `items` in the [message tag](#l4re_concepts_abi_msgtag). The
layout of a typed message item varies depending on being an input or output
value, see [typed message items](#l4re_concepts_abi_items).
- Word 63 [(out)]: Depending on the architecture, this word may be used by the
kernel to signify the position of a thread’s UTCB in memory. See
architecture-specific implementation of #l4_utcb(). If at all, the kernel
writes this word when kernel-user memory is set up as UTCB while binding a
thread to a task; see #l4_thread_control_bind(), #L4::Thread::Attr::bind().
- Word 64 [in] `BDR`: See [buffer descriptor
register](#l4re_concepts_abi_utcb_bdr).
- Words 65…122 [in] `BRs`: See [IPC Buffer Registers](#l4re_concepts_descr_brs),
[receive items](#l4re_concepts_abi_items_receive) and
#l4_utcb_br()->[br](#l4_buf_regs_t::br). The number of buffer registers is
defined by #L4_UTCB_GENERIC_BUFFERS_SIZE.
- Word 123 [out] `error code`: See [IPC Thread Control
Registers](#l4re_concepts_descr_tcrs) and
#l4_utcb_tcr()->[error](#l4_thread_regs_t::error).
- Word 124 [(out)] `free marker`: Written by the kernel, but not necessarily
during IPC. See [IPC Thread Control Registers](#l4re_concepts_descr_tcrs) and
#l4_utcb_tcr()->[free_marker](#l4_thread_regs_t::free_marker).
- Word 125…128 `TLS`: Ignored and left untouched by the kernel. See [IPC Thread
Control Registers](#l4re_concepts_descr_tcrs) and
#l4_utcb_tcr()->[user](#l4_thread_regs_t::user).
\subsection l4re_concepts_abi_utcb_bdr Buffer descriptor register
See [IPC Buffer Descriptor Register](#l4re_concepts_descr_bdr) and
#l4_utcb_br()->[bdr](#l4_buf_regs_t::bdr).
MSB 25 24 23 [9] 15 14 [5] 10 9 [5] 5 4 [5] 0 bits
┌───────────┬──────────┬───────────┬────────────────┬────────────────┬────────────────┐
│ SBZ │ inherit │ SBZ │ index of first │ index of first │ index of first │
│ │ FPU flag │ │ obj cap buffer │ io buffer │ memory buffer │
└───────────┴──────────┴───────────┴────────────────┴────────────────┴────────────────┘
\section l4re_concepts_abi_items Typed message items
The number of words in a typed message item varies depending on the particular
kind of item. However, for the first word, the following properties are shared:
- *Void item:* If all bits of the first word of a typed message item are zero,
then it is a void item.
- *Non-void item:* The first word of a non-void typed message item has the
following binary layout:
MSB 4 3 2 0 bits
┌────────────────────────────┬───┬────────┐
│ │ t │ │
└────────────────────────────┴───┴────────┘
Bit 3 (`t`) is the type bit. If `t` is set, the item is a map item. Currently,
map item is the only supported type. Hence, this bit must be set for all items
except for void items.
There are three sub-types of typed message items: *send items*, *receive items*,
and *return items*; see [Message Items](#l4_msgitem_api).
Many typed items make use of flexpages, therefore, these are described before
the various kinds of typed items. Note that flexpages are also used outside of
typed message items, e.g., for #L4::Task::unmap().
\subsection l4re_concepts_abi_items_flexpages Flexpages
A flexpage consists of a single word and, except for some special values,
describes a range in an address space, see [flex pages](#l4_fpage_api).
The general layout is defined as follows:
MSB 6 5 [2] 4 3 [4] 0 bits
┌───────────────────────────────────┬─────────┬─────────────┐
│ │ type │ │
└───────────────────────────────────┴─────────┴─────────────┘
- Bits 4…5 `type`: See #l4_fpage_type() and #L4_fpage_type.
The type #L4_FPAGE_SPECIAL only supports some selected values, which are only
supported for selected interfaces; see #L4_FPAGE_SPECIAL.
The other types share the same layout:
MSB 12 11 [6] 6 5 [2] 4 3 [4] 0 bits
┌─────────────────┬─────────────────┬─────────┬─────────────┐
│ start │ order │ type │ permissions │
└─────────────────┴─────────────────┴─────────┴─────────────┘
- Bits 0…3 `permissions`: See #l4_fpage_rights(), #L4_fpage_rights (memory space)
and #L4_cap_fpage_rights (object space). Should be zero for I/O port space.
- Bits 6…11 `order`: The log₂ size of the flexpage. See #l4_fpage_size.
- Bits 12…MSB `start`: The starting page number / I/O port number / capability
index of the flexpage. Must be aligned to the flexpage size. See
#l4_fpage_page(), #l4_fpage_memaddr(), #l4_fpage_ioport() and #l4_fpage_obj().
Also see #l4_fpage() (memory space), #l4_iofpage() (I/O port space) and
#l4_fpage_obj() (object space).
\subsection l4re_concepts_abi_items_send Send items
A send item consists of two words. The second word of a non-void send item is a
[flexpage](#l4re_concepts_abi_items_flexpages). The type of the flexpage
determines the interpretation of the `attr` bits in the first word (see below).
If not void, the layout of the first word is defined as follows:
first word second word
MSB 12 11 8 7 4 3 2 1 0 bits
┌──────────┬─────┬──────┬───┬─────┬───────┬──────────┐┌───────────────┐
│ hot_spot │ SBZ │ attr │ 1 │ SBZ │ grant │ compound ││ send flexpage │
└──────────┴─────┴──────┴───┴─────┴───────┴──────────┘└───────────────┘
`SBZ` means “should be zero”.
- Bit 0 (`compound`): Compound bit. See #L4_ITEM_CONT and
#L4::Ipc::Snd_fpage::is_compound().
- Bit 1 (`grant`): Grant flag. See #L4_ITEM_MAP, #L4_MAP_ITEM_GRANT and
#L4::Ipc::Snd_fpage::Map_type.
- Bits 7..4 (`attr`): Attributes. See #L4_obj_fpage_ctl and
#l4_fpage_cacheability_opt_t, #L4::Ipc::Snd_fpage::Cacheopt.
- Bits MSB­..12 (`hot_spot`): Send base (also called hot spot). See
#L4::Ipc::Snd_fpage::snd_base().
For details, see [IPC Message registers](#l4re_concepts_descr_mrs).
\subsection l4re_concepts_abi_items_receive Receive items
A non-void receive item consists of up to three words.
If not void, the general layout of the first word is defined as follows:
MSB 4 3 2 1 0 bits
┌──────────────────────────┬───┬────────┬───────┬─────┐
│ │ 1 │ rcv_id │ small │ fwd │
└──────────────────────────┴───┴────────┴───────┴─────┘
The `small` and `fwd` bits determine the details of the layout of the whole
message item.
If `small` is unset, then also `rcv_id` must be unset, and the most
significant bits should be zero:
┌──────────────────────────┬───┬────────┬───────┬─────┐
│ SBZ (should be zero) │ 1 │ 0 │ 0 │ fwd │
└──────────────────────────┴───┴────────┴───────┴─────┘
If `small` is set, the most significant bits are layouted as follows:
MSB 12 11 4 3 2 1 0 bits
┌─────────────┬────────────┬───┬────────┬───────┬─────┐
│ rcv cap idx │ SBZ │ 1 │ rcv_id │ 1 │ fwd │
└─────────────┴────────────┴───┴────────┴───────┴─────┘
At most one of `rcv_id` and `fwd` may be set.
The number and meaning of the words in the whole item are determined by the
`small` and `fwd` bits:
first word second word third word
rcv_id small fwd
─┬─────┬─────┬─────┐┌───────────────────┐
│ 0 │ 0 │ 0 ││ rcv flexpage │
─┴─────┴─────┴─────┘└───────────────────┘ 12 11 0
─┬─────┬─────┬─────┐┌───────────────────┐┌─────────────┬─────┐
│ 0 │ 0 │ 1 ││ rcv flexpage ││ fwd cap idx │ SBZ │
─┴─────┴─────┴─────┘└───────────────────┘└─────────────┴─────┘
─┬─────┬─────┬─────┐
│ 0/1 │ 1 │ 0 │
─┴─────┴─────┴─────┘ 12 11 0
─┬─────┬─────┬─────┐┌─────────────┬─────┐
│ 0 │ 1 │ 1 ││ fwd cap idx │ SBZ │
─┴─────┴─────┴─────┘└─────────────┴─────┘
The meaning of the bits in detail:
- Bit 0 (`fwd`): See #L4_RCV_ITEM_FORWARD_MAPPINGS and
#L4::Ipc::Rcv_fpage::forward_mappings(). For `fwd cap idx` see
#L4::Ipc::Rcv_fpage::rcv_task().
- Bit 1 (`small`): See #L4_RCV_ITEM_SINGLE_CAP and #L4::Ipc::Small_buf vs.
#L4::Ipc::Rcv_fpage.
- Bit 2 (`rcv_id`): See #L4_RCV_ITEM_LOCAL_ID.
\subsection l4re_concepts_abi_items_return Return items
A return item always consists of two words. The general layout of a non-void
return item is defined as follows:
first word second word
MSB 12 11 6 5 4 3 2 1 0 bits
┌──────────┬───────┬──────┬───┬──────────┬───┐┌───────────────────┐
│ hot_spot │ order │ type │ 1 │ rcv_type │ c ││ payload │
└──────────┴───────┴──────┴───┴──────────┴───┘└───────────────────┘
└──────────┘ └───┘ └───┘ from send item’s first word
└──────────────┘ from send item’s flexpage
└──────────┘ initially zero
As indicated above, the `hot_spot`, `1`, and `c` (`compound`) are copied from
the sender’s send item’s first word, and `order` and `type` are copied from the
sender’s send item’s flexpage. The `rcv_type` and `payload` are determined by
what is actually transferred, which is also affected by the `rcv_id` bit in the
receiver’s receive item. The `rcv_type` determines the content and layout of the
payload.
There are four cases for `rcv_type`:
`00`: Used if at least one mapping was actually transferred for
the corresponding send item. The payload is undefined:
(also see #L4::Ipc::Snd_fpage::cap_received()):
┌──────────┬───────┬──────┬───┬──────────┬───┐┌───────────────────┐
│ hot_spot │ order │ type │ 1 │ 00 │ c ││ undefined │
└──────────┴───────┴──────┴───┴──────────┴───┘└───────────────────┘
`01`: Used if transfer of mappings was attempted, but actually
nothing was transferred, because nothing was mapped on the sender’s side for
the corresponding send item. The payload is undefined:
┌──────────┬───────┬──────┬───┬──────────┬───┐┌───────────────────┐
│ hot_spot │ order │ type │ 1 │ 01 │ c ││ undefined │
└──────────┴───────┴──────┴───┴──────────┴───┘└───────────────────┘
`10`: Used if the receive item’s `rcv_id` bit was set and the conditions for
transferring an IPC gate label were fulfilled. In that case, no mapping is done
for this item and the payload consists of the bitwise OR (`|`) of the IPC gate
label and the write and special permissions (see #L4_CAP_FPAGE_W and
#L4_CAP_FPAGE_S) that would have been mapped (also see
#L4::Ipc::Snd_fpage::id_received()):
2 1 0 bits
┌──────────┬───────┬──────┬───┬──────────┬───┐┌──────────┬────────┐
│ hot_spot │ order │ type │ 1 │ 10 │ c ││ label │ rights │
└──────────┴───────┴──────┴───┴──────────┴───┘└──────────┴────────┘
`11`: Used if the receive item’s `rcv_id` bit was set and the conditions for
transferring the sender’s flexpage word were fulfilled. In that case, no mapping
is done for this item and the payload is a copy of the sender’s flexpage word
(also see #L4::Ipc::Snd_fpage::local_id_received()):
┌──────────┬───────┬──────┬───┬──────────┬───┐┌───────────────────┐
│ hot_spot │ order │ type │ 1 │ 11 │ c ││ send flexpage │
└──────────┴───────┴──────┴───┴──────────┴───┘└───────────────────┘
*/

593
src/l4/doc/source/l4_ipc.dox Normal file
View File

@@ -0,0 +1,593 @@
// vi:ft=c
/* -*- c -*- */
/**
\page l4re_concepts_ipc %L4 Inter-Process Communication (IPC)
Inter-process communication (IPC) is the fundamental communication mechanism in
the L4Re Microkernel.
Basically IPC invokes a subroutine in a different context using input and
output parameters. It is used to communicate between userland threads and, as a
special case, to communicate between a userland thread and a kernel object. IPC
provides the only (non-debugging) way of doing system calls.
\section l4re_concepts_ipc_mechanism IPC mechanism
When using this API, an IPC operation can be conducted using the l4_ipc()
function (or one of its related \ref l4_ipc_api "helpers"). In general it
causes a method to be invoked on the called kernel object. An IPC operation
consists of a send and receive phase, but either of them can be skipped, that
is, an IPC operation can consist of only either a send or a receive phase. IPC
is always synchronous and blocking and can be given a timeout. Timeouts can be
specified separately for each phase. Invoking the IPC syscall without any phase
is deprecated.
On the lowest abstraction level, IPC operations need the following arguments:
- \ref l4re_concepts_descr_flags "flags" describing the IPC mode,
- the \ref l4re_concepts_descr_capidx "capability selector" of the
communication partner,
- a \ref l4re_concepts_descr_label "label",
- a \ref l4re_concepts_descr_msgtag "message tag", and
- a pair of \ref l4re_concepts_descr_timeouts "timeout" values.
During an IPC operation the kernel accesses the UTCB of the current thread to
read parameters which are not passed as direct arguments.
As result of an IPC operation the kernel returns a message tag and a label and
the kernel also changes UTCB content. For the detailed call signature, refer to
l4_ipc(). Furthermore, depending on the IPC parameters, the kernel might have
transferred the FPU state and capabilities (memory, I/O ports, and/or object
capabilities) from the sender to the receiving thread.
The transition between the IPC send phase and the IPC receive phase is atomic,
that is, as soon as the send phase has finished, the thread receive phase
starts. A relative receive timeout does not start before the send phase has
finished (see also below) and a thread which received an IPC call from another
thread can assume that the other thread is ready to receive the reply message
and the replying thread can therefore reply with a timeout of zero, see
\ref l4re_concepts_descr_timeouts.
For performance optimization and under certain conditions, the kernel may
perform a context switch from the IPC sender to the IPC receiver without
consulting the scheduler after the send phase finished. For instance, a client
performing an IPC call to a server has to wait for the server anyway. Hence,
after the client request was sent to the server, the kernel switches directly
to the server thread. This behavior can be disabled by setting the
#L4_MSGTAG_SCHEDULE flag in the sender message tag (see below).
\subsection l4re_concepts_descr_flags IPC Flags
The *flags* defined in #l4_syscall_flags_t are used by the invoking thread to
define the intended IPC operation. The variants of l4_ipc() (see \ref
l4_ipc_api) use the flags
- to request the IPC phases (send-only IPC, receive-only IPC, IPC with send
and receive phase), and
- to decide, if the reply capability (see \ref l4re_concepts_descr_capidx
"below") should be used instead of the capability of a dedicated kernel
object as target for the send phase (*reply*), and
- to decide, if receiving should wait for an incoming message from any
possible sender (*open wait*) instead of a message from a dedicated
sender (*closed wait*).
\subsection l4re_concepts_descr_capidx Partner capability selector
The *partner capability selector* defines a kernel object as partner of the IPC
operation. Some kernel objects forward IPC to a userland thread.
Basically an object capability is represented by #l4_cap_idx_t where the bits
starting from #L4_CAP_SHIFT are used as index into the local capability table
of the current address space.
Specifying #L4_INVALID_CAP as target for an IPC operation is equivalent to
specifying a thread capability of the current thread with full permissions.
As a result, the userland thread either communicates with its corresponding
kernel thread object (if #L4_PROTO_THREAD is specified as protocol value,
see the description of the message tag \ref l4re_concepts_descr_msgtag "below")
or the IPC target is the current userland thread. In the latter case, no IPC
will be performed and the send phase and the receive phase will block until the
corresponding timeout has expired, see \ref l4re_concepts_descr_timeouts
"below".
A special partner is defined by the *reply capability*. Since it would
be impractical (and a security flaw) to always pass an explicit object
capability to reply to for each IPC, the kernel generates an implicit one that
can be used for just that purpose if the IPC contains an **open wait** phase.
The reply capability is valid after a receive phase and points to the kernel
object that sent the IPC just received. It can be used only once. The reply
capability is selected by setting the #L4_SYSF_REPLY flag, see \ref
l4re_concepts_descr_flags "above".
\subsection l4re_concepts_descr_label IPC Label
The IPC label is a machine word which is transferred unchanged from the IPC
sender to the IPC receiver when directly sending to a userland thread. However,
the primary purpose of the label is to create a relationship between an
L4::Rcv_endpoint (L4::Ipc_gate or L4::Irq) and the bound thread.
During L4::Rcv_endpoint::bind_thread(), a label is specified. If the thread
receives an IPC message through the endpoint, that label is delivered to the
receiving thread as output parameter of l4_ipc() instead of the label specified
during the corresponding IPC send operation (see the detailed description of
L4::Ipc_gate for more details on the label with IPC gates). The label is
usually used by the receiving thread to invoke the object which is responsible
for handling the IPC request of the corresponding endpoint. This mechanism is
used by the L4::Epiface mechanism for server loops.
\subsection l4re_concepts_descr_msgtag IPC Message Tag
The *message tag* (#l4_msgtag_t) describes the payload of the IPC and
can also be used to enable certain features. It contains:
- a *protocol value* (cf. l4_msgtag_t::label(), also called the tag's
_label_),
- the number of items in \ref l4re_concepts_descr_mrs
"UTCB message registers" to transfer (cg. l4_msgtag_t::words() and
l4_msgtag_t::items()), and
- flags (cf. l4_msgtag_t::flags() and #L4_msgtag_flags, may be 0).
The information from the message tag is required by the kernel to transfer the
message. The IPC system call returns a message tag as result of the IPC
operation. On success, a copy of the message tag specified by the sender is
returned if there is a receive phase. Without receive phase, a successful IPC
syscall returns the message tag specified as input parameter.
Failures during IPC are signalled using the #L4_MSGTAG_ERROR flag in the
message tag. If this bit is set by the kernel, the content of the returned
message tag apart from that bit is undefined and the kernel wrote the actual
error code into the l4_thread_regs_t::error register of the UTCB (see also
\ref l4re_concepts_descr_tcrs). When an IPC error occurs after the rendezvous
of the IPC partners, both partners observe the same error information. If, for
instance, the IPC was aborted using L4::Thread::ex_regs(), the sender gets an
#L4_IPC_SECANCELED error while the receiver gets an #L4_IPC_RECANCELED error.
The function L4Re::chkipc() can be used to verify that an IPC operation
finished successfully: It throws an error if the IPC failed.
\internal
See kk-all chat from 2022-04-11: Alex says that the message tag is undefined in
case of an error (only the error bit is set).
\endinternal
The *protocol value* is usually used to distinguish between different
protocols of the same interface. Certain protocol IDs are pre-defined when
talking to kernel objects, see #L4_msgtag_protocol. From IPC point of view, the
protocol value is just payload that is transferred from sender to receiver and
hence doesn't have a dedicated meaning.
By convention, during IPC calls, the protocol value is used for return values,
where negative values signify errors. See the
\ref l4_cxx_ipc_iface_return_types "section" about %L4 RPC return types for
further information. The function L4Re::chksys() can be used to verify that an
RPC call using IPC was successful: It throws an error if the IPC failed or if
the returned protocol value is negative.
\subsection l4re_concepts_descr_timeouts IPC Timeouts
As written above, IPC *timeouts* are specified separately for the send phase
(IPC send timeout) and the receive phase (IPC receive timeout). The timeout of
one phase is encapsulated by #l4_timeout_s. Both timeouts are combined into a
single #l4_timeout_t parameter. Timeouts are either relative to the current
time of the invoking thread or absolute. In the latter case, the absolute time
of the deadline of the respective phase is written into a UTCB buffer register
(see l4_timeout_abs()). The relative timeout of the receive phase starts
immediately after the send phase has finished.
Two specific timeout values are sufficient for most IPC operations:
- #L4_IPC_TIMEOUT_NEVER is used if the IPC partner might not yet be ready.
Usually a client trusting a server will perform an IPC call with an
infinite timeout for both phases. The send phase will take some time if the
IPC receiver is currently not ready. The receive phase will take some time
as the server needs time to serve the request. Also, a server will usually
wait with an infinite receive timeout for the next request (see below for
a possible exception).
- #L4_IPC_TIMEOUT_0 is used when it is either certain that the IPC receiver
is currently ready or if the IPC sender doesn't want to wait if the IPC
receiver is not ready. The former case applies to a thread which was called
with an IPC call, for example a server got a client request. The reply to
the IPC call should use a timeout of zero to ensure that a client doesn't
block a server (server could not deliver the result of the request).
See also L4::Ipc_svr::Default_timeout.
Another case is an IPC send operation for waking up another thread from an
IPC receive operation. If the other thread is not ready to receive, then it
might be already woken up and it does not make sense to wait any longer.
Also triggering an IRQ is usually done with a send timeout of 0, see
L4::Triggerable::trigger().
In certain cases it also makes sense to specify an IPC timeout different from
"never" or "zero":
- A server might leave the server loop after some time to perform idle work
(see L4::Ipc_svr::Server_iface::add_timeout()).
- A thread does not want to wait for an infinite time if the partner is not
ready. This could be also some safety measure.
- A thread wants to block for a certain amount of time without consuming CPU
time. The l4_ipc_sleep() function specifies the #L4_INVALID_CAP as target
for an IPC receive operation and specifies the intended relative waiting
period as IPC timeout. Waiting for an absolute timeout would be possible
with similar code.
\note The kernel IPC path is optimized for the two special cases using
#L4_IPC_TIMEOUT_NEVER and #L4_IPC_TIMEOUT_0. Specifying a different
timeout causes more maintenance effort for the kernel.
\note Special care is required if a finite timeout for the receive phase of an
IPC call is specified: The IPC receive operation could abort before the
partner was able to send the reply message. Under certain circumstances
the partner may still have the temporary reply capability to the calling
thread and may use this capability to reply to the caller at a later,
unexpected time specifying an arbitrary IPC label. This case is relevant
for servers which call another, possibly untrusted, server while serving a
client request.
\subsection l4re_concepts_descr_utcb User-level Thread Control Block
The \ref l4_utcb_api "UTCB" is located on a power-of-2-sized and
power-of-2-aligned memory area shared between userland and the kernel
(L4::Task::add_ku_mem()). The UTCB is bound to a thread during the
L4::Thread::control() operation with the L4::Thread::Attr parameters set up
using L4::Thread::Attr::bind(). The UTCB is used for IPC-related data exchange
and is set up before invoking l4_ipc(). To access certain parts of the UTCB,
the corresponding functions have to be used (there is no data type L4_utcb or
similar). The UTCB consists of:
- the \ref l4re_concepts_descr_mrs "message registers"
`MR[0]`, `MR[1]`, ..., `MR[n-1]` with n = #L4_UTCB_GENERIC_DATA_SIZE
(access using l4_utcb_mr()),
- the \ref l4re_concepts_descr_bdr "buffer descriptor register" `BDR`
(access using l4_utcb_br(), see l4_buf_regs_t::bdr),
- the \ref l4re_concepts_descr_brs "buffer registers"
`BR[0]`, `BR[1]`, ..., `BR[m-1]` with m = #L4_UTCB_GENERIC_BUFFERS_SIZE
(access using l4_utcb_br()),
- the \ref l4re_concepts_descr_tcrs "thread control registers" (access using
l4_utcb_tcr(), includes the IPC error code), and
- in case of an exception IPC, the register state of the thread which
triggered the exception (access using l4_utcb_exc()).
IPC to a kernel object requires the setup of the UTCB of the corresponding
userlevel thread. IPC between userlevel threads requires the setup of UTCBs
of both partners.
The kernel changes only the following UTCB content:
- The message registers of the UTCB of the receiver of an IPC, and
- the IPC error field of the thread invoking l4_ipc() if there was an error
during IPC.
\internal
Another exception: See Ic7e8aa98d8f782b684445cc6f866df3bffae2c37 / #CD-518.
\endinternal
\subsubsection l4re_concepts_descr_mrs IPC Message registers
The *message registers* contain *untyped items* and *typed items*. The sender's
typed items are interpreted by the kernel in conjunction with the receiver's
_receive items_. Each typed send item occupies two message registers.
The untyped items, on the other hand, are free to be used by the communication
partners to exchange data: The content of all message registers used for
untyped items (l4_msgtag_t::words()) is copied from the UTCB of the IPC sender
to the UTCB of the IPC receiver.
A typed send item consists of a *flexpage* (see l4_fpage(), l4_obj_fpage(), and
l4_iofpage()) of the to be transferred capabilities (*flexpage word*) and a
_message word_. There are two types of send items: *map items* and *void
items*. For a void item, the message word is all zero. For a map item, the
message word contains:
- the *compound bit* allowing to use the same receive buffer for the
subsequent typed send item (scatter-gather behavior,
see #L4_ITEM_CONT of #l4_msg_item_consts_t),
- the *type bit* defining this typed send item as a *map item*,
- the *grant flag* for delegating the access to the flexpage from the
sender to the receiver and atomically removing the rights from the sender
(see #l4_msg_item_consts_t),
- *attributes* with semantics depending on the item type; for memory
mappings, they contain cacheability information
(see #l4_fpage_cacheability_opt_t); for objects, they contain additional
rights (see #L4_obj_fpage_ctl),
- the *send base* (also called *hot spot*) defining what is actually mapped
when send and receive flexpages have a different size.
A typed send item can be created using l4_sndfpage_add(). This function sets
the compound bit unconditionally. Alternatively, the functions l4_map_control()
and l4_map_obj_control() can be used to set up the message word of a map item
for a memory flexpage respective for objects.
See \ref l4re_concepts_descr_transfer "below" for a description how typed items
are transferred.
\subsubsection l4re_concepts_descr_brs IPC Buffer Registers
The *buffer registers* and *buffer descriptor register* are
interpreted by the kernel during the receive phase (if any). Buffer registers
define *receive items* which are required to receive typed send items (memory,
I/O ports or object capabilities). To specify a receive item, up to three buffer
registers are required:
- A *small receive item* (L4::Ipc::Small_buf) occupying one buffer
register is sufficient to receive one object capability.
- A *receive item* (L4::Ipc::Rcv_fpage) occupying two or three buffer
registers (*message word*, a *flexpage*, and an optional destination task
capability index) is required to receive memory flexpages, I/O ports, or
multiple object capabilities.
\subsubsection l4re_concepts_descr_bdr IPC Buffer Descriptor Register
The buffer descriptor register defines indices of buffer registers used to
receive dedicated types of send items and also contains a flag:
- 5 bits starting at #L4_BDR_MEM_SHIFT define the index of the first receive
item used for memory flexpages.
- 5 bits starting at #L4_BDR_IO_SHIFT define the index of the first receive
item used for I/O flexpages.
- 5 bits starting at #L4_BDR_OBJ_SHIFT define the index of the first receive
item used for object flexpages.
- The #L4_UTCB_INHERIT_FPU can be set using l4_utcb_inherit_fpu() and allows
to receive the FPU state from the IPC sender. This is only relevant if the
sender set #L4_MSGTAG_TRANSFER_FPU in the message tag.
For most use cases, a BDR value of zero is sufficient. In that case, if `BR[0]`
contains a void item, no capabilities are received. Otherwise, only one type of
capabilities (memory, I/O ports or objects) can be received even if there are
several receive items. For more complex setups that require receiving different
types of capabilities in one receive operation, other BDR values are necessary.
The BDR of the receiving thread is only used by the kernel if at least one
typed item is transferred during the IPC or if #L4_MSGTAG_TRANSFER_FPU is set
in the UTCB of the sending thread.
\subsubsection l4re_concepts_descr_tcrs IPC Thread Control Registers
The l4_thread_regs_t::error register contains the IPC error code in case the
#L4_MSGTAG_ERROR flag is set in the message tag returned by an IPC syscall.
Otherwise this register is not touched by the kernel. See
#l4_ipc_tcr_error_t for a detailed enumeration of all possible error codes
during an IPC operation.
The l4_thread_regs_t::free_marker is set by the kernel to zero immediately
before a thread is destroyed. This value indicates that the kernel does not
longer use the UTCB and it can be re-used by other threads.
The other members of l4_thread_regs_t are never touched by the kernel.
\subsection l4re_concepts_descr_transfer Transfer of Typed Send Items
The kernel interprets all typed items in the sender UTCB (l4_msgtag_t::items())
and performs the following operations while modifying the corresponding typed
items in the receiver UTCB:
- If the message item of the sender is void, this item is ignored and the
message word of the corresponding typed item in the receiver UTCB is set to
zero (making it a void item). The flexpage word of this item is not
changed.
- Otherwise, if the type bit of the message item of the sender is not set,
the IPC is aborted with #L4_IPC_SEMSGCUT / #L4_IPC_REMSGCUT.
- Otherwise, if there is a receive item corresponding to the flexpage type of
the send item available (see \ref l4re_concepts_descr_bdr), information
described by the flexpage is transferred to the receiver.
In the last case, the message word of the typed item in the receiver UTCB is
modified to contain the send base, the type and the size of the transferred
flexpage, as well as a copy of the compound bit and the type bit of the send
item. If the receiver ordered a local ID in the corresponding receive item, the
kernel attempts to apply special rules, see #L4_RCV_ITEM_LOCAL_ID. Otherwise,
regular mappings as described by the flexpage of the send item are created in
the receiver space.
A receive item forms a *receive window* of a specific address and size in the
receiver space. Each typed send item that is a map item requires a
corresponding receive item. By default, there is a one-to-one mapping (one
receive item per typed send item) but it is also possible to use one receive
item to receive several typed send items: The compound bit (see
#l4_msg_item_consts_t) of a send item defines if the following typed send item
shall use the same receive item as the current one for receiving the flexpage.
If the compound bit is set, proper values of the send base shall be used to
prevent overlapping of addresses in the receiver space.
The send base is relevant when the size of the receive flexpage differs from
the size of the transferred resource. As a typical example, triggering a memory
page fault opens a receive window covering the entire memory address space of
the faulting thread. The pager will usually reply a memory flexpage smaller
than the entire address space of the faulting thread. Hence, the pager has to
specify a proper base which is used as offset of the sent object in the receive
flexpage in the *receiver space*. If the sender flexpage is bigger than the
receive window, a flexpage of the size of the receive window starting at the
send base in the *sender space* is transferred to the receiver.
\internal
See Fiasco's source code: map_util.cpp / free_constraint().
\endinternal
The kernel will stop transmission of typed items before l4_msgtag_t::items() is
reached either if it finds a void item as receive buffer or if the flexpage
type of the send item does not match the flexpage type of the corresponding
receive item. Under both conditions, the IPC is aborted with #L4_IPC_SEMSGCUT /
#L4_IPC_REMSGCUT.
\note The kernel ignores the flexpage access rights of the receive items. The
actual rights for a transferred resource in the target address space are
defined by the access rights to that resource of the IPC sender address
space and the flexpage access rights in the typed send item.
Additionally, when transferring object capabilities, the transferred
rights also depend on the sender’s rights on the capability invoked for
IPC.
The kernel does not unmap capabilities in the receive window when there is no
capability present at the corresponding index at the sender. Further, the
receiver cannot reliably detect at which capability indices it received
capabilities in its receive windows. Therefore, before receiving from an
untrusted source, all receive windows should be cleared. Otherwise the receiver
may erroneously associate a capability in one of its receive windows with his
last IPC partner although it was actually received in an earlier IPC.
However, the kernel indicates if at least one object capability was received or
not, see #L4::Ipc::Snd_fpage::cap_received().
\section l4re_concepts_ipc_examples Examples
A number of examples show the interplay of the concepts introduced so far.
\subsection l4re_concepts_ipc_examples_1 User Thread to Kernel Object
The L4::Scheduler kernel object has a method L4::Scheduler.idle_time(). It
takes a set of CPUs to query, represented by two machine words.
In user space, the function L4::Cap<L4::Scheduler>->idle_time() is called,
which does the following:
- Fill `MR[0]` with a constant identifying the method being called
(#L4_SCHEDULER_IDLE_TIME_OP).
- Fill `MR[1]` and `MR[2]` with the two words making up the CPU set.
- Set up the message tag with the protocol value (#L4_PROTO_SCHEDULER), the
number of untyped and typed items (3 and 0), and some flags.
- Call l4_ipc() with the partner capability ID, the tag, the pointer to the
filled UTCB, infinite timeouts, and with flags indicating a send and
receive phase. (The label does not matter in this case.)
This function traps into kernel space using standard platform specific
mechanisms. The kernel reads the protocol value on the message tag, checks that
the partner capability ID refers to a valid object that speaks that protocol,
and dispatches the message to the appropriate handler. The handler fills the
first 64 bits of the message registers with the computed time value. This will
cover `MR[0]` on 64-bit architectures and `MR[0]` and `MR[1]` on 32-bit
architectures.
It then sets up the return message tag:
- The number of untyped items is 1 or 2.
- The number of typed items is 0.
- The protocol value contains the return value and is set to 0.
- An error would be signalled as a negative protocol value. Under certain
conditions (e.g. wrong kernel object capability specified), the error is
signalled as IPC error (see #L4_MSGTAG_ERROR in the description of the
\ref l4re_concepts_descr_msgtag).
- (The return label is as irrelevant in this case as the send label.)
This reply is received by the receive phase of the original l4_ipc() call from
userland. Finally the l4_ipc() function copies the time value out of the
message registers and forwards it with a possible error from the message tag
flags to its caller.
\subsection l4re_concepts_ipc_examples_2 User Thread to User Thread
When the target kernel object is of type L4::Thread (or L4::Ipc_gate, but we
will cover this in the example \ref l4re_concepts_ipc_examples_3 "below") and
the message tag's protocol value is not #L4_PROTO_THREAD, the kernel will
forward the IPC message to the userland thread represented by the kernel
object. There it can be received by a call to l4_ipc(). The restriction of the
protocol number is necessary because one also wants to invoke L4::Thread's
control methods such as L4::Thread.switch_to() or L4::Thread.ex_regs(). Besides
this restriction, the interpretation of all the IPC parameters and the untyped
items of the UTCB is up to the communication partners.
\subsubsection l4re_concepts_ipc_examples_2_1 Simple Messages
A simple example is a client calling a server to have a computation performed
on a value: Similar to IPC from a userland thread to a kernel object, the
client writes the value to `MR[0]`. It sets up the message tag with some agreed
upon protocol value (which, as explained above, must be different from
#L4_PROTO_THREAD), number of untyped items to 1, typed items to 0, and no flags
set. The client may want to pass a label that identifies itself, as many
clients can use the server. In this context, the identifier might also be
passed via the message registers, but the label is the proper place for this,
as it gets a special treatment by the kernel for IPC gates (covered by the
example \ref l4re_concepts_ipc_examples_3 "below"). The client then calls
l4_ipc() with the tag, label and flags indicating it wants a send phase and a
receive phase (as it wants a result back). The target is the capability index
referring to a capability for the L4::Thread kernel object of the server.
To be able to receive an IPC message, the server has set up a UTCB of its own
and called l4_ipc() with flags indicating it only wants to enter a receive
phase and it accepts IPCs from any partner. This is called an **open wait**.
(The alternative would be to specify a capability index referring to a
L4::Thread capability to exclusively receive from.)
Both system calls (the send IPC initiated by the client and the receive IPC
initiated by the server) may be seen by the kernel in any order but the IPC
will not start before sender and receiver are ready. In that case the kernel
will copy the relevant message registers the client specified in the message
tag from the client's UTCB to the server's UTCB, in the current example just
`MR[0]`. It will then switch the client to the receive phase of its call (which
cannot yet be executed) and return the server's call with the message tag and
label.
The server inspects the tag for the correct protocol value and number of
untyped items passed, inspect the label to decide whether it maybe wants
special treatment of this particular client, performs the computation on
`MR[0]` and writes the result back to `MR[0]` (or to more words, depending on
what exactly it computes). It sets up the tag in the usual way, but probably
needs to pass no label, as the client knows who it is talking to.
For the reply, the server makes use the reply capability (see
\ref l4re_concepts_descr_capidx "above"). Since the client sent the last IPC to
the server, the reply capability will point to it. So when the server calls
l4_ipc() with the computed result in the message registers and using the reply
capability as target, the kernel knows to forward this to the client's thread.
The kernel copies the message registers from the server's UTCB to the client's
UTCB, and the client's l4_ipc() system call, which is still stuck in the
receive phase, is returned with the tag.
The client looks at the tag and then the message registers for its wanted
result and the example is concluded.
\subsubsection l4re_concepts_ipc_examples_2_2 Send Items
IPC between userland threads is also used to transfer typed items: Memory, I/O
ports, and objects, all represented as flexpages. Typed items and untyped
items can be part of the same IPC. As general rule, the sender specifies what
he wants to send, the receiver where and how much it wants to receive, and the
kernel checks the required permissions before doing the actual transfer. As
written before, this mechanism is synchronous and the receiver cannot be
transferred items against its will. \see l4_fpage_api
Suppose a client wants a server to have read only access to a page of its
memory. The client sets up a flexpage covering the page and with only the
#L4_FPAGE_RO right set. The server sets up a flexpage of a memory region where
it will receive the mapping. This may be larger than one page, suppose for our
case four pages, in which case the exact position of the mapping will be
resolved by the send base provided by the sender. The client combines the hot
spot and some flags into a machine word and writes it to `MR[0]` (see also
l4_map_control()). At `MR[1]` follows the flexpage it wants to send (see also
l4_fpage()). The server does almost the same but writes the words to `BR[0]`
and `BR[1]`. (The server could also specify a hot spot, but it is currently
ignored by the kernel.) The client specifies 1 typed and 0 untyped items in the
message tag. The server writes 0 to `BDR` to specify that the first receive
item starts at the first buffer register.
Both client and server initiate their IPC, the client with only a send phase to
the server, and the server with an open wait receive phase. The kernel checks
the compatibility of the send items and the receive buffers (e.g. that no
object capability flexpage is sent to a receive buffer describing a memory
mapping flexpage) and updates its internal structures to reflect the change. In
our case, the sender's hot spot indicates to which of the four pages that make
up the receive buffer the sent page should be mapped. The kernel also
translates the typed send item to the server's address space and stores it in
the server's UTCB at `MR[0]` and `MR[1]`.
Once the server returns from its syscall, it will have read access to the
client's shared page.
\subsection l4re_concepts_ipc_examples_3 User Thread to User Object
A common use case for thread to thread communication is when a server
implements a number of object interfaces and a client wants to invoke methods
on them. For security reasons, the server does not want to hand out its thread
capability to everyone it nonetheless wants to serve. It also may not want to
allow every client access to everyone of its interfaces. For this purpose,
IPC gates implemented by the kernel object L4::Ipc_gate can be used.
An IPC gate can be bound to a thread and forwards IPC to it. In doing so it
applies two transformations
1. It sets the label to a predefined value.
2. It changes the rights of transferred items (see #L4_CAP_FPAGE_S).
For each object of every interface the server implements, it creates an IPC
gate and binds it to itself (see L4::Ipc_gate::bind_thread()). It sets the
gate's label to a unique value identifying the object. Then it hands the gate
out to clients. Several clients can be handed the same gate and will all end up
invoking methods on the same object.
Instead of setting the target as the server's thread kernel object, the client
uses the IPC gate's instead. The label the client sends is irrelevant, as the
gate will overwrite it with the value the server has set during the bind
operation. The server executes an open wait, and the kernel performs the same
operation as in the above \ref l4re_concepts_ipc_examples_2_2 "example" with
the transformed IPC finally ending up in the server's thread.
The server checks that the received label refers to one of its objects. It then
checks if the protocol value in the message tag matches the interface the
object implements. Then it invokes the method specified in `MR[0]` with the
rest of the arguments. Finally it returns the results via UTCB and message tag
to the reply capability and waits for the next IPC.
*/

24
src/l4/doc/source/l4re-awesome.css Normal file
View File

@@ -0,0 +1,24 @@
/* Disable animation when showing search results. */
#MSearchResultsWindow {
animation: none;
}
/* more visually responsive sidebar */
html {
--side-nav-arrow-opacity: 0.4;
--side-nav-arrow-hover-opacity: 1;
--side-nav-hover-background: #f0f0f0;
}
#nav-tree div.item:hover .arrow {
opacity: var(--side-nav-arrow-opacity);
}
#nav-tree div.item a:hover .arrow {
opacity: var(--side-nav-arrow-hover-opacity);
}
#nav-tree div.item:has(a:hover), #nav-tree div.item:has(a:focus) {
background-color: var(--side-nav-hover-background);
}

17
src/l4/doc/source/l4re-footer.html Normal file
View File

@@ -0,0 +1,17 @@
<!-- HTML footer for doxygen 1.9.1-->
<!-- start footer part -->
<!--BEGIN GENERATE_TREEVIEW-->
<div id="nav-path" class="navpath"><!-- id is needed for treeview function! -->
<ul>
$navpath
<li class="footer">$generatedby <a href="https://www.doxygen.org/index.html"><img class="footer" src="$relpath^doxygen.svg" width="104" height="31" alt="doxygen"/></a> $doxygenversion </li>
</ul>
</div>
<!--END GENERATE_TREEVIEW-->
<!--BEGIN !GENERATE_TREEVIEW-->
<hr class="footer"/><address class="footer"><small>
$generatedby&#160;<a href="https://www.doxygen.org/index.html"><img class="footer" src="$relpath^doxygen.svg" width="104" height="31" alt="doxygen"/></a> $doxygenversion
</small></address>
<!--END !GENERATE_TREEVIEW-->
</body>
</html>

56
src/l4/doc/source/l4re-header.html Normal file
View File

@@ -0,0 +1,56 @@
<!-- HTML header for doxygen 1.9.1-->
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "https://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<meta name="generator" content="Doxygen $doxygenversion"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<!--BEGIN PROJECT_NAME--><title>$projectname: $title</title><!--END PROJECT_NAME-->
<!--BEGIN !PROJECT_NAME--><title>$title</title><!--END !PROJECT_NAME-->
<link href="$relpath^tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="$relpath^jquery.js"></script>
<script type="text/javascript" src="$relpath^dynsections.js"></script>
$treeview
$search
$mathjax
<link href="$relpath^$stylesheet" rel="stylesheet" type="text/css" />
$extrastylesheet
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<!--BEGIN TITLEAREA-->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<!--BEGIN PROJECT_LOGO-->
<td id="projectlogo"><img alt="Logo" src="$relpath^$projectlogo"/></td>
<!--END PROJECT_LOGO-->
<!--BEGIN PROJECT_NAME-->
<td id="projectalign" style="padding-left: 0.5em;">
<div id="projectname">$projectname
<!--BEGIN PROJECT_NUMBER-->&#160;<span id="projectnumber">$projectnumber</span><!--END PROJECT_NUMBER-->
</div>
<!--BEGIN PROJECT_BRIEF--><div id="projectbrief">$projectbrief</div><!--END PROJECT_BRIEF-->
</td>
<!--END PROJECT_NAME-->
<!--BEGIN !PROJECT_NAME-->
<!--BEGIN PROJECT_BRIEF-->
<td style="padding-left: 0.5em;">
<div id="projectbrief">$projectbrief</div>
</td>
<!--END PROJECT_BRIEF-->
<!--END !PROJECT_NAME-->
<!--BEGIN DISABLE_INDEX-->
<!--BEGIN SEARCHENGINE-->
<td>$searchbox</td>
<!--END SEARCHENGINE-->
<!--END DISABLE_INDEX-->
</tr>
</tbody>
</table>
</div>
<!--END TITLEAREA-->
<!-- end header part -->

2847
src/l4/doc/source/l4re.cfg Normal file
View File

File diff suppressed because it is too large Load Diff

80
src/l4/doc/source/l4re.dox Normal file
View File

@@ -0,0 +1,80 @@
/* vim:set ft=c: */
/**
* \example hello/server/src/main.c
* This is the famous "Hello World!" program.
*
* \example examples/sys/ipc/ipc_example.c
* This example shows how two threads can exchange data using the L4 IPC
* mechanism. One thread is sending an integer to the other thread which
* is returning the square of the integer. Both values are printed.
*
* \example examples/sys/ipc/ipc.cfg
* Sample configuration file for the IPC example.
*
* \example examples/sys/start-with-exc/main.c
* This example shows how to start a newly created thread with a defined set
* of CPU registers.
*
* \example examples/sys/singlestep/main.c
* This example shows how a thread can be single stepped on the x86
* architecture.
*
* \example examples/sys/aliens/main.c
* This example shows how system call tracing can be done.
*
* \example examples/sys/utcb-ipc/main.c
* This example shows how to send IPC using the UTCB to store payload.
*
* \example examples/sys/isr/main.c
* Example of an interrupt service routine.
*
* \example examples/clntsrv/src/server.cc
* Client/Server example using C++ infrastructure -- Server implementation.
* \example examples/clntsrv/src/client.cc
* Client/Server example using C++ infrastructure -- Client implementation.
* \example examples/clntsrv/src/shared.h
* Client/Server example using C++ infrastructure -- Shared header file.
* \example examples/clntsrv/configs/clntsrv.cfg
* Sample configuration file for the client/server example.
*
* \example examples/libs/l4re/c/ma+rm.c
* Coarse grained memory allocation, in C.
* \example examples/libs/l4re/c++/mem_alloc/ma+rm.cc
* Coarse grained memory allocation, in C++.
*
* \example examples/libs/l4re/c++/shared_ds/ds_clnt.cc
* Sharing memory between applications, client side.
* \example examples/libs/l4re/c++/shared_ds/ds_srv.cc
* Sharing memory between applications, server/creator side.
* \example examples/libs/l4re/c++/shared_ds/shared_ds.cfg
* Sharing memory between applications, configuration file.
*
* \example examples/libs/l4re/streammap/server.cc
* Client/Server example showing how to map a page to another task -- Server
* implementation. Note that there's also a shared memory library that
* supplies this functionality in more convenient way.
* \example examples/libs/l4re/streammap/client.cc
* Client/Server example showing how to map a page to another task -- Client
* implementation. Note that there's also a shared memory library that
* supplies this functionality in more convenient way.
* \example examples/libs/l4re/streammap/streammap.cfg
* Sample configuration file for the client/server map example.
*
*
* \example examples/libs/libirq/loop.c
* libirq usage example using a self-created thread.
*
* \example examples/libs/libirq/async_isr.c
* libirq usage example using asynchronous ISR handler functionality.
*
* \example examples/sys/migrate/thread_migrate.cc
* Thread migration example.
*
* \example examples/sys/migrate/thread_migrate.cfg
* Sample configuration file for the thread migration example.
*
* \example tmpfs/lib/src/fs.cc
* Example file system for L4Re::Vfs.
*/

16
src/l4/doc/source/latex-extra-stylesheet.tex Normal file
View File

@@ -0,0 +1,16 @@
\DeclareUnicodeCharacter{2264}{$\leq$}
\DeclareUnicodeCharacter{2212}{-}
\DeclareUnicodeCharacter{2500}{-}
\DeclareUnicodeCharacter{2502}{|}
\DeclareUnicodeCharacter{250C}{|-} % \ulcorner
\DeclareUnicodeCharacter{2510}{-|} % \urcorner
\DeclareUnicodeCharacter{252C}{-|-}
\DeclareUnicodeCharacter{2514}{|\_} % \llcorner
\DeclareUnicodeCharacter{2518}{\_|} % \lrcorner
\DeclareUnicodeCharacter{2534}{\_|\_}
\DeclareUnicodeCharacter{2082}{$_{2}$}
\AtBeginDocument{%
\fancyfoot[RE]{\fancyplain{}{\bfseries\scriptsize Generated for L4Re by Doxygen }}
\fancyfoot[LO]{\fancyplain{}{\bfseries\scriptsize Generated for L4Re by Doxygen }}
}

146
src/l4/doc/source/pthreads.dox Normal file
View File

@@ -0,0 +1,146 @@
// vi:ft=c
/**
\page l4re_pthreads Pthread Support
L4Re supports the standard pthread library functionality. Therefore L4Re
itself does not contain any documentation for pthreads itself. Please refer
to the standard pthread documentation instead.
The L4Re specific parts will be described herein.
<ul>
<li>
Include pthread-l4.h header file:
\code
#include <pthread-l4.h>
\endcode
</li>
<li>Return the local thread capability of a pthread thread:
Use \c pthread_l4_cap(pthread_t t) to get the capability index of
the pthread t.
For example:
\code
pthread_l4_cap(pthread_self());
\endcode
</li>
<li> Setting the L4 priority of an L4 thread works with a special
scheduling policy (other policies do not affect the L4 thread
priority):
\code
pthread_t t;
pthread_attr_t a;
struct sched_param sp;
pthread_attr_init(&a);
sp.sched_priority = l4_priority;
pthread_attr_setschedpolicy(&a, SCHED_L4);
pthread_attr_setschedparam(&a, &sp);
pthread_attr_setinheritsched(&a, PTHREAD_EXPLICIT_SCHED);
if (pthread_create(&t, &a, pthread_func, NULL))
// failure...
pthread_attr_destroy(&a);
\endcode
</li>
<li> You can prevent your pthread from running immediately after the call to
\c pthread_create(..) by adding \c PTHREAD_L4_ATTR_NO_START to the
\c create_flags of the pthread attributes. To finally start the thread
you need to call \c scheduler()->run_thread() passing the capability
of the pthread and scheduling parameters.
\code
pthread_t t;
pthread_attr_t attr;
pthread_attr_init(&attr);
attr.create_flags |= PTHREAD_L4_ATTR_NO_START;
if (pthread_create(&t, &attr, pthread_func, nullptr))
// failure...
pthread_attr_destroy(&attr);
// do stuff
auto ret = L4Re::Env::env()->scheduler()->run_thread(pthread_l4_cap(t),
l4_sched_param(2));
if (l4_error(ret))
// failure...
\endcode
</li>
</ul>
<h4>
Constraints on pthread_t, user-land capability slot, and kernel thread-object
</h4>
<ul>
<li>
`pthread_l4_cap()` is guaranteed to return the valid capability slot
of the pthread (A) until `pthread_join()` or `pthread_detach()` is invoked
on (A)'s `pthread_t`.
</li>
<li>
`pthread_l4_cap()` exposes internal state of the pthread management, take
the necessary precautions as you would for any shared data in concurrent
environments.
If you use `pthread_l4_cap()` guarding against concurrency issues is your
duty.
</li>
<li>
There is no guarantee that a valid capability slot points to a
present capability.
</li>
<li>
<b>Example</b>
It is possible to obtain a valid thread capability slot and for
`l4_task_cap_valid()` to return the capability as not present.
The following example showcases a possible sequence of events.
\code
// Assume: void some_func(void *)
pthread_t pthread = nullptr;
pthread_create(&pthread, nullptr, some_func, nullptr);
// pthread running some_func()
l4_cap_idx_t cap_idx = pthread_l4_cap(pthread);
l4_is_valid_cap(cap_idx); // ---> true
long valid = l4_task_cap_valid(L4RE_THIS_TASK_CAP, cap_idx).label());
// valid == 1 --> capability object is present (refers to a kernel object).
// some_func() exits
cap_idx = pthread_l4_cap(pthread);
l4_is_valid_cap(cap_idx); // ---> true
valid = l4_task_cap_valid(L4RE_THIS_TASK_CAP, cap_idx).label());
// valid == 0 --> capability object is not present (refers to no kernel object).
pthread_join(pthread, nullptr); // invalidates the cap slot and frees
// the pthread's data structures
// using cap_idx here is undefined behavior.
\endcode
</li>
</ul>
*/

14
src/l4/doc/source/search.js.reduce_keyTimeoutLength.patch Normal file
View File

@@ -0,0 +1,14 @@
Make Doxygen search field snappier.
diff -Naur old/html/search/search.js new/html/search/search.js
--- old/html/search/search.js 2024-08-05 15:40:32.890343561 +0200
+++ new/html/search/search.js 2024-08-05 15:40:42.557089345 +0200
@@ -63,7 +63,7 @@
this.name = name;
this.resultsPath = resultsPath;
this.keyTimeout = 0;
- this.keyTimeoutLength = 500;
+ this.keyTimeoutLength = 50;
this.closeSelectionTimeout = 300;
this.lastSearchValue = "";
this.lastResultsPage = "";

94
src/l4/doc/source/server_overview.dox Normal file
View File

@@ -0,0 +1,94 @@
// vi:ft=c
/**
\page l4re_servers L4Re Servers
\brief Here you shall find a quick overview over the standard services
running on the L4Re Microkernel.
Sigma0, the Root Pager
======================
Sigma0 is a special server running on L4 because it is responsible
of resolving page faults for the root task, the first useful task on
L4Re. Sigma0 can be seen as part of the kernel, however it runs in
unprivileged mode. To run something useful on the L4Re Microkernel you
usually need to run Sigma0, nevertheless it is possible to replace Sigma0 by
a different implementation.
For more details see \subpage l4re_servers_sigma0
Moe, the Root Task
==================
Moe is our implementation of the L4 root task that is responsible for
bootstrapping the system, and to provide basic resource management services
to the applications on top. Therefore Moe provides L4Re resource management
and multiplexing services:
\li \b Memory in the form of memory allocators (L4Re::Mem_alloc, L4::Factory)
and data spaces (L4Re::Dataspace)
\li \b Cpu in the form of basic scheduler objects (L4::Scheduler)
\li \b Vcon multiplexing for debug output (output only)
\li \b Virtual \b memory \b management for applications, L4Re::Rm
Moe further provides an implementation of L4Re name spaces (L4Re::Namespace),
which are for example used to provide a read only directory of all multi-boot
modules. In the case of a boot loader, like grub that enables a VESA frame
buffer, there is also a single instance of an L4Re graphics session
(L4Re::Goos).
To start the system Moe starts a single ELF program, the init process. The
init process (usually Ned, see the next section) gets access to all resources
managed by Moe and to the Sigma0 root pager interface.
For more details see \subpage l4re_servers_moe "Moe, the Root-Task".
Ned, the Default Init Process
=============================
To keep the root task free from complicated scripting engines and to avoid
circular dependencies in application startup (that could lead to dead locks)
the configuration and startup of the real system is managed by an extra task,
the init process.
Ned is such an init process that allows system configuration via Lua scripts.
For more information see \subpage l4re_servers_ned "Ned".
Io, the Platform and Device Resource Manager
============================================
Because all peripheral management in L4Re is done in user-level
applications, there is the need to have a centralized management of
the resources belonging to the platform and to peripheral devices.
This is the job of Io. Io provides portable abstractions for iterating and
accessing devices and their resources (IRQ's, IO Memory...), as well as
delegating access to those resources to other applications (e.g., device
drivers).
For more details see \subpage io "Io, the Io Server".
Other Servers
=============
The following additional server package are available on top of the core
L4Re environment.
- Rtc, the Real-Time Clock Server
is a simple multiplexer for real-time clock hardware on your platform.
- fb-drv, the Low-Level Graphics Driver
provides low-level access and initialization of various
graphics hardware. It has support for running VESA BIOS calls on Intel x86
platforms, as well as support for various ARM display controllers.
`fb-drv` provides a single instance of the L4Re::Goos interface and can
serve as a back end for the Mag server, in particular, if there is no graphics
support in the boot loader.
*/

94
src/l4/doc/source/tutorial.dox Normal file
View File

@@ -0,0 +1,94 @@
/**
\page l4re_tutorial Tutorial
This tutorial assumes that the reader is familiar with the basic %L4 concepts
that were discussed in the \ref l4re_intro section.
Here you can find the first steps to boot a very simple setup. The setup
consists of the following components:
\li L4Re Microkernel
\li Sigma0 --- Root Pager
\li Moe --- Root Task
\li Ned --- Init Process
\li hello --- The classical 'Hello World' Application
The guide assumes that you already compiled the base components and describes
how to generate an ISO image, with GRUB as a boot loader, that can for
example be booted within QEMU.
First you need a \c modules.list file that contains an entry for the scenario.
\code
modaddr 0x002000000
entry hello
kernel fiasco -serial_esc
roottask moe rom/hello.cfg
module l4re
module ned
module hello.cfg
module hello
\endcode
This file describes all the binaries and scripts to put into the ISO image,
and also describes the GRUB \c menu.lst contents. What you need to do is to
set the \c make variable \c MODULE_SEARCH_PATH to contain the path to your
L4Re Microkernel's build directory and the directory containing your \c hello.cfg
script.
The \c hello.cfg script should look like the following. A ready to use
version can be found in l4/conf/examples.
\code
local L4 = require("L4");
L4.default_loader:start({}, "rom/hello");
\endcode
The first line of this script ensures that the \c L4 package is available
for the script. The second line uses the default loader object defined in that
package and starts the binary \c rom/hello.
\note All modules defined in \c modules.list are available as data spaces
(L4Re::Dataspace) and registered in a name space (L4Re::Namespace). This
name space is in turn available as 'rom' to the init process
(\ref l4re_servers_ned "Ned").
Now you can go to your L4Re build directory and run the following command.
\note The example assumes that you have created the \c modules.list and \c
hello.cfg files in the /tmp directory. Adapt if you created them
somewhere else.
\code
make grub2iso E=hello MODULES_LIST=/tmp/modules.list MODULE_SEARCH_PATH=/tmp:<path_to_fiasco_builddir>
\endcode
Now you should be able to boot the image in QEMU by running:
\code
qemu-system-x86_64 -m 1024 -cdrom images/hello.iso -serial stdio
\endcode
If you press `<ESC>` in the terminal that shows you the serial output you
enter the microkernel's debugger... Have fun.
\section customizations Customizations
A basic set of bootable entries can be found in \c l4/conf/modules.list. This file
is the default for any image creation as shown above. It is recommended that
local modification regarding image creation are done in
\c conf/Makeconf.boot. Initially you may copy \c Makeconf.boot.example to
\c Makeconf.boot. You can overwrite \c MODULES_LIST to set your own
modules-list file. Set \c MODULE_SEARCH_PATH to your setup according to the
examples given in the file.
When configured a \c make call is reduced to:
\code
make grub2iso E=hello
\endcode
All other local configuration can be done in a
\c Makeconf.local file located in the \c l4 directory.
*/