You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <[email protected]>
description={Address Space Identifier. Depending on architecture, the kernel provides software ASIDs, which are associated with VSpace root objects, and define the virtual address space of a thread. They are mapped to hardware ASIDs on demand when the architecture supports these. Multiple threads may be in the same address space}
10
+
}
11
+
12
+
\newglossaryentry{badge}{
13
+
name=Badge,
14
+
description={A badge is a piece of extra information stored in a capability, mostly used for endpoint and notification capabilities. It can be used by applications to identify caps previously handed out to clients}
15
+
}
16
+
17
+
\newglossaryentry{cap}{
18
+
name=Capability,
19
+
description={The main access control concept in seL4. A capability conceptually is a reference to a kernel object together with a set of access rights. Most seL4 capabilities store additional bits of information. Some of this additional information may be exposed to the user, but the bulk of it is kernel-internal book-keeping information. Capabilities are stored in CNodes and TCBs}
20
+
}
21
+
22
+
\newglossaryentry{cdt}{
23
+
name=CDT,
24
+
description={Capability Derivation Tree. A kernel-internal data structure that tracks the child/parent relationship between capabilities. Capabilities to new objects are children of the Untyped capability the object was created from. Capabilities can also be copied and result in either child or sibling capabilities, depending on the operation that was used and the depth of the existing derivation tree. The revoke operation will delete all children of the invoked capability}
25
+
}
26
+
27
+
\newglossaryentry{cnode}{
28
+
name=CNode,
29
+
description={Capability Node. Kernel-controlled storage that holds capabilities. Capability nodes can be created in different sizes and be shared between CSpaces}
30
+
}
31
+
32
+
\newglossaryentry{cptr}{
33
+
name=CPtr,
34
+
description={Capability Pointer. A user-level reference to a capability, relative to a specified root CNode or the thread’s CSpace root}
35
+
}
36
+
37
+
\newglossaryentry{cspace}{
38
+
name=CSpace,
39
+
description={A directed graph of CNodes. The CSpace of a thread defines the set of capabilities it has access to. The root of the graph is the CNode capability in the CSpace slot of the thread. The edges of the graph are the CNode capabilities residing in the CNodes spanned by this root}
40
+
}
41
+
42
+
\newglossaryentry{endpoint}{
43
+
name=Endpoint,
44
+
description={IPC is facilitated by small kernel objects known as endpoints, which act as general communication ports. Invocations on endpoint objects are used to send and receive IPC messages}
45
+
}
46
+
47
+
\newglossaryentry{guard}{
48
+
name=Guard,
49
+
description={Guard of a CNode capability. From the user’s perspetive the CSpace of a thread is organised as a guarded page table. The kernel will resolve user capability pointers into internal capability slot pointers. The guard of one link/edge in the CSpace graph defines a sequence of bits that will be stripped from the user-level capability pointer before resolving resumes at the next CNode}
50
+
}
51
+
52
+
\newglossaryentry{iommu}{
53
+
name=IOMMU,
54
+
description={Input–Output Memory Management Unit. Applies virtual address translation and memory protection to DMA capable I/O devices}
55
+
}
56
+
57
+
\newglossaryentry{iopagetable}{
58
+
name=IOPageTable,
59
+
description={This object represents a node in the multilevel page-table structure used by IOMMU hardware to translate hardware memory accesses}
60
+
}
61
+
62
+
\newglossaryentry{iospace}{
63
+
name=IOSpace,
64
+
description={This object represents the address space associated with a hardware device. It represents the right to modify a device’s address space. See \autoref{ch:io}}
65
+
}
66
+
67
+
\newglossaryentry{ipc}{
68
+
name=IPC,
69
+
description={Inter Process Communication is facilitated by endpoints, which act as general communication ports. Invocations on endpoint objects are used to send and receive messages}
70
+
}
71
+
72
+
\newglossaryentry{irqcontrol}{
73
+
name=IRQControl,
74
+
description={A single capability from which IRQHandler capabilities to all IRQ numbers in the system can be derived. This capability can be moved between CSpaces and CSlots but cannot be duplicated. Revoking this capability removes all IRQHandlers}
75
+
}
76
+
77
+
\newglossaryentry{irqhandler}{
78
+
name=IRQHandler,
79
+
description={Capabilities that represent the ability of a thread to handle a certain interrupt. See \autoref{ch:io}}
80
+
}
81
+
82
+
\newglossaryentry{notificationobject}{
83
+
name=Notification Object,
84
+
description={A word-size array of flags that provides a non-blocking signalling mechanism similar to a binary semaphore. Operations are signalling a subset of flags in a single operation, polling to check any flags, and blocking until any are signalled. Notification capabilities can be signal-only or wait-only}
85
+
}
86
+
87
+
\newglossaryentry{replyobject}{
88
+
name=Reply Object,
89
+
description={(MCS only) A reply object is a vessel for tracking reply messages, used to send a reply message and
90
+
wake up the caller}
91
+
}
92
+
93
+
\newglossaryentry{schedulingcontext}{
94
+
name=Scheduling Context,
95
+
description={(MCS only) An abstraction of CPU execution time}
96
+
}
97
+
98
+
\newglossaryentry{tcb}{
99
+
name=TCB,
100
+
description={Thread Control Block. The kernel object that stores management data for threads, such as the thread's CSpace, VSpace, thread state, or user registers}
101
+
}
102
+
103
+
\newglossaryentry{untypedmemory}{
104
+
name=Untyped Memory,
105
+
description={Memory that can be used to create kernel objects via the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} invocation. It is the foundation of memory allocation in the seL4 kernel. See \autoref{sec:kernmemalloc}}
106
+
}
107
+
108
+
\newglossaryentry{vm}{
109
+
name=VM,
110
+
description={Virtual Memory. The concept of translating virtual memory addresses to physical frames. See \autoref{ch:vspace}}
111
+
}
112
+
113
+
\newglossaryentry{vspace}{
114
+
name=VSpace,
115
+
description={Virtual Address Space. In analogy to CSpace, the virtual memory space of a thread. See \autoref{ch:vspace}}
0 commit comments