Skip to content

docs: trivial fixes #533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
yf13 wants to merge 1 commit into
base: main
Choose a base branch
from
+2 −1
Open

docs: trivial fixes #533

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion docs/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1811,6 +1811,7 @@ At build-time, the Microkit tool embeds the capDL specification that describe
all kernel objects that needs to be created. Then for each kernel object, the spec
describe what state they need to be in and what capabilities exist to that object
(i.e. who has access to this kernel object). For example, the spec would specify the:

- starting Instruction Pointer (IP), Stack Pointer (SP) and IPC buffer pointer of a Thread Control Block (TCB),
- page table structure and mapping attributes of an address space (VSpace),
- interrupts (IRQ),
Expand Down Expand Up @@ -1862,7 +1863,7 @@ In order to do this however, the Microkit tool needs to emulate how the seL4 ker
to obtain the list of free untyped objects that the kernel would give to the initial task.

While this is non-trivial to do, it comes with the useful property that if the tool
produces a valid image, there should be no errors upon initialising the system
produces a valid image, there should be no errors upon initialising the system.
If there are any errors with configuring the system (e.g running out of memory),
they will be caught at build-time. This can only reasonably be done due to the
static-architecture of Microkit systems.
Loading