1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Glossary. Documentation only.
9
10
11
12This file is a running glossary of technical nouns used in
13documenting the abstract model.
14
15The entries should be listed alphabetically.
16Each has three details:
17   1. a short name, e.g. cnode
18   2. a long name, e.g. capability node
19   3. a reference to the section where it is first discussed.
20
21The long name (2) should only be used when the term is first
22discussed, i.e. at (3).
23It should be followed by the short name (1) in parantheses and a
24label command of the form: \label{glos:<shortname>}.
25That label should be used to generate the reference (3).
26
27e.g. A \emph{capability node} (cnode)\label{glos:cnode} is a ...
28
29A fourth optional argument can give additional information of one
30or more of the following types:
31   - names that should not be used.
32   - a list of historical terms that mean the same thing.
33*)
34
35chapter "Glossary"
36
37(*<*)
38
39theory Glossary_Doc
40imports "Syscall_A"
41begin
42
43(*>*)
44text \<open>
45\newcommand{\glossaryentry}[4][\null]
46    {\begin{list}{\null}{\setlength{\leftmargin}{0pt}
47                         \setlength{\rightmargin}{0pt}
48                         \setlength{\labelwidth}{0pt}
49                         \setlength{\itemindent}{0pt}
50                         \setlength{\topsep}{1.0em}}
51     \item  \parbox[t]{.18\textwidth}{\raggedright{\bf #2}}%
52            \hfill\parbox[t]{.75\textwidth}{\raggedright{#3}}%
53            \hfill\parbox[t]{.05\textwidth}{\raggedright{%\autoref{#4}
54}}%
55     \ifx#1\null\relax\else%
56        \item\nopagebreak\hfill
57             \begin{minipage}[t]{.775\textwidth}{\it #1}\end{minipage}
58     \fi
59     \end{list}}
60
61\glossaryentry
62  {ntfn, Notification}
63  {A \emph{notification} object. A kernel object in seL4 consisting
64  of a set of binary semaphores, used for sending (signalling)
65  notifications to other threads.}
66  {glos:ntfn}
67
68\glossaryentry
69  {asid, asid pool}
70  {Address Space Identifier. ASIDs are associated with page
71  directories (PDs) and define the virtual address space of a
72  thread. Multiple threads may be in the same address space.
73  Since ARM hardware supports only 255 different ASIDs, seL4 on ARM
74  supports the concept of virtual ASIDs that are mapped to hardware ASIDS
75  managed in a two-level structure. The user manages only the second
76  level of this structure: the asid pool. An asid pool can be seen as
77  a set of virtual ASIDs that can be connected to and disconnected from
78  page directories.}
79  {}
80
81
82\glossaryentry
83  {badge}
84  {A badge is a piece of extra information stored in an endpoint
85  capability. It can be used by applications to identify caps
86  previously handed out to clients.}
87  {glos:badge}
88
89\glossaryentry
90  {cap, capability}
91  {The main access control concept in seL4. A capability conceptually
92  is a reference to a kernel object together with a set of access
93  rights. Most seL4 capabilities store additional bits of
94  information. Some of this additional information may be
95  exposed to the user, but the bulk of it is kernel-internal
96  book-keeping information. Capabilities are stored in CNodes and
97  TCBs.}
98  {glos:cap}
99
100\glossaryentry
101  {cdt}
102  {Capability Derivation Tree. A kernel-internal data structure that
103  tracks the child/parent relationship between capabilities. Capabilities
104  to new objects are children of the Untyped capability the object was
105  created from. Capabilities can also be copied; in this case the user may
106  specify if the operation should produce children or siblings of
107  the source capability. The revoke operation will delete all children
108  of the invoked capability.}
109  {}
110
111\glossaryentry
112  {cnode}
113  {Capability Node. Kernel-controlled storage that holds capabilities.
114   Capability nodes can be created in different sizes and be shared
115   between CSpaces. CNodes can be pointed to by capabilities themselves.}
116  {glos:cnode}
117
118\glossaryentry
119  {cspace}
120  {A directed graph of CNodes. The CSpace of a thread defines the set
121  of capabilities it has access to. The root of the graph is the CNode
122  capability in the CSpace slot of the thread. The edges of the graph
123  are the CNode capabilities residing in the CNodes spanned by this root.}
124  {glos:cspace}
125
126\glossaryentry
127  {cptr}
128  {Capability Pointer. A user-level reference to a capability,
129  relative to a specified root CNode or the thread's CSpace root. In
130  this specification, a user-level capability pointer is a sequence of
131  bits that define a path in the CSpace graph that should end in a
132  capability slot. The kernel resolves user-level capability pointers
133  into capability slot pointers (cslot\_ptr).}
134  {glos:cptr}
135
136\glossaryentry
137  {cslot\_ptr}
138  {Capability Slot Pointer. A kernel-internal reference to a capability. It
139  identifies the kernel object the capability resides in as well as
140  the location (slot) of the capability inside this object. }
141  {glos:cptr}
142
143\glossaryentry
144  {ep}
145  {Endpoint. Without further qualifier refers to a synchronous
146  communications (IPC) endpoint in seL4.}
147  {glos:ep}
148
149\glossaryentry
150  {guard}
151  {Guard of a CNode capability. From the user's perspetive the CSpace
152  of a thread is organised as a guardedage table. The kernel will
153  resolve user capability pointers into internal capability slot pointers.
154  The guard of one link/edge in the CSpace graph defines a sequence of bits
155  that will be stripped from the user-level capability pointer before
156  resolving resumes at the next CNode.}
157  {}
158
159\glossaryentry
160  {ipc}
161  {Inter Process Communication. In seL4: sending short synchronous messages
162  between threads. To communicate via IPC in seL4, the
163  receiver listens at an endpoint object and the sender sends to the
164  same endpoint object. There is a separate mechanism for
165  notifications between threads.}
166  {}
167
168\glossaryentry
169  {kheap}
170  {Kernel Heap. This is not an actual C heap in the sense that it
171  supports malloc and free. Rather, it is the kernel virtual memory
172  view of physical memory in the machine. }
173  {}
174
175\glossaryentry
176  {pd}
177  {Page Directory. The first level of an ARM virtual memory page
178  table. A page directory can be seen as an array of page directory
179  entries (PDEs).}
180  {}
181
182\glossaryentry
183  {pde}
184  {Page Directory Entry. One entry in the page directory. It either
185  is invalid, contains a translation to a frame, or a translation to
186  a second level page table.}
187  {}
188
189\glossaryentry
190  {pt}
191  {Page Table. The second level of an ARM virtual memory page
192  table. It can be seen as an array of page table entries.}
193  {}
194
195\glossaryentry
196  {pte}
197  {Page Table Entry. One entry of a second level ARM page table. It is
198  either invalid or contains a translation to a frame.}
199  {}
200
201\glossaryentry
202  {replycap}
203  {Reply Capability. Reply capabilities are created automatically
204  in the receiver of a Call IPC. The reply capability points back
205  to the sender of the call and can be used to send a reply efficiently
206  without having to explicitly set up a return channel. Reply capabilities
207  can be invoked only once. Internally, reply capabilities are created
208  as copies of so-called Master Reply Capabilities that are always
209  present in the master reply slot of the sender's TCB.}
210  {}
211
212\glossaryentry
213  {tcb}
214  {Thread Control Block. The kernel object that stores management data
215  for threads, such as the thread's CSpace, VSpace, thread state, or user
216  registers.}
217  {}
218
219\glossaryentry
220  {thread}
221  {The CPU execution abstraction of seL4.}
222  {}
223
224\glossaryentry
225  {vm}
226  {Virtual Memory. The concept of translating virutal memory addresses
227  to physical frames. SeL4 uses the MMU (Memory Management Unit) to
228  provide controlled virtual memory mechanisms to the user, to protect
229  kernel data and code from users, and to enforce separation between
230  users (if set up correctly). }
231  {}
232
233\glossaryentry
234  {vspace}
235  {In analogy to CSpace, the virtual memory space of a thread. In the
236  ARM case, the VSpace of a thread is defined by its top-level page
237  directory and that page directory's ASID.}
238  {}
239
240\glossaryentry
241  {zombie}
242  {Zombie Capability. This capability is not accessible to the
243  user. It stores continuation information for the preemtable
244  capability delete operation.}
245  {}
246\<close>
247
248(*<*)
249end
250(*>*)
251