Searched refs:capabilities (Results 1 - 14 of 14) sorted by relevance

/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dipc.tex25 capabilities.
36 tag consists of four fields: the label, message length, number of capabilities
38 message length and number of capabilities determine either the number of
39 message registers and capabilities that the sending thread wishes to transfer,
40 or the number of message registers and capabilities that were actually
45 manner in which capabilities were received. It is described in
63 endpoint capabilities received}
104 of data and capabilities (namely the IPC buffer) to be transferred between two
120 Endpoint capabilities may be \emph{minted} to
129 capabilities wit
[all...]
H A Dcspace.tex16 capabilities that the thread possesses, thereby governing which
19 Recall that capabilities reside within kernel-managed objects known as
21 contain a capability. This may include capabilities to further
28 capability. Threads refer to capabilities in their CSpaces (e.g. when
31 of the indices of the \obj{CNode} capabilities forming the path to the
38 Recall that capabilities can be copied and moved within CSpaces, and
40 \autoref{sec:cap-transfer}). Furthermore, new capabilities can be
44 these copied capabilities and the originals. The revoke method
45 removes all capabilities (in all CSpaces) that were derived from a
54 addressing capabilities withi
[all...]
H A Dnotifications.tex23 \obj{Notification} capabilities can be badged, using
26 capabilities (see \autoref{sec:ep-badges}). As with \obj{Endpoint}
27 capabilities, badged \obj{Notification} capabilities cannot be
28 unbadged, rebadged or used to create child capabilities with
73 specific badge (or range of badges) for capabilities to the bound
H A Dbootup.tex20 which contains capabilities to the initial
27 The first 12 slots contain specific capabilities as listed in
69 which capabilities are stored where in its CNode, the kernel provides
77 capabilities, it also informs the initial thread about
103 \texttt{seL4\_SlotRegion} & \texttt{ioSpaceCaps} & I/O space capabilities for ARM SMMU \\
108 \texttt{seL4\_SlotRegion} & \texttt{untyped} & untyped-memory capabilities \\
122 \texttt{extraBIPages} slot region gives the frames capabilities for the pages that make up
140 The capabilities in \texttt{userImageFrames} are
143 The capabilities in \texttt{userImagePaging} are ordered in descending order
144 of paging structure size. Within a given paging structure size, capabilities ar
[all...]
H A Dobjects.tex39 \item[Capability spaces] store capabilities (i.e., access rights) to
57 capabilities. This enables software-component isolation with a high
70 capability system, where capabilities are managed by the kernel.
74 slots, where each slot may contain further \obj{CNode} capabilities. An
83 kernel service. Furthermore, capabilities can be \emph{minted} to
89 authority. Revocation recursively removes any capabilities that have
91 capabilities through the system is controlled by a
108 number of data words and possibly some capabilities. The structure and encoding
111 Threads send messages by invoking capabilities within their capability space.
113 transferred through the kernel to another thread. When capabilities t
[all...]
H A Dio.tex24 \obj{IRQHandler} capabilities represent the ability of a thread to
44 When the system first starts, no \obj{IRQHandler} capabilities are
51 resulting capabilities as appropriate. Methods on \obj{IRQControl} can
52 be used for creating \obj{IRQHandler} capabilities for interrupt sources.
60 In addition to managing \obj{IRQHandler} capabilities, x86 platforms require
80 Access to I/O ports is controlled by \obj{IO Port} capabilities. Each
107 \obj{IO Port} capabilities to sub ranges of I/O ports. Any range that is issued
137 \obj{Page} capabilities are used to represent the actual frames that are
H A Dvspace.tex26 capabilities to the required objects.
52 By making these cache related operations invocations on page directory capabilities in addition to
53 the page capabilities themselves, the
56 to those capabilities directly.
H A Dthreads.tex130 invalid capabilities silently fail). In this case, the capability
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/api/
H A Dbootinfo_types.h23 seL4_Uint32 capabilities; member in struct:seL4_VBEInfoBlock
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/x86/sel4/arch/
H A Dbootinfo_types.h23 seL4_Uint32 capabilities; member in struct:seL4_VBEInfoBlock
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DDeviceContext.sml480 val CURVECAPS = W (28 (* Curve capabilities *))
481 val LINECAPS = W (30 (* Line capabilities *))
482 val POLYGONALCAPS = W (32 (* Polygonal capabilities *))
483 val TEXTCAPS = W (34 (* Text capabilities *))
484 val CLIPCAPS = W (36 (* Clipping capabilities *))
485 val RASTERCAPS = W (38 (* Bitblt capabilities *))
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DHolBdd.tex233 has similar capabilities.
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DHolBdd.tex233 has similar capabilities.
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/
H A Dquotient.tex2609 %of tools and capabilities to prove theorems that existed at the lower
2610 %level, and recreate those capabilities at the higher level. This has

Completed in 193 milliseconds