From 273c1e57406cb56e7a431adbf1d87f097d7ae130 Mon Sep 17 00:00:00 2001 From: Craig Christianson <48270982+craigc01@users.noreply.github.com> Date: Wed, 12 Jul 2023 18:33:43 -0600 Subject: [PATCH 1/2] Update capabilities.md Added a lost parenthesis and added clarity on the << symbol. Signed-off-by: Craig Christianson <48270982+craigc01@users.noreply.github.com> --- tutorials/capabilities/capabilities.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md index 8fd0322d..98d39752 100644 --- a/tutorials/capabilities/capabilities.md +++ b/tutorials/capabilities/capabilities.md @@ -96,9 +96,9 @@ By convention the 0th CSlot is kept empty, for the same reasons as keeping NULL process virtual address spaces: to avoid errors when uninitialised slots are used unintentionally. The field `info->CNodeSizeBits` gives a measure of the size of the initial -CNode: it will have `1 << CNodeSizeBits` CSlots. A CSlot has +CNode: it will have `1 << CNodeSizeBits` CSlots where the `<<` symbol represents the left bit shift operator. A CSlot has `1 << seL4_SlotBits` bytes, so the size of a CNode in bytes is -`1 << (CNodeSizeBits + seL4_SlotBits`. +`1 << (CNodeSizeBits + seL4_SlotBits)`. ### CSpaces From ce951e59397e35cf37e72783db11886d7a10aaff Mon Sep 17 00:00:00 2001 From: Craig Christianson <48270982+craigc01@users.noreply.github.com> Date: Tue, 18 Jul 2023 10:27:58 -0600 Subject: [PATCH 2/2] Update capabilities.md Changed 1>>N notation to 2^N notation --- tutorials/capabilities/capabilities.md | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md index 98d39752..0e8a2933 100644 --- a/tutorials/capabilities/capabilities.md +++ b/tutorials/capabilities/capabilities.md @@ -32,15 +32,15 @@ By the end of this tutorial, you should be familiar with: ### What is a capability? -A *capability* is a unique, unforgeable token that gives the possessor -permission to access an entity or object in system. One way to think of a +A *capability* is a unique, unforgeable token that gives the possess +permission to access an entity or object in the system. One way to think of a capability is as a pointer with access rights. There are three kinds of capabilities in seL4: * capabilities that control access to kernel objects such as thread control blocks, * capabilities that control access to abstract resources such as `IRQControl`, and -* untyped capabilities, that are responsible for memory ranges and allocation - from those (see also the [Untyped] tutorial). +* untyped capabilities that are responsible for memory usage, mapping, and allocation +(see also the [Untyped] tutorial). [untyped]: https://docs.sel4.systems/Tutorials/untyped.html @@ -92,13 +92,17 @@ Each CSlot in a CNode can be in the following state: * empty: the CNode slot contains a null capability, * full: the slot contains a capability to a kernel resource. -By convention the 0th CSlot is kept empty, for the same reasons as keeping NULL unmapped in +By convention the 0th CSlot is kept empty, for the same reasons as keeping NULL unmapped in process virtual address spaces: to avoid errors when uninitialised slots are used unintentionally. -The field `info->CNodeSizeBits` gives a measure of the size of the initial -CNode: it will have `1 << CNodeSizeBits` CSlots where the `<<` symbol represents the left bit shift operator. A CSlot has -`1 << seL4_SlotBits` bytes, so the size of a CNode in bytes is -`1 << (CNodeSizeBits + seL4_SlotBits)`. +In `src/main.c`, we define a variable called `info` which is of type `seL4_BootInfo`. This data structure +is defined in a file called `bootinfo_types.h` and provides us with usefull information about our +running process. The field `info->initThreadCNodeSizeBits` tells us the the number of CSlots in +the initial CNode. Notice that the variable name ends in `SizeBits`. This suffix generally tells us +that the number given is not the actual size, but the number of bits required to represent the actual +size. Written mathematically, our CNode has 2initThreadCNodeSizeBits CSlots. The constant `seL4_SlotBits` which is defined in a file called `constants.h` tells us that a single CSlot occupies +2seL4_SlotBits bytes. So, the total size of our CNode is +2(initThreadCNodeSizeBits + seL4_SlotBits) bytes. ### CSpaces