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>
Define CONFIG_KERNEL_LOG_BUFFER in the same way as all other kernel
config options so that it is present in autoconf.h
Signed-off-by: Kent McLeod <kent@kry10.com>
autoconf.h is expected to contain all defined config options for an seL4
build configuration. Having these redefinitions were leftover from when
the verification build system didn't produce an autoconf.h file and set
the config separately. Its more likely that these defaults would
incorrectly hide an include path misconfiguration and produce settings
that are inconsistent with the kernel's configuration.
Signed-off-by: Kent McLeod <kent@kry10.com>
- Add underscored in name to improve readability.
- Add brackets to ensure parameters are atoms
- add comment clarifying c99 usage
Signed-off-by: Axel Heider <axelheider@gmx.de>
This adds a flags parameter to SchedControl_Configure to enable
configuration of a sporadic SC.
This also allows flags to be added in the future as needed without
breaking the API.
This allows the user to configure an SC either to be constrained as a
sporadic task where accumulated time is only delayed to when a task has
become runnable (implementing the sporadic server algorithm) or
whenever the task becomes the current executing task (implementing the
sliding-window constraint as in constant-bandwidth servers).
This can be used to prevent non-realtime tasks from exceeding bandwidth
under any circumstances, even in an over-committed configuration, whilst
also allowing work-conserving tasks to be configured in the same system.
To implement sporadic servers, we need to ensure that the suspension of
a task cannot be used as a mechanism to amplify budget of a task by
granting that task access to effectively multiple periods worth of
replenishments within a single period.
To align the implementation of SCs with the model of sporadic servers we
must delay available time until the release of a task. Within seL4, a
release would be any time where an SC changes from not being associated
with a Running, RunningVM, or Restart thread to one that is.
This can occur when an SC is bound to a new thread in such a state or
when a thread changes to such a state from any non-running states.
Critically, replenishments should not be delayed at the point when an SC
becomes the current SC (as was the case prior to this commit). This has
the effect of enforcing a continuous, constant bandwidth which is a
restriction that is incompatible with standard scheduling logic.
Accounting for this requires inserting a new refill_unblock_check
call whenever a sporadic SC is unblocked and removing the
refill_unblock_check call from when said SC is scheduled.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This provides a generic way to print an seL4_Word on 32-bit and 64-bit
platforms, aligned with PRIu64 and friends. Use it as:
printf("foo = %" PRI_sel4_word "\n", (seL4_Word)foo);
Signed-off-by: Axel Heider <axelheider@gmx.de>
Today the file autoconf.h is created by the CMake build system and thus
HAVE_AUTOCONF is always defined. Time to get rid of some legacy by
removing the check if HAVE_AUTOCONF is set.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This option was legacy from when autoconf.h wasn't always present in the
include path. Now it causes incorrect configuration options.
Signed-off-by: Kent McLeod <kent@kry10.com>
This symbol definition leads to an additional thread local storage
allocation for each object file that includes this header file. Then
when the final executable is linked, the weak symbol references are all
replaced by the global symbol declared by libsel4 in sel4_bootinfo.c.
The net result is unnecessarily large thread local storage being
required for each thread.
Signed-off-by: Kent McLeod <kent@kry10.com>
This makes the kernel configuration defaults public and known to the
user level. Generally shouldn't depend on these definitions outside of
code testing and benchmarking the kernel.
Signed-off-by: Curtis Millar <curtis@curtism.me>
Adding the master control caps that are used to create transaction
and context banks caps. This commit includes the internal kernel
structure that required to manage any created transaction and
context bank caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
