Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
This way common error codes can be in their own file.
To use, add the xmlns:xi="http://www.w3.org/2001/XInclude
attribute to the top level node and use:
<xi:include href="file-to-include.xml"/>
The content of the file will be included verbatim.
Include files must be complete XML documents, but without
<?xml version="1.0" ?> at the top. Practically this means
all nodes within the file need to be contained in one root
element.
Caveat: There is no proper dependency for Xincludes files in
the Makefile, so you need to do make clean after changing an
included XML file!
Signed-off-by: Indan Zupancic <indan@nul.nu>
Currently the seL4_VCPUReg enum only defines the seL4_VCPUReg_VMPIDR_EL2
register when the kernel is configured for SMP. This register should be
available for unicore systems too as otherwise a user level VMM is not
able to control the value of MPIDR_EL1 that the guest VM reads.
Signed-off-by: Kent McLeod <kent@kry10.com>
Disambiguate (for the reader) between normal and mcs versions of
SetSpace in the manual. This does not yet solve doxygen confusion.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide seL4_BootInfoFrameSize (and seL4_BootInfoFrameBits) for
userland, to there is no longer a need to hard-code the 4 KiByte
assumption.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Additional header files may now be included in non-C contexts and so we
need to guard some C definitions with the __ASSEMBLER__ guards
convention.
Signed-off-by: Kent McLeod <kent@kry10.com>
Some slot positions in the rootnode would depend on configuration.
However that makes it difficult to add new root caps, especially if
multiple caps only exist based on configuration. Make all caps always
there, but null if not configured.
Signed-off-by: Robbie VanVossen <robert.vanvossen@dornerworks.com>
Now the vspace_cap is used for all vspace roots and all other page
tables are referred to by page table caps.
Signed-off-by: Kent McLeod <kent@kry10.com>
Guard the new implementation of 64-bit x86 guests behind a config
option. This is done so that existing projects that use x86_64 hosts
with ia32-bit guests can continue to be supported until either the old
feature is preferred to be deprecated, or support can be added to
support both simmultaneously.
Signed-off-by: Kent McLeod <kent@kry10.com>
This commit combines a number of smaller commits which do the following:
* Enter IA-32e mode when running a 64-bit host
* Handle additional general purpose registers in 64-bit mode
* Handle 64-bit specific MSR events
* Properly save and restore FS, GS, and Shadow GS registers
CCDC-GVSC DISTRIBUTION A. Approved for public release; distribution
unlimited. OPSEC#4481.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
__builtin_offsetof is not part of the verification C subset -- avoid
accidental use by not declaring a macro for it and filter out the
single use by explicitly marking it as invisible to verification.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a `--form_file <file>` option to the bitfield generator for
printing a `/* generated from <file> */` message in a comment.
Use this option in cmake to provide the original source .bf file before
preprocessing so it's easier to find out where the corresponding
definitions are.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This header file is shared by kernel and userland. We can control the
kernel compiler setting, but userland might use an arbitrary setup.
Put a safeguard in place that things works as expected.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The "excluding extra refills" was confusing. seL4_CoreSchedContextBytes
is the size of sched_context_t + minimum refills, excluding any extra
refills.
We'd write it that way, but sched_context_t is not in scope in this
file.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Currently, building `libsel4` as a static library with `KernelIsMCS`
enabled fails with the following error:
```
static declaration of 'seL4_NBWait' follows non-static declaration
```
This [was mentioned][1] in the original PR that modified exported
functions to use `LIBSEL4_INLINE_FUNC`.
[1]: https://github.com/seL4/seL4/pull/101#issuecomment-442010551
Signed-off-by: Klim Tsoutsman <klim@tsoutsman.com>
This adds support for the Pine64 Quartz64 and other devices based on
the Rockchip RK3566. The platform support is adapted from the
Rockpro64 code, except that the RK356x has A55 cores, and adjusting
for the fact that the ARM Generic Timer is the only on-chip timer
available.
Signed-off-by: Peter S. Housel <housel@acm.org>
This also adds a compile assert for checking that MinSchedContextBits
is the correct size in relation to seL4_CoreSchedContextBytes.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Add a comment that they are empty on purpose. They are not removed to
keep the infrastructure in case there will be deprecated items in the
future.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The MCS-related macros were causing the build to fail when configured to
use the sysenter instruction. Additionally, some message registers
weren't explicitly being passed to the assembly block for
seL4_NBSendRecv in this configuration.
Signed-off-by: Jimmy Brush <code@jimmah.com>
For writing/reading/copying TCB registers, the
arch_flags parameter is not used on RISC-V (in
addition to x86 and ARM).
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Now that there is no need to reserve page table entries in each VSpace
object, the full architecture specified address space range is usable.
Signed-off-by: Kent McLeod <kent@kry10.com>
The condition element currently exists parallel
to the condition attribute. The condition attribute
should be removed in a subsequent patch.
Signed-off-by: matt rice <ratmice@gmail.com>
This patch restricts mixed-content elements from ANY
to the various leaf nodes which are used.
This is intended to allow for easier parsing in languages with
no recursive datatypes like rust.
Since they no longer have to handle things like
'<description> text
<description>more text</description>
<description>'
which the dtd allowed for, but never used.
tested with:
for i in {libsel4/arch_include/*/interfaces/,\
libsel4/include/interfaces/,\
libsel4/sel4_arch_include/*/interfaces}/*.xml;
do
xmllint --noout --dtdvalid libsel4/tools/sel4_idl.dtd $i;
done
Signed-off-by: matt rice <ratmice@gmail.com>
This adds an alternative script for syscall_stub_gen.py
syscall_stub_gen_rs.py was initially derived from Robigalia project
which can be found here: https://gitlab.com/robigalia/sel4-sys
However, this is no longer compatible.
The script is intended to be used with a proper sel4-sys crate
in order to allow Rust applications to interface with the seL4 API.
Signed-off-by: Wojciech Sipak <wsipak@antmicro.com>
Signed-off-by: Karol Gugala <kgugala@antmicro.com>
