Home
last modified time | relevance | path

Searched refs:a (Results 1 – 25 of 106) sorted by relevance

12345

/seL4-master/manual/parts/
A Dcspace.tex18 \obj{CNode}s, forming a directed graph. Conceptually a thread's CSpace
33 % it was not possible to change a capability's rights during a CNode_Copy.
224 illustrates a standard scenario: the top level is a large untyped
313 When performing a system call, a thread specifies to the kernel the
323 As explained earlier, a CSpace is a directed graph of \obj{CNode}
338 Like a virtual memory address, a capability address is simply an
340 does a virtual memory address), a capability address refers to a
372 \item a top level CNode object with a 12-bit guard set to 0x000 and
377 \item a second level CNode that contains a reference to a top level
475 slots, the user supplies a starting address and a window size.
[all …]
A Dintro.tex11 The seL4 microkernel is an operating-system kernel designed to be a secure,
12 safe, and reliable foundation for systems in a wide variety of application
13 domains. As a microkernel, it provides a small number of mechanisms that can be
17 The small number of mechanisms translates to a small implementation on the order
25 time~\cite{Blackham_SCRH_11,Blackham_SH_12}. \citet{Klein_AEMSKH_14} give a
27 paper~\cite{whitepaper} provides a shorter, but more accessible overview.
34 This manual describes the seL4 kernel's API from a user's point of view. The
35 document starts by giving a brief overview of the seL4 microkernel design,
36 followed by a reference of the high-level API exposed by the seL4 kernel to
40 of the seL4 kernel, this document is by no means a formal specification of the
[all …]
A Dobjects.tex71 a capability---to request a kernel service, for example---using the
88 create a derived capability with a subset of the rights of the
115 services. There is a standard message format, each message containing a
123 interpreted as a method invocation in a manner specific to the type of kernel
124 object. For example, invoking a thread control block (TCB) capability with a
138 waits for a \emph{Reply}. A \emph{reply} message is always delivered via a
175 In the MCS configuration, \emph{Receive} takes a reply capability---a
176 capability to a reply object--as a parameter.
235 a request and waiting for the next can be performed in a single kernel
291 a sender and a receiver rendezvous at the endpoint, and the
[all …]
A Dthreads.tex19 With MCS, a scheduling context is represented by a scheduling context object
81 When a thread modifies a another threads priority (including itself) it must provide a
181 one kernel entry. When a thread is bound to a scheduling context, if it is in a runnable state and
257 both a notification object and a thread, the behaviour will be the same as for a passive server:
298 With these methods, a
317 make any more progress until the page is mapped. If a thread experiences a
344 If a reply message is sent to a nested server and a scheduling context without
370 Faults are delivered in such a way as to imitate a Call from the faulting
378 can occur when lookup of a capability referenced by a
411 This fault occurs when a thread executes a system call with a syscall
[all …]
A Dio.tex125 modify a device's memory mappings.
201 Faults that occur when a memory transaction conflicts with a StreamID or CB
227 track which VSpace a context bank has bound to it, and which context bank a
252 transaction stream, which can be used to bind and unbind a stream to a
285 allocated in a system.
289 context banks. Currently only direct mapping of a StreamID to a context bank is
314 By providing a \obj{seL4\_ARM\_CB} cap, a user-level thread can configure the
363 Deleting a \obj{seL4\_ARM\_CB} cap that contains a valid capBindSID field will:
409 maintaining: the number of context banks using a given ASID, and the ASID that a
418 its ASID (triggered by updating a page table entry, e.g. unmapping a page), and
[all …]
A Dvspace.tex9 A virtual address space in seL4 is called a VSpace. In a similar
10 way to a CSpace (see \autoref{ch:cspace}), a VSpace is composed of objects
28 Each architecture has a top-level paging structure (level 0) and a number of intermediate levels.
41 the capability being mapped, e.g. to map a level 1 paging structure at a specific virtual address,
50 API allows users more flexible policy options. For example, a process that has delegated a page
92 The top-level page directory covers a range of 4\,GiB and each page table covers a 1\,MiB range.
103 Arm AArch64 processors have a four-level page-table structure, where the VSpace is realised as a
118 realised as a \texttt{PageTable}.
151 The virtual address for a \obj{Page} mapping
155 To map a page readable, the capability
[all …]
A Dipc.tex11 kernel-provided services. Messages are sent by invoking a capability to a
20 Each message contains a number of message words and optionally a number of
44 % FIXME: a little too low-level, perhaps?
99 \obj{Endpoint}s allow a small amount
125 create a new endpoint capability with a \emph{badge} attached to it, a data
126 …hosen by the invoker of the \emph{mint} operation. When a message is sent to an endpoint using a b…
178 If a receiver gets a message whose tag has an \texttt{extraCaps} of 2 and a
252 the caller who would still be waiting for a reply.
260 A reply capability is invoked in the same way as a normal send on a
267 that invoking a reply capability cannot block: If you own a reply capability,
[all …]
A Dnotifications.tex9 Notifications are a simple, non-blocking signalling mechanism that
10 logically represents a set of binary semaphores.
14 A \obj{Notification} object contains a single data word, called the
37 The \apifunc{seL4\_Wait}{sel4_wait} method works similarly to a
56 \obj{Notification} objects and \obj{TCB}s can be bound together in a 1-to-1 relationship
57 through the \apifunc{seL4\_TCB\_BindNotification}{tcb_bindnotification} invocation. When a
58 \obj{Notification} is bound to a \obj{TCB}, signals to that notification object
60 endpoint. To distinguish whether the received message was a notification
61 or an IPC, developers should check the badge value. By reserving a
66 Once a notification has been bound, the only thread that may perform
/seL4-master/include/
A Dutil.h9 #define PASTE(a, b) a ## b argument
10 #define _STRINGIFY(a) #a argument
11 #define STRINGIFY(a) _STRINGIFY(a) argument
45 #define MIN(a,b) (((a)<(b))?(a):(b)) argument
46 #define MAX(a,b) (((a)>(b))?(a):(b)) argument
/seL4-master/src/machine/
A Dio.c101 #define MASK_TYPE(a) (1U<<( a -' ')) argument
335 l = z - a; in printf_core()
336 out(f, a, l); in printf_core()
471 a = z - p; in printf_core()
472 *a = arg.i; in printf_core()
476 z = a + strnlen(a, p < 0 ? INT_MAX : p); in printf_core()
480 p = z - a; in printf_core()
525 a = z; in printf_core()
531 if (p < z - a) { in printf_core()
532 p = z - a; in printf_core()
[all …]
/seL4-master/LICENSES/
A DLPPL-1.3c.txt47 with the Work or a significant portion of such a file, either verbatim or
69 or interpreting a part or the whole of the Work.
76 a program implementing the `TeX language'.
92 3. You may distribute a Compiled Work that has been generated from a complete,
114 a. If a component of this Derived Work can be a direct replacement for a component
160 a. A Derived Work may be distributed under a different license provided that
165 b. If a Derived Work is distributed under a different license, that Derived
278 a different license. You may use the text of this license as a model for your
351 Given such a notice and statement in a file, the conditions given in this
370 a Derived Work is intended to be used as a (compatible or incompatible) replacement
[all …]
A DCC-BY-SA-4.0.txt64 relation with a moving image.
108 that members of the public may access the material from a place and at a time
117 this Public License. Your has a corresponding meaning.
121 a. License grant.
168 Section 3(a)(1)(A)(i).
191 a. Attribution.
202 ii. a copyright notice;
222 by Section 3(a)(1)(A) to the extent reasonably practicable.
243 a. for the avoidance of doubt, Section 2(a)(1) grants You the right to extract,
253 a substantial portion of the contents of the database.
[all …]
A DGPL-2.0-or-later.txt35 For example, if you distribute copies of such a program, whether gratis or
36 for a fee, you must give the recipients all the rights that you have. You
64 or work, and a "work based on the Program" means either the Program or any
84 You may charge a fee for the physical act of transferring a copy, and you
85 may at your option offer warranty protection in exchange for a fee.
126 the Program (or with a work based on the Program) on a volume of a storage
142 a medium customarily used for software interchange; or,
187 7. If, as a consequence of a court judgment or allegation of patent infringement
193 a consequence you may not distribute the Program at all. For example, if a
201 the section as a whole is intended to apply in other circumstances.
[all …]
A DGPL-2.0-only.txt35 For example, if you distribute copies of such a program, whether gratis or
36 for a fee, you must give the recipients all the rights that you have. You
64 or work, and a "work based on the Program" means either the Program or any
84 You may charge a fee for the physical act of transferring a copy, and you
85 may at your option offer warranty protection in exchange for a fee.
126 the Program (or with a work based on the Program) on a volume of a storage
142 a medium customarily used for software interchange; or,
187 7. If, as a consequence of a court judgment or allegation of patent infringement
193 a consequence you may not distribute the Program at all. For example, if a
201 the section as a whole is intended to apply in other circumstances.
[all …]
A DApache-2.0.txt43 or translation of a Source form, including but not limited to compiled object
49 made available under the License, as indicated by a copyright notice that
57 annotations, elaborations, or other modifications represent, as a whole, an
75 owner as "Not a Contribution."
90 each Contributor hereby grants to You a perpetual, worldwide, non-exclusive,
97 any entity (including a cross-claim or counterclaim in a lawsuit) alleging
107 (a) You must give any other recipients of the Work or Derivative Works a copy
118 (d) If the Work includes a "NOTICE" text file as part of its distribution,
119 then any Derivative Works that You distribute must include a readable copy
122 one of the following places: within a NOTICE text file distributed as part
[all …]
/seL4-master/tools/
A Dhelpers.cmake62 # generate a rule for copying the input file to a default name.
92 # Function to generate a custom command to process a bitfield file. The input
93 # (pbf_path) is either a .bf file or, if you used pre-processor directives, a
94 # pre-processed .bf file. As this invokes a python tool that places a file
125 # Wrapper function for generating both a target and command to process a bitfield file
131 # Wrapper around GenBFTarget for generating a C header file out of a bitfield specification
300 # Set a configuration option to a particular value. This value will not appear in
320 # Defines a configuration option that is a user configurable string. Most parameters
535 # Defines a target for a 'configuration' library, which generates a header based
563 # Set a property on the library that is a list of the files we generated. This
[all …]
/seL4-master/tools/hardware/outputs/
A Delfloader.py114 for i, cpu_node in enumerate(sorted(cpus, key=lambda a: a.path)):
140 return sorted(cpu_info, key=lambda a: a['cpuid'])
159 device_info.sort(key=lambda a: a['compat'])
/seL4-master/manual/
A DDoxyfile12 # All text after a double hash (##) is considered a comment and is placed in
15 # All text after a single hash (#) is considered a comment and will be ignored.
35 # The PROJECT_NAME tag is a single word (or a sequence of words surrounded by
50 # for a project that appears at the top of each page and should give viewer a
130 # doxygen will generate a detailed section even if there is only a brief
199 # to treat a multi-line C++ comment block as a detailed description. Set this
360 # (for instance a group of public functions) to be put as a subgroup of that
389 # When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or
689 # Note that if you run doxygen from a directory containing a file called
840 # output. The symbol name can be a fully qualified name, a word, or if the
[all …]
/seL4-master/configs/
A DseL4Config.cmake22 # This macro is intended to be called from within a platform config.
74 # Register a platform's config options to be set if it is selected.
94 # helper macro that prints a message that no sub platform is specified and
104 # helper macro that prints a message that no architecture is specified and
114 # This could be moved to a cmake function
116 # can take a long time though.
129 # been set by a platform.
167 # Verify that, as a minimum any variables that are used
197 # Check for v7ve before v7a as v7ve is a superset and we want to set the
203 set(KernelArmArmV "armv7-a" CACHE INTERNAL "")
[all …]
/seL4-master/
A Dconfig.cmake278 to be linked with the kernel as a scheduling configuration."
329 imply you are using a verified kernel."
342 "Builds the kernel with support for a userspace debug API, which can \
420 setting if your serial output is redirected to a file or pipe."
427 "On a double fault the kernel can try and print out the users stack to aid \
471 # of the currently running thread without a capability.
477 is used to ensure a thread has enough budget to get in and out of the \
478 kernel. When running in a simulator the WCET estimate, which is tuned \
479 for hardware, may not be sufficient. This option provides a hacky knob \
480 that can be fiddled with when running inside a simulator."
[all …]
A Dgdb-macros7 #GDB macros for displaying seL4 data structures. Currently a work in progress.
16 This is a set of macros to interpret sel4 data structures. Available commands:
39 Type help <command> for more information on a specific command
313 …Determines the type of a cap and prints relevant information. arg0: a kernel capability data struc…
408 printf "Error: not a CNode\n"
469 printf "Error: not a CNode\n"
490 Dump the contents of a CNode. arg1: the CNode to dump
625 …"Prints all of the fields in a vtd context table. There is one entry for each (dev, fn) in the bus…
663 "Prints all of the fields in a vtd page table. arg0: a pointer to the page table"
680 "Convert a virtual address in the kernel to a physical address"
[all …]
/seL4-master/include/arch/riscv/arch/object/
A Dstructures.h33 #define ASID_LOW(a) (a & MASK(asidLowBits)) argument
34 #define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) argument
/seL4-master/src/kernel/
A Dboot.c812 word_t a = 0; in init_freemem() local
819 } else if (avail_reg[a].start >= avail_reg[a].end) { in init_freemem()
821 a++; in init_freemem()
828 insert_region(avail_reg[a]); in init_freemem()
829 a++; in init_freemem()
835 avail_reg[a].start = MIN(avail_reg[a].end, reserved[r].end); in init_freemem()
842 region_t m = avail_reg[a]; in init_freemem()
850 a++; in init_freemem()
863 for (; a < n_available; a++) { in init_freemem()
864 if (avail_reg[a].start < avail_reg[a].end) { in init_freemem()
[all …]
/seL4-master/src/arch/x86/
A Dconfig.cmake103 "The kernel maintains a mapping of 16-bit VPIDs to VCPUs. This option should be \
129 "The kernel only ever supports one method of performing syscalls at a time. This \
233 number of pixels. For a text mode this is the number of characters, value of zero \
251 …"Inserts a header that indicates to the bootloader that the kernel supports a multiboot 1 boot hea…
258 …"Inserts a header that indicates to the bootloader that the kernel supports a multiboot 2 boot hea…
266 "Prevent against the Meltdown vulnerability by using a reduced Static Kernel
268 This only needs to be enabled if deploying to a vulnerable processor"
312 to protect user level process from each other in a multicore environment."
328 "Performs a IBPB on every context switch to prevent Spectre attacks between user
331 Note that in a multicore environment you should also enable STIBP to prevent
[all …]
/seL4-master/include/arch/x86/arch/32/mode/object/
A Dstructures.h59 #define ASID_LOW(a) (a & MASK(asidLowBits)) argument
60 #define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) argument

Completed in 73 milliseconds

12345