diff --git a/docs/manual.md b/docs/manual.md index c45eaae37..3e084e25b 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1177,9 +1177,9 @@ To boot a Microkit image, use a GDB prompt via openOCD per [seL4 Docs](https://d 2. Set the `a0` and `a1` registers for OpenSBI - # tell OpenSBI where DTB is (there is none) + (gdb) # tell OpenSBI where DTB is (there is none) (gdb) set $a0=0 - # tell OpenSBI that the default hart is #0 + (gdb) # tell OpenSBI that the default hart is #0 (gdb) set $a1=0 3. Load OpenSBI's FW_JUMP payload targeted at `0x90000000`, implicitly setting the program counter. @@ -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), @@ -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.