Skip to content

Commit e1cfa13

Browse files
docs update
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
1 parent f3e6aa8 commit e1cfa13

File tree

2 files changed

+15
-18
lines changed

2 files changed

+15
-18
lines changed

DEVELOPER.md

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -108,15 +108,13 @@ When you build the SDK, provide an extra argument `--toolchain-prefix-riscv64 ri
108108
The SDK includes a binary of the seL4 kernel.
109109
During the SDK build process the kernel is build from source.
110110

111-
At this point in time there are some minor changes to the seL4 kernel required for Microkit. This is temporary, more details can be found [here](https://github.com/seL4/microkit/issues/52).
112-
113111
Please clone seL4 from:
114112

115113
https://github.com/seL4/seL4.git
116114

117-
The correct branch to use is `microkit`.
115+
The correct branch to use is `master`.
118116

119-
Testing has been performed using commit `3aafe9e0b9527794c547d12090117e1000302da0`.
117+
Testing has been performed using commit `b60b6652a47f4e749d06fbdb9dd7b5d074625b03`.
120118

121119
## Building the SDK
122120

docs/manual.md

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1183,8 +1183,11 @@ PCIDs not supported by the processor
11831183
```
11841184

11851185
@billn continue
1186+
11861187
@billn directing the user to write grub stanzas and stuff is a bit complicated, how about we build a bootable ISO from the tool?
11871188

1189+
@billn GRUB is also not Mac friendly, maybe recommend users to use something like Limine instead?
1190+
11881191
## ZCU102 {#zcu102}
11891192

11901193
The ZCU102 can run on a physical board or on an appropriate QEMU based emulator.
@@ -1289,9 +1292,6 @@ For the kinds of systems targeted by the Microkit, this reduction of the usable
12891292
The limitation on the size of by-value arguments is forced by the (architecture-dependent) limits on the payload size of the underlying seL4 operations, as well as by efficiency considerations.
12901293
The protected procedure payload should be considered as analogous to function arguments in the C language; similar limitations exist in the C ABIs (Application Binary Interfaces) of various platforms.
12911294

1292-
\
1293-
\
1294-
12951295
## Limits
12961296

12971297
The limitation on the number of protection domains in the system is relatively arbitrary.
@@ -1318,32 +1318,30 @@ correspond to PD program images to the Microkit tool which is responsible to
13181318
for packaging everything together into a single bootable image for the target
13191319
platform.
13201320

1321-
This final image contains a couple different things:
1321+
On ARM and RISC-V, this final image contains a couple different things:
13221322

13231323
* the Microkit loader
13241324
* seL4
1325-
* the Monitor (and associated invocation data)
1326-
* the images for all the user's PDs
1325+
* the capDL initialiser (and associated capDL specification)
13271326

13281327
When booting the image, the Microkit loader starts, jumps to the kernel, which
1329-
starts the monitor, which then sets up the entire system and starts all the PDs.
1328+
starts the capDL initialiser, which then sets up the entire system and starts all the PDs, including the Monitor.
1329+
1330+
On x86, the tool produces a boot module that only contains the capDL initialiser.
1331+
The seL4 kernel image is distributed as part of the SDK. You must bring your own
1332+
Multiboot 2 compliant bootloader which then loads the kernel and boot module.
13301333

13311334
Now, we will go into a bit more detail about each of these stages of the
13321335
booting process as well as what exactly the Microkit tool is doing.
13331336

1334-
## Loader
1337+
## Loader (ARM and RISC-V)
13351338

13361339
The loader starts first, it has two main jobs:
13371340

1338-
1. Unpack all the parts of the system (kernel, monitor, PD images, etc) into
1341+
1. Unpack all the parts of the system (kernel and capDL initialiser) into
13391342
their expected locations within main memory.
13401343
2. Finish initialising the hardware such that the rest of the system can start.
13411344

1342-
Unpacking the system image is fairly straight-forward, as all the information
1343-
about what parts of the system image need to go where is figured out by the
1344-
tool and embedded into the loader at build-time so when it starts it just goe
1345-
through an array and copies data into the right locations.
1346-
13471345
Before the Microkit loader starts, there would most likely have been some other
13481346
bootloader such as U-Boot or firmware on the target that did its own hardware
13491347
initialisation before starting Microkit.
@@ -1358,6 +1356,7 @@ that will not be done by a previous booting stage, such as:
13581356
Once this is all completed, the loader jumps to seL4 which starts executing.
13591357
The loader will never be executed again.
13601358

1359+
@bill continue fixing below
13611360
## Monitor
13621361

13631362
Once the kernel has done its own initialisation, it will begin the

0 commit comments

Comments
 (0)