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>
These files should have been released under BSD-2-Clause in the first
place (as per parent LICENSE.md file).
Closes#245
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
With clang 11 these become bss symbols rather than commons, resulting in
multiple definition errors at link time. gcc 10 is likely to expose the
same issue.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
- seL4_BenchmarkDumpAllThreadsUtilisation: Prints a JSON formatted
record of total and per-thread utilisation statistics about the system.
This currently includes a thread's total cycles scheduled, total number
of times scheduled, total cycles spent in the kernel and total number of
times entering the kernel and then totals of each for all threads on the
current core.
- seL4_BenchmarkResetAllThreadsUtilisation: Resets the current counts of
every user thread on the current core.
These syscalls are only available in a Debug build configuration as they
use a kernel debug list of all of the threads that exist for a given
node.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
For each thread also track number of times scheduled, number of kernel
entries and amount of cycles spent inside the kernel. Also add
core-wide totals for each.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
The format string in userError is now written to
the IPC buffer for debugging purposes.
This requires an snprintf which reuses vprintf with
a new structure for handling how output is done.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
Translation validation reports errors using the "real" struct type name
instead of the typedef name, so having anonymous structs makes debugging
translation validation harder.
Relates to #168. The definition for `seL4_UntypedRetypeMaxObjects` lives
in the UAPI `types.h` but appears to have no link to the value actually
used by the kernel, which is configurable. This change sets the UAPI
definition to the generated definition from the kernel config steps and
defaults to the previous fixed value if, for some reason, the configured
definition is not available.
Use the __ASSEMBLER__ macro to suppress C definitions from appearing in
non-C files when the preprocessor is used. Other libsel4/*/constants.h
files use this strategy to avoid duplicating definitions for seL4 object
sizes that can changed based on kernel configuration.
- seL4_TCB_Configure no longer takes a fault endpoint.
- seL4_TCB_SetSpace takes a cap in the callers cspace for the
fault endpoint, not the target tcbs.
- seL4_TCB_SetSchedParams now also takes a fault endpoint as above.
This change installs the fault endpoint cap into the tcb cnode
first validating it.
This means either of the functions that set it will now return an error
if the cap is not either a null cap or an endpoint with send and
grant rights.
Significantly, the cap passed to the function should be in the callers
cspace, not the target tcbs.
This allows users to define custom amounts of refills without
increasing the scheduling context size system wide.
also add libsel4 functions for refill size
This is the first part of the seL4 MCS. This commit:
* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.
Created a new syscall, seL4_DebugSendIPI for ARM to send arbitrary SGIs
(software generated interrupts) to arbitrary cores. As SGIs are
specifically PPIs (private interrupts), this syscall effectively allows
to trigger PPIs on arbitrary cores, for debug/testing purposes.
Some platforms and configurations do not allow user code to change the
value of the register used for TLS. On these architectures a syscall can
be used to allow the kernel to update the register on their behalf.
This does not immediately update the value in the user context on many
configurations as the values are only stored in the user context on a
context switch.
This removes the assumption that each platform sotres the IPC buffer
address in a platform-specific register. The IPC buffer address is
instead stored in a thread-local variable in libsel4 which must be
initialised by the runtime.
