Searched refs:as (Results 1 - 24 of 24) sorted by relevance

/seL4-refos-master/libs/libmuslc/src/fenv/i386/
H A Dfenv.s9 # consider sse fenv as well if the cpu has XMM capability
73 # consider sse fenv as well if the cpu has XMM capability
102 # consider sse fenv as well if the cpu has XMM capability
134 # consider sse fenv as well if the cpu has XMM capability
154 # consider sse fenv as well if the cpu has XMM capability
/seL4-refos-master/libs/libmuslc/src/fenv/i386_sel4/
H A Dfenv.s9 # consider sse fenv as well if the cpu has XMM capability
73 # consider sse fenv as well if the cpu has XMM capability
102 # consider sse fenv as well if the cpu has XMM capability
134 # consider sse fenv as well if the cpu has XMM capability
154 # consider sse fenv as well if the cpu has XMM capability
/seL4-refos-master/kernel/manual/parts/
H A Dvspace.tex20 virtual memory address spaces. It should be noted that, as usual, the
30 For each architecture, the VSpace is realised as a different object, as determined by the
43 structure is passed as an argument.
45 In general, the top-level structure has no invocations for mapping, but is used as an argument to
58 On IA-32, the VSpace is realised as a \texttt{PageDirectory}, which covers the entire 4\,GiB range
72 On x86-64, the VSpace is realised as a \texttt{PML4}. Three further levels of paging structure are
73 defined, as shown in the table below. All structures are indexed with 9 bits of the virtual
87 Like IA-32, ARM AArch32 realise the VSpace as a \texttt{PageDirectory}, which covers the entire
103 ARM AArch64 processors have a four-level page-table structure, where the VSpace is realised as
[all...]
H A Dipc.tex38 kernel and is passed unmodified as the first data payload of the message. The
78 \texttt{seL4\_IPCBuffer} as defined in \autoref{tbl:ipcbuffer}. The
79 kernel uses as many physical registers as possible to transfer IPC
104 IPC \obj{Endpoints} uses a rendezvous model and as such is
151 as a CPTR in the sending thread's capability space. The number of capabilities
192 a lookup failure error as described in \autoref{sec:errors}.
196 and terminates as soon as an error is encountered. Possible error
232 some specific actions are taken. First a call will do exactly the same action as
[all...]
H A Dobjects.tex10 more complex services may be implemented as applications on top of these
19 The basic services seL4 provides are as follows:
39 \item[Device primitives] allow device drivers to be implemented as
62 degree of assurance, as only those operations explicitly authorised by
66 object (such as a thread control block) and carries access rights that
76 Capability spaces are implemented as a directed graph of kernel-managed
123 interpreted as a method invocation in a manner specific to the type of kernel
128 % kernel objects) go to the API reference which is very terse and not nearly as
133 Fundamentally, we can regard the kernel as providing three system calls:
157 If there are no other runnable threads with the same priority as th
[all...]
H A Dcspace.tex15 Recall that capabilities reside within kernel-managed objects known as
49 programmer is responsible for constructing CSpaces as well as
68 must therefore have a capability to enough untyped memory as well as
89 capability has the same badge and guard as the original.
118 any outstanding sends that use the same badge and object as the
149 relative to the various object types, as detailed
155 methods such as \apifunc{seL4\_CNode\_Mint}{cnode_mint} and
186 Various methods, such as \apifun
[all...]
H A Dthreads.tex31 it will not be able to perform most kernel invocations, as they require
84 The initial task starts with an MCP and priority as the highest priority in the system (\texttt{seL4\_MaxPrio}).
93 Thread priority (structure \texttt{seL4\_PrioProps\_t}) consists of two values as follows:
113 represent a lower bound on execution, as a thread must have the highest or equal highest priority
120 referred to as \emph{active}. Budget charging and replenishment rules are different for round-robin
124 Threads where $b == p$ are treated as round robin threads, where $b$ acts as a timeslice.
143 Round-robin threads are treated that same as sporadic threads except for one case: how the
170 to their whole budget, as they can be preempted or switch threads more often without filling their
171 replenishment queue. However, the scheduling overhead will be higher as th
[all...]
H A Dio.tex12 Interrupts are delivered as notifications. A thread
47 resulting capabilities as appropriate. Methods on \obj{IRQControl} can
61 be considered as the kernel outsourcing the allocation of this namespace to
87 Each of these methods takes as arguments an \obj{IO Port} capability
116 remapped from the device's point of view. It acts as an MMU for the
149 PCI identifier of the device as the low 16 bits of the \texttt{badge} argument, and
150 a Domain ID as the high 16 bits of the \texttt{badge} argument.
194 to stages in the ArmV8 virtual memory system architecture such as either
241 SMMU fault interrupts can be handled the same as other platform level interrupts.
324 The SMMU-v2 uses the same paging structure as th
[all...]
H A Dintro.tex14 services to applications, such as abstractions to create and manage virtual address
H A Dnotifications.tex45 The \apifunc{seL4\_Poll}{sel4_poll} is the same as \apifunc{seL4\_Wait}{sel4_wait}, except if
H A Dbootup.tex24 thread's own resources as well as to all available global resources.
30 The first 12 slots contain specific capabilities as listed in
H A Dapi.tex193 \ipcbloc{IPCBuffer[2..]} & Lookup failure description as described in \autoref{sec:lookup_fail_desc}\\
/seL4-refos-master/projects/refos/design/
H A Dintro.tex17 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.
36 \texttt{Dataspace servers} (henceforth also referred to as \emph{dataservers}) are servers which implement the dataspace interface (or a subset of it) in order to provide a dataspace service to clients. Dataspace servers are often designed to provide dataspaces which represent a common concept. For instance, a file server may implement the dataspace interface for files stored on disk, and an audio driver may serve audio bytestream dataspaces.
38 \texttt{Process servers} are servers which implement the process server interface and provide process abstraction. In practice, the process server may also need to implement additional interfaces and provide additional functionality in order for a system to start. For instance, in \refOS the process server also does naming and console input and output, implements the dataspace interface for anonymous memory and acts as the memory manager.
40 \texttt{Pagers} are servers which implement the pager service interface, which is very closely related to the dataspace interface and can be considered an optional feature of a dataspace server. Dataspace servers which act as pagers may have their dataspaces mapped directly into client virtual memory.
45 \refOS is designed with an \Lf family microkernel in mind and assumes the existence of features such as interprocess communication and capabilities. This section describes these assumed features. These features are available in advanced \Lf-based microkernels such as \seLf.
54 Exceptions, such as page faults, are propagated via sending and blocking on a synchronous endpoint.
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.
73 In the sample implementation given using the \seLf microkernel, these assumptions are implemented as kerne
[all...]
H A Dinterface.tex13 This chapter explains the interfaces which make up the \refOS protocol. These interfaces set the language with which components in the system interact. Interfaces are intended to provide abstractions to manage conceptual objects such as a processes, files and devices.
28 \item[\obj{process}] is an object which is most likely maintained by the process server (\srv{procserv}) and represents a process. If something has access to a process object, it may perform operations involving that process such as killing that process and calling methods on behalf of that process.
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.
38 \item[\obj{memwindow}] is an object that represents an address space range (i.e. a memory window) segment in a process's virtual memory. If something has access to a memory window object, it may perform operations on the memory window object such as mapping the memory window to a dataspace and mapping a frame into the memory window.
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.
125 Start a new thread, sharing the current client process's address space. The child thread will have the same priority as the parent process.
160 Open a new dataspace at the dataspace server, which represents a series of bytes. Dataspace mapping methods such as datamap() and init\_data() directly or indirectly map the contents of a dataspace into a memory window after which the contents can be read from and written to. The concept of a dataspace in \refOS is similar to a file in UNIX: what a dataspace represents depends on the server that is implementing the interface.
172 Expand a given dataspace. Note that some dataspaces may not support this method as sometimes the size of a dataspace makes no sense (serial input for instance).
194 Initialise a dataspace by the contents of a source dataspace. The source dataspace is where the content is, and the source dataspace must originate from the invoked dataserver. Whether the destination dataspace and the source dataspace can originate from the same dataserver depends on the dataserver implementation: one should refer to the dataserver documentation. One example use case for this is a memory manager implementing the dataspace for RAM having a block of RAM initialised by an external data source such as a file from a file server.
223 Share a dataspace of a dataserver with another process. The exact implementation of this is context-based. For example, a server sharing a parameter buffer may implement this method as \textt
[all...]
H A Dpaper.tex39 %%% internal as well as external links).
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.
H A Dprotocol.tex109 \autoref{f:opendata} shows mapping an open dataspace into a given memory window. The initialisation sets up the components for sample fault delegation in the system. Note that the process server is acting as the memory manager. The paging could instead be implemented through a separate memory manager process.
198 In this example, the shared dataspace is implemented by the process server (acting as the memory manager) and is shared with a server. This is typical for a shared memory communication buffer.
283 \autoref{f:initdata} shows creating a dataspace and setting the dataspace so that it is initialised with the contents of another dataspace. This example initialises a RAM dataspace (with the process server acting as its data server as per \refOS's implementation) with the contents of an executable file from another dataspace.
/seL4-refos-master/kernel/src/arch/x86/32/
H A Dhead.S37 # Must be done in this sequence as per the intel manual
79 /* Call boot_sys() (takes 2 parameters) and set restore_user_context() as */
80 /* return EIP. This will start the roottask as soon as boot_sys() returns. */
130 /* Call boot_node() and set restore_user_context() as return EIP. */
/seL4-refos-master/libs/libmuslc/dist/
H A Dconfig.mak32 # Uncomment for warnings (as errors). Might need tuning to your gcc version.
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/doc/
H A DGuidebook.tex63 the idea out of your head as you recall the tales of those who entered
84 at the local inn, becoming more and more depressed as you watch the odds
100 You have just begun a game of {\it NetHack}. Your goal is to grab as much
101 treasure as you can, retrieve the Amulet of Yendor, and escape the
144 disciplines have become capable of fighting as effectively without weapons
145 as with. They wear no armor but make up for it with increased mobility.
157 of place in a dungeon. They are, however, experts in archery as well
158 as tracking and stealthy movement.
235 seen on the current dungeon level; as you explore more of the level,
350 taken as goo
[all...]
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/doc/
H A DGuidebook.tex63 the idea out of your head as you recall the tales of those who entered
84 at the local inn, becoming more and more depressed as you watch the odds
100 You have just begun a game of {\it NetHack}. Your goal is to grab as much
101 treasure as you can, retrieve the Amulet of Yendor, and escape the
144 disciplines have become capable of fighting as effectively without weapons
145 as with. They wear no armor but make up for it with increased mobility.
157 of place in a dungeon. They are, however, experts in archery as well
158 as tracking and stealthy movement.
235 seen on the current dungeon level; as you explore more of the level,
350 taken as goo
[all...]
/seL4-refos-master/libs/libmuslc/src/internal/i386/
H A Dsyscall.s4 # and 5 args arriving as: eax, edx, ecx, edi, esi, 4(%esp).
/seL4-refos-master/libs/libmuslc/
H A Dconfigure7 To assign environment variables (e.g., CC, CFLAGS...), specify them as
27 --host=HOST same as --target
348 # it must be defined away as part of the CFLAGS.
499 # violations. We want to treat these as errors regardless of whether
586 # the dynamic linker to work, but enable it if it works as
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/src/
H A Dobjnam.c224 fruit_nam = pl_fruit; /* use it as is */
609 * because an identified object not described as "blessed" or
857 /* treat an object as fully ID'd when it might be used as reason for death */
1061 * verb is given in plural (without trailing s). Return as input
1073 /* various singular words that vtense would otherwise categorize as plural */
1098 * verb is given in plural (without trailing s). Return as input
1099 * if subj appears to be plural. Add special cases as necessary.
1149 * 2nd person singular behaves as if plural.
1704 absence of spaces and/or hyphens (such as "pickax
2044 struct alt_spellings *as = spellings; local
[all...]
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/src/
H A Dobjnam.c224 fruit_nam = pl_fruit; /* use it as is */
609 * because an identified object not described as "blessed" or
857 /* treat an object as fully ID'd when it might be used as reason for death */
1061 * verb is given in plural (without trailing s). Return as input
1073 /* various singular words that vtense would otherwise categorize as plural */
1098 * verb is given in plural (without trailing s). Return as input
1099 * if subj appears to be plural. Add special cases as necessary.
1149 * 2nd person singular behaves as if plural.
1704 absence of spaces and/or hyphens (such as "pickax
2044 struct alt_spellings *as = spellings; local
[all...]

Completed in 148 milliseconds