At the moment, the seL4 microkit does not setup TLS variable
support. The workaround has been to `#define __thread` (blank)
before including `<sel4/sel4.h>` in `<microkit.h>`, which causes
issues if `<microkit.h>` is included *after* `<sel4/sel4.h>`,
often with obscure linker errors to `__emutls_**` symbols.
Instead we add a libsel4 config option that allows us to build
it with __thread copied out. We introduce an LIBSEL4_THREAD_LOCAL
macro in a similar way to the existing LIBSEL4_INLINE macro.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Not all platforms are 512-byte aligned. Specifically, 64-bit
platforms are 1024-byte byte aligned.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
SEL4_VMENTER_CALL_CONTROL_ENTRY_MR refers to the
VM Entry Interruption-Information Field of the VMCS [1].
Not the VM-Entry Controls, which are two different things.
[1]: src/arch/x86/object/vcpu.c: vcpu_update_state_sysvmenter()
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
In the definition of tcb_t, there's extra fields if there's
SMP or BENCHMARK_TRACK_UTILISATION or ARM_HYPERIVSOR_SUPPORT.
It looks like the combination of all three (which Microkit uses)
is not enough for 11 bits.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Otherwise it is not possible to send SGIs to all cores on platforms
with non-contiguous Affinity values or more than 16 cores.
16 is the limit of the target list, which is only relevant when
sending an SGI to multiple targets at once.
Update the API documentation to reflect what's actually happening.
Signed-off-by: Indan Zupancic <indan@nul.nu>
There's a few cases in the kernel where the ksKernelEntry tracking
is not perfect, such as in SError reporting, and (I believe) a few
other places which I haven't tracked down to a cause - but some of
e.g. the RISC-V trap code where the first entry faults and the 2nd
proceeds can report stale information.
In these cases, the kernel says that the entry was via a certain
syscall or interrupt (etc), even though that was clearly not the
case because we know the kernel exited. Now we will print out this:
halting...
Kernel entry via Unknown (0)
The changes:
- When exiting the kernel, via `c_exit_hook()`, reset
`ksKernelEntry.path` to "Unknown".
An alternative here would have been add a global "valid" boolean
to the kernel state, but this requires modifying every site where
we set the ksKernelEntry.path to also set valid = true, which is
ugly.
- Remove Entry_UnimplementedDevice from entry_type_t as it is never
used, to leave enough room to add Entry_Unknown.
- Switch out the CONFIG_DEBUG_BUILD || BENCHMARK TRACK ENTRIES #if
in the x86 breakpoint code with the more concise
`TRACK_KERNEL_ENTRIES` define used elsewhere.
Signed-off-by: julia <git.ts@trainwit.ch>
This was missed in cb8ee83f0cd2268b1d6b1cd5ca30b031db5896c4; their
use was removed from syscall_stub_gen but their typedefs remained.
Signed-off-by: julia <git.ts@trainwit.ch>
Add flags to tcb_t and the seL4_TCBFlag_fpuDisabled flag.
Enums are signed, make TCB flags word_t to make it unsigned.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Allow SGIs to be generated from non-SMP kernels.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The SiFive Premier P550 [1] is a new development board from SiFive
that is based on the ESWIN EIC7700X SoC.
The platform is interesting to the seL4 community as it implements
the RISC-V hypervisor extension meaning we now have real hardware to
evaluate RISC-V hypervisor changes to seL4. It also implements the
Sscofpmf extension and so we'll be able to get more experiment with
proper profiling on RISC-V.
Unfortunately, it seems we still do not have proper ASID suppor
according to [2].
The board comes in two configurations, 16GB and 32GB of memory.
This adds support for the 16GB model.
The DTS comes from SiFive's fork of Linux [3].
No modifications were made, any extra things are in the overlay.
[1]: https://www.sifive.com/boards/hifive-premier-p550
[2]: https://forums.sifive.com/t/asid-vmid-support-in-p550-eic7700x/6887
[3]: https://github.com/sifive/riscv-linux/tree/dev/kernel/hifive-premier-p550
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Save and restore the CNTKCTL register alongside other virtual timer
registers when switching VCPUs.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
This introduces two new constants to the vcpu reg enum, with the goal of
unifying reg range saves/restores and making explicit which registers
are affected.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
seL4_VCPUReg_CPACR was sometimes saved to an inactive current VCPU,
overwriting the previous value and erroneously enabling FPU access.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Compatibility with versions <3.10 is going away.
As it happens, we're not using any CMake features that have changed
between 3.7 and 3.16, so bump the lowest version to 3.16.
Also remove the minimum version statement from the platform config
files --- they're all very simple files that are version independent;
and the version is checked elsewhere anyway.
Also, Fix style issue
A commit to fix style to make the PR go through.
Signed-off-by: Peter Chubb <Peter.Chubb@unsw.edu.au>
Nowhere else in the documentation uses the phrase
"Must be a depth of 32"
which seems incorrect for 64-bit riscv.
Also, the index parameter had the same description as root, which
is incorrect.
Signed-off-by: julia <git.ts@trainwit.ch>
This configuration is not in CI (hence why it lead to
a build error in the first place) so I just tested
it locally via sel4test with:
```
../init-build.sh -DPLATFORM=qemu-riscv-virt \
-DMCS=1 -DKernelRiscvExtD=1 \
-DKernelRiscvExtF=1 -DRISCV32=1
```
and it passed.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This commit's parent renames the interface XML files.
The symlinks added in this commit serve to ease the transition to the
new names for downstream projects.
These links are added:
- include/interfaces/{sel4.xml -> object-api.xml}
- arch_include/*/interfaces/{sel4arch.xml -> object-api-arch.xml}
- sel4_arch_include/*/interfaces/{
sel4arch.xml -> object-api-sel4-arch.xml
}
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
This new platform is NXP Semiconductor's Evaluation Kit for the i.MX 8M
Plus Applications Processor. It's from the i.MX 8M family of processors
and is largely similar to the existing i.MX 8M Quad and i.MX 8M Mini
platforms.
Signed-off-by: Damon Lee <damon@kry10.com>
Check for CONFIG_ENABLE_SMP_SUPPORT instead of checking for the
number in CONFIG_MAX_NUM_NODES. This allows enabling SMP support
with just one node also.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
- fix: brackets in check
- fix: use CONFIG_ENABLE_SMP_SUPPORT
- conditions for CONFIG_MAX_NUM_NODES have been removed
Signed-off-by: Axel Heider <axel.heider@codasip.com>
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>
