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