From c77611a25d135875cc7204d945bcee5beef26ae7 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 5 Jul 2026 12:57:06 +1000 Subject: [PATCH] capabilities: attempts at slightly clearer prose - "possessor" has confused people before; simplify the sentence - fix typo (missing 'the') - avoid passive tense and 0th in the CSlot 0 sentence; rewrite into two sentences for more clarity - mention what `info` is, trying to keep it brief, and add a reminder that `1 << x` means 2^x With thanks to Craig Christianson for the material in PR #102. Signed-off-by: Gerwin Klein --- tutorials/capabilities/capabilities.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md index 2b5e718..5c8a3ac 100644 --- a/tutorials/capabilities/capabilities.md +++ b/tutorials/capabilities/capabilities.md @@ -36,8 +36,8 @@ Answers are also available in drop down menus under each section. ### 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 constitutes a +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: @@ -96,12 +96,15 @@ 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 - process virtual address spaces: to avoid errors when uninitialised slots are used unintentionally. +By convention, most libraries keep the CSlot at index 0 empty, so that using an +uninitialised slot variable produces an explicit error. This is similar to +leaving NULL unmapped in a process's virtual address space. -The field `info->CNodeSizeBits` gives a measure of the size of the initial -CNode: it will have `1 << CNodeSizeBits` CSlots. A CSlot has -`1 << seL4_SlotBits` bytes, so the size of a CNode in bytes is +The structure `info` of type `seL4_BootInfo` in the example code contains +information the kernel provides to the initial task. The field +`info->CNodeSizeBits` in this structure is the *size in bits* of the initial CNode: +the initial CNode has `1 << CNodeSizeBits` (i.e. 2CNodeSizeBits) CSlots. +A CSlot has `1 << seL4_SlotBits` bytes, so the size of this CNode in bytes is `1 << (CNodeSizeBits + seL4_SlotBits)`. ### CSpaces