diff --git a/manual/parts/cspace.tex b/manual/parts/cspace.tex index 78e27455445eae645a75088ac5cd4d7199f857cc..5b7802489114186f3ce04a6b5775eceb1312ee6d 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 fb61b40617f34c9e5a3aad04ca2ec563b1162f05..ecfab939ff243fad5712b1043d254a645743d865 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