From 8c111818a263857791d60c193445e74260433aa9 Mon Sep 17 00:00:00 2001 From: Stephen Sherratt <Stephen.Sherratt@nicta.com.au> Date: Wed, 4 May 2016 15:31:30 +1000 Subject: [PATCH] manual: Reword some cspace explanation for clarity --- manual/parts/cspace.tex | 10 +++++----- manual/parts/objects.tex | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/manual/parts/cspace.tex b/manual/parts/cspace.tex index 78e274554..5b7802489 100644 --- a/manual/parts/cspace.tex +++ b/manual/parts/cspace.tex @@ -49,7 +49,7 @@ managers of untyped memory to destroy the objects in that memory so it can be retyped. seL4 requires the programmer to manage all in-kernel data structures, -including C\-Spaces, from userspace. This means that the userspace +including CSpaces, from userspace. This means that the userspace programmer is responsible for constructing CSpaces as well as addressing capabilities within them. This chapter first discusses capability and CSpace management, before discussing how capabilities @@ -310,10 +310,10 @@ a capability address must be efficient. Therefore, CSpaces are implemented as \emph{guarded page tables}. % FIXME: need a references to justify the above decision -As explained earlier, a CSpace is simply a hierarchy of \obj{CNode} -objects, and each \obj{CNode} is simply a table of slots that each -contain either a capability or a reference to another \obj{CNode}. The -kernel stores a capability to the root \obj{CNode} of each thread's +As explained earlier, a CSpace is a directed graph of \obj{CNode} +objects, and each \obj{CNode} is a table of slots, where each slot can +either be empty, or contain a capability, which may refer to another \obj{CNode}. +The kernel stores a capability to the root \obj{CNode} of each thread's CSpace in the thread's TCB. Conceptually, a \obj{CNode} capability stores not only a reference to the \obj{CNode} to which it refers, but also carries two values, its \emph{guard} and \emph{radix}. diff --git a/manual/parts/objects.tex b/manual/parts/objects.tex index fb61b4061..ecfab939f 100644 --- a/manual/parts/objects.tex +++ b/manual/parts/objects.tex @@ -72,8 +72,8 @@ capability system, where capabilities are managed by the kernel. Capability spaces are implemented as a directed graph of kernel-managed \emph{capability nodes} (\obj{CNode}s). A \obj{CNode} is a table of slots, where each slot may contain further \obj{CNode} capabilities. An -address in a capability space is then the concatenation of the indices -of the \obj{CNode} capabilities forming the path to the destination +address of a capability in a capability space is the concatenation of the indices +of slots within \obj{CNodes} forming the path to the destination slot; we discuss \obj{CNode} objects in detail in \autoref{ch:cspace}. Capabilities can be copied and moved within capability spaces, and -- GitLab