Searched refs:The (Results 1 - 25 of 69) sorted by relevance

123

/seL4-refos-master/libs/libmuslc/src/ldso/powerpc/
H A Ddlsym.s6 mflr 5 # The return address is arg3.
/seL4-refos-master/libs/libmuslc/src/ldso/powerpc64/
H A Ddlsym.s9 mflr 5 # The return address is arg3.
/seL4-refos-master/projects/refos/design/
H A Dinterface.tex22 In \refOS, the access to an object (the permission to invoke the methods which manage the object) is implemented using a badged endpoint capability. The badge number is used to uniquely identify the instance of an object. Since most expected implementations of these protocols likely will use a similar method to track access permissions, the term capability may be used interchangably with object in this document. For example "window capability" means a capability which represents the access to a window object.
36 \item[\obj{dataspace}] is an object that represents a dataspace. The dataspace itself may represent anything that may be modeled as a series of bytes including devices, RAM and files. If something has access to a dataspace object, it may read from the dataspace object, write to the dataspace object and execute the dataspace object by mapping a memory window to the dataspace, closing the dataspace, or deleting the dataspace. Performing these operations is dependent on the dataspace permissions.
51 The process server interface provides the abstraction for managing processes and threads. The abstraction includes management of processes' virtual memory, memory window creation and deletion, process creation and deletion, death notification of client processes and thread management. Note that in implementations \cp{procserv}{session} could be the same capability as \cp{procserv}{process} in which case the process server is connectionless. \cp{procserv}{session} may also be shared with \cp{procserv}{anon} for simplification.
59 \item [procserv\_liveness\_C] The new client's liveness capability, which the client has given to the server through session connection
60 \item [death\_notify\_ep] The asynchronous endpoint through which death notification occurs
61 \item [death\_id] The unique client ID that the server will receive on death notification
62 \item [principle\_id] The ID used for permission checking (optional)
72 \item [base\_vaddr] The window base address in the calling client's VSpace
73 \item [size] The siz
[all...]
H A Dintro.tex15 The overall design of \refOS revolves around the abstraction of a dataspace. A dataspace is a memory space (a series of bytes) representing anything from physical RAM to file contents on a disk to a device or even to a random number generator. The concept is analogous to UNIX files which may represent anything from \texttt{/usr/bin/sh} to \texttt{/dev/audio} to \texttt{/dev/urandom}.
17 The dataspace abstraction which dataspace servers provide paves the way for more complicated infrastructure such as sharing with complex trust relationships, memory management, file systems, and distributed naming. On top of this additional infrastructure, an operating system could implement features such as POSIX standard system calls, ports of existing software, drivers and display servers.
52 \textbf{Synchronous Calls} are used to invoke methods implemented by a server. They involve a badged capability invocation of a synchronous endpoint that identifies the server and represents the authority of the caller. The caller blocks until the server responds. A caller implicitly trusts the server it calls. Calling an untrusted server is possible, but doing so should be avoided in general.
57 \textbf{Reply} protocols occur via reply capabilities. A call via invoking a synchronous endpoint generates a reply capability for the server to respond to the caller. The callee can send a response to the original caller and unblock the caller by replying with the reply capability. Reply capabilities are guaranteed either to succeed or to fail and not to block. Non-blocking replies are required for a trusted server to safely reply to an untrusted client.
61 with at-least-once semantics (the bits are OR'd together). The asynchronous endpoint can be used to notify an untrusted client. To send messages (as opposed to just notifications) to an untrusted client, shared memory must be set up between the server and the client. Care must be taken to avoid unfavourable results like blocking and denial of service on shared memory buffers which may fill up.
69 The basic concept of a capability is that a capability is an object that contains the permissions to access a particular object. This is a similar concept to UNIX file descriptors which indicate the access that a process has to a file. Just like UNIX file descriptor tables, capability objects are kept in kernel memory. User programs only have handles to such objects and cannot directly manipulate them.
112 Most of the interface methods are synchronous. The client making the call is considered to be less trusted than the server that is receiving the call. When a client makes a call, it is blocked until the server finishes handling the call and replies via the reply operation. When the server replies, the call is said to be finished and the client resumes execution. Method invocation is implemented with a synchronous call operation via a synchronous endpoint. Capabilities may be passed via method invocation and also via the corresponding reply.
137 For example, the notation \met{dataserv}{dataspace}{open} means an invocation of the \texttt{open} method of the \obj{dataspace} interface on the server called \srv{dataserv}. Note that any \srv{server} can implement a particular \obj{interface}. The encoding of method and arguments in the actual message is left as an implementation detail.
160 The followin
[all...]
H A Dpaper.tex131 The design of a multi-server operating system is crucial to its efficiency, security and dependability. Increasing usage of embedded systems and microcontroller chips has increased the interest from both industrial and academic communities in microkernel-based component-based software systems. This has resulted in heightened interest in developing better systems and more advanced microkernels.
133 This document outlines a basic reference design for system components and interfaces for an operating system. The protocols have been designed with an \Lf like microkernel in mind and assume functionality such as interprocess communcation, capability-based access models and virtual memory support. This reference design aims to standardise the protocols for tasks often required to build a system such as resource sharing, virtual memory management and naming. Operating systems may implement these protocols and extend them to incorporate more features.
135 A sample implementation of the following protocols is provided in addition to this document in the form of a simple operating system which runs simple client programs. The sample implementation, named \refOS, runs on the \seLf microkernel, which adds an extra dimension of dependability. Although this document outlines the major design strategies that \refOS employs, the doxygen code documentation provides additional details about \refOS.
146 The following people have contributed to this document:
/seL4-refos-master/kernel/manual/parts/
H A Dintro.tex11 The seL4 microkernel is an operating-system kernel designed to be
15 spaces, threads, and inter-process communication (IPC). The small number
23 confidentiality~\cite{Murray_MBGBSLGK_13}. The kernel's small size was
28 The document starts by giving a brief overview of the seL4 microkernel
H A Dipc.tex9 The seL4 microkernel provides a message-passing IPC mechanism for communication
10 between threads. The same mechanism is also used for communication with
22 The message words are sent to or received from a thread by placing them in its \emph{message registers}.
23 The message registers are numbered and the first few message registers are implemented
26 The reason for this design is efficiency:
28 The IPC buffer is assigned to the calling thread (see \autoref{sec:threads} and \autoref{api:tcb_setipcbuffer}).
31 Every IPC message also has a tag (structure \texttt{seL4\_MessageInfo\_t}). The
33 (the \texttt{extraCaps} field) and the \texttt{capsUnwrapped} field. The
37 transferred. The label is not interpreted by the
38 kernel and is passed unmodified as the first data payload of the message. The
[all...]
H A Dbootup.tex11 The seL4 kernel creates a minimal boot environment for the initial thread, which
22 The initial thread's CSpace consists of exactly one CNode
25 The CNode size can be configured at compile time (default is $2^{12}$
30 The first 12 slots contain specific capabilities as listed in
75 space. The mapped address is chosen by the kernel and given to the initial
78 The BootInfo Frame contains the C struct described in
84 The type \texttt{seL4\_SlotRegion} is a C struct
123 describes what the chunk is and how long it is, where the length includes the header. The
124 length can be used to skip over chunks that you do not understand. The only generally
126 chunk that has no data, any other types are platform or architecture specific. The
[all...]
H A Dcspace.tex31 % FIXME The references to mint in the following paragraph and previously in
40 these copied capabilities and the originals. The revoke method
67 amount of untyped memory (see \autoref{sec:object_sizes}). The caller
82 capability. The newly created capability may have fewer rights than
102 third to the second. The first and third specified slots may be the
104 capability in the second slot. The method is atomic; either both or
129 \texttt{node\_depth} arguments. The \texttt{node\_offset} argument specifies the
131 The \texttt{num\_objects} argument specifies the number of capabilities (and, hence, objects)
143 \obj{Reply}ing (see \autoref{ch:ipc}). The
148 Grant, having GrantReply or not is irrelevant. The meanin
[all...]
H A Dio.tex59 for delivery, ranging from VECTOR\_MIN to VECTOR\_MAX. The rights to allocate
93 The I/O port methods return error codes upon failure.
153 a 16-bit quantity. The first 8 bits identify the bus that the device is on.
154 The next 5 bits are the device identifier: the number of the device on
155 the bus. The last 3 bits are the function number. A single device may
163 The IOMMU page-table structure has three levels.
193 The standard specifies different types of address translations that correspond
211 The specificiation allows StreamIDs to be up to 16bits wide. There are also a
216 The seL4 API allows system software to manage an SMMU by assigning StreamIDs to
225 context bank in a system. The kerne
[all...]
H A Dnotifications.tex29 The \apifunc{seL4\_Signal}{sel4_signal} method updates the
38 The \apifunc{seL4\_Wait}{sel4_wait} method works similarly to a
45 The \apifunc{seL4\_Poll}{sel4_poll} is the same as \apifunc{seL4\_Wait}{sel4_wait}, except if
H A Dobjects.tex19 The basic services seL4 provides are as follows:
40 unprivileged applications. The kernel exports hardware device
54 The seL4 microkernel provides a capability-based access-control model.
94 been derived from the original capability being revoked. The propagation of
113 The seL4 kernel provides a message-passing service for communication between
116 number of data words and possibly some capabilities. The structure and encoding
127 % TODO: The \apifunc{}{} refs in the paragraphs below (up to the section on
146 appropriate one. The \emph{Yield} system call is not associated with any kernel
152 The fundamental system calls are:
186 The remainin
[all...]
H A Dvspace.tex15 The kernel also includes \obj{ASID Pool} and
29 The top-level paging structure corresponds directly to the higher-level concept of a VSpace in seL4.
36 The size and type of structure at each level, and the number of bits in the virtual address resolved
54 The rest of this section details the paging structures for each architecture.
88 4\,GiB address range, and a second-level \texttt{PageTable}. The second-level structures on AArch32
92 The top-level page directory covers a range of 4\,GiB and each page table covers a 1\,MiB range.
117 RISC-V provides the same paging structure for all levels, \texttt{PageTable}. The VSpace is then
151 The virtual address for a \obj{Page} mapping
158 writeable, the capability must have write permissions. The requested
250 capability. The \ob
[all...]
H A Dthreads.tex47 pointer. The thread can then be activated either by setting the
64 The \apifunc{seL4\_TCB\_Suspend}{tcb_suspend} method deactivates a thread.
84 The initial task starts with an MCP and priority as the highest priority in the system (\texttt{seL4\_MaxPrio}).
111 The tuple $(b, p)$ forms an upper bound on the thread's execution -- the kernel will not permit a
153 \item The maximum number of refills in a single scheduling context is determined by the size
174 Whenever a thread is executing it consumes the budget from its current scheduling context. The
206 The kernel does not conduct any schedulability tests, as task admission is left to user-level policy
218 context is donated to the passive thread. The generated reply cap ensures that the callee is merely
227 delivered. The passive receiver will be set to inactive as it does not have a scheduling context.
247 the scheduling context that is bound to the notification object. The schedulin
[all...]
H A Dapi.tex49 The API-ID of a target breakpoint. This ID will be a positive integer, with
143 The requested operation is not permitted.
226 The object currently has other objects derived from it and the requested
241 The \obj{Untyped Memory} object does not have enough unallocated space to
/seL4-refos-master/libs/libmuslc/src/internal/sh/
H A Dsyscall.s5 ! The kernel syscall entry point documents that the trap number indicates
/seL4-refos-master/libs/libmuslc/src/internal/i386/
H A Dsyscall.s3 # The calling convention for __vsyscall has the syscall number
38 # The __vsyscall6 entry point is used only for 6-argument syscalls.
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/doc/
H A DGuidebook.tex75 immortality by the gods. The amulet is rumored to be somewhere beyond the
207 on will escape an Elf. The quality of Elven craftsmanship often gives
228 The armor and weapons fashioned by the Orcs are typically of inferior quality.
260 {\it NetHack\/} offers a variety of display options. The options available to
263 enabled when your executable was created. The three possible display
265 and a graphical interface using small pictures called tiles. The two
275 understand what {\it NetHack\/} is doing with the screen. The {\it NetHack\/}
278 The way the screen looks for you depends on your platform.
282 The bat bites!
302 \subsection*{The statu
[all...]
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/doc/
H A DGuidebook.tex75 immortality by the gods. The amulet is rumored to be somewhere beyond the
207 on will escape an Elf. The quality of Elven craftsmanship often gives
228 The armor and weapons fashioned by the Orcs are typically of inferior quality.
260 {\it NetHack\/} offers a variety of display options. The options available to
263 enabled when your executable was created. The three possible display
265 and a graphical interface using small pictures called tiles. The two
275 understand what {\it NetHack\/} is doing with the screen. The {\it NetHack\/}
278 The way the screen looks for you depends on your platform.
282 The bat bites!
302 \subsection*{The statu
[all...]
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/include/
H A Dvmsconf.h113 * to prompt the player for a command to spawn in order to respond. The
139 * The remainder of the file should not need to be changed.
254 #define The vms_the macro
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/include/
H A Dvmsconf.h113 * to prompt the player for a command to spawn in order to respond. The
139 * The remainder of the file should not need to be changed.
254 #define The vms_the macro
/seL4-refos-master/seL4_tools/cmake-tool/helpers/
H A Dmake-uimage56 object. ARCHITECTURE must be either "arm" or "arm64". The image is
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/src/
H A Dwrite.c236 The(aobjnam(new_obj, "slip")),
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/src/
H A Dwrite.c236 The(aobjnam(new_obj, "slip")),
/seL4-refos-master/kernel/manual/
H A Dmanual.tex117 The primary authors of this document are Matthew Grosvenor and Adam Walker,

Completed in 133 milliseconds

123