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>
A CPointer addressing a CNode is accompanied by a depth limit. The
manual describes the depth limit as the length of a big-endian prefix of
the CPointer, whereas the specification and implementation treat the
depth limit as the length of a big-endian suffix.
This commit corrects the manual to match the specification.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
- Add a chapter in the Hardware I/O Section
- Link API documentation back to chapter.
Co-authored-by: Qian Ge <Qian.Ge@data61.csiro.au>
Signed-off-by: Kent McLeod <kent@kry10.com>
The initial thread's CNode guard size is calculated so that the CNode
resolves the number of bits in the architecture word size.
Signed-off-by: Jimmy Brush <code@jimmah.com>
The concept of system criticality has been removed from the kernel.
This commit removes a last remnant of it from the manual.
Fixes github issue #240
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
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.
For some reason the kernel documented and maintained constants for a
512MiB 'huge page' in riscv32 which is not part of the specification.
The references and constants are removed
...and other tweaks.
* Clarify the synonymy of Receive and Wait on non-MCS systems.
* Note that Receive takes a reply object on MCS systems, and not on
non-MCS systems. Also note redundancy of Wait on non-MCS systems.
* Use the full English word "Receive" when the discussion is at the
conceptual level. It still gets abbreviated in C context, where it also
receives the "seL4_" prefix.
* Try a little harder to explain what's the same and what's different
about a non-MCS "reply capability" and an MCS capability to a reply
object.
* Explain what MCS stands for at the beginning of the chapter. In the
manual's current organisation, this precedes by a few paragraphs the
term's first occurrence.
* Recast language about things being "on the MCS kernel" in favour of
describing "MCS" and "non-MCS" _configurations_ of the kernel. (We do
not refer to the "master" kernel in the manual--thankfully.)
* Correct doubled word "to to".
* Italicise "reply capability" to better distinguish it from the
(already italicised) "reply object".
* Add a TODO comment about hyphenation grief.
* Recast language of introduction to system calls.
* Rearrange system calls to present them in a more pedagogically useful
order.
* Add TODO comment for future manual organisation efforts.
- Remove Remap function from seL4 API for arm, x86, riscv and the
respective invocation implementation.
- Update Map as replacement for Remap
- Update manual
This allows a change of rights if the frame being mapped is already
mapped in at the given vaddr. To map a page to a different address,
unmap it first.
Co-authored-by: Hesham Almatary <hesham.almatary@data61.csiro.au>
Co-authored-by: Anna Lyons <Anna.Lyons@data61.csiro.au>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
This allows users to define custom amounts of refills without
increasing the scheduling context size system wide.
also add libsel4 functions for refill size
Previously the manual would only parse the doxygen for a single xml
file, which meant references to symbols on other files would break.
Parse all doxygen files when constructing the ref dict to fix this.
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.
Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
GrantReply is a new access right added to endpoint capabilities, which
allows seL4_Call to be used on those capabilities (specifically, it
allows reply caps *only* to be granted across endpoints).
Prior to the addition of GrantReply, endpoint capabilities required the
Grant access right, which allowed any arbitrary capabilitiy to be
transferred over an endpoint. Using GrantReply, systems can now be
constructed where threads using seL4_Call over an endpoint do not need to be in the same
security subsystem.
This change updates the vspace chapter to separate the high-level concept of a VSpace from the
architectually defined objects. It also updates the various names for the vspace parameter to all be
vspace.
- instead of referring to only PDs and PTs, use generic language about paging structures
- link to each architectures methods
- create tables that show the info for all archictures
- increases the maintainability of the docs
- move descriptions of methods to the API reference
- remove hardcoded invocations in manual
This commit removes the content completely from vspace.tex, as it is out of date and needs
restructuring. The next commit does the restructuring.
