This is useful for sel4test et al for testing that a certain
PD has been succesfully migrated between cores, or that it
is running on a particular core.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
The actual libsel4 wrappers and kernel code only ever exists
when CONFIG_ENABLE_SMP_SUPPORT exists, so there's no point
also defining the syscall code as well.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
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>
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>
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>
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>
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>
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>
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>
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>
__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>
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>
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>
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>
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 reverts a small part of 1596aa5857 which unexpectedly broke the
binary verification frontend, because the verification tool chain
forces the enum to `int` instead of `long`.
See also seL4 issue #738 -- when that issue is solved, we may be
able to go back to the more specific type.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
* use enum for SEL4_BOOTINFO_HEADER_xxx
Also add more comments and use seL4_BootInfoID in seL4_BootInfoHeader.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Remove a userError that is present on mainline kernel but not on MCS.
seL4_ReplyRecv is often used in a loop to create an event handler. When
first entering this loop, or when handling signals from notifications,
there won't already be a pending caller blocked on the reply object. In
this case the kernel doesn't perform a reply transfer and continues with
the receive operation. This is a common operation and shouldn't result
in a userError being printed by the kernel each time the reply phase
ends up as a no-op.
Signed-off-by: Kent McLeod <kent@kry10.com>
Align the API wrapper guards with the kernel syscall implementation,
the function is available if CONFIG_ENABLE_SMP_SUPPORT is set instead
of depending on CONFIG_MAX_NUM_NODES.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Mutate cannot be used to badge endpoints (many years ago, before the
first public release, this was possible, but was removed).
Also explain why Mutate is not always replaceable with Mint+Delete.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add error conditions for the lazy bind of SchedContexts to
notifications or TCBs (introduced in e18e32e28e).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
