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>
The concept of untyped object was confusing the description here, esp
when it comes to the CDT and what is derived from what. Also explain
when memory is actually zeroed, because that is important for where you
want to make sure that no confidential data remains in memory, for
instance.
This commit only affects the retype/revoke explanation and does not
attempt to clear up the concept of untyped object more generally.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Extra spaces are inserted after texttt tags when generating doxygen
comments in order to ensure that xmlonly tags are readable by doxygen.
The extra spaces cause a description like this:
```
Testing <texttt text="1"/>, 2, 3
```
To be rendered like this:
```
Testing 1 , 2, 3
```
This change identifies text runs that start with extra spaces and either
a period or a comma and removes the extra spaces, allowing at least
common punctuation to be rendered correctly.
Signed-off-by: Jimmy Brush <code@jimmah.com>
- resolve mix of service mechanism, abstraction
- update verification explanation + references
- remove reference to ARM11 which is slated to be discontinued
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The old draftcopy package doesn't seem to work on newer texlive
installations. We also don't want to pass `draft` to the `report`
style, because that will switch off images.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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).
