/seL4-refos-master/libs/libmuslc/src/linux/ |
H A D | ppoll.c | 6 int ppoll(struct pollfd *fds, nfds_t n, const struct timespec *to, const sigset_t *mask) argument 9 to ? (struct timespec []){*to} : 0, mask, _NSIG/8);
|
H A D | epoll.c | 25 int epoll_pwait(int fd, struct epoll_event *ev, int cnt, int to, const sigset_t *sigs) argument 27 int r = __syscall(SYS_epoll_pwait, fd, ev, cnt, to, sigs, _NSIG/8); 29 if (r==-ENOSYS && !sigs) r = __syscall(SYS_epoll_wait, fd, ev, cnt, to); 34 int epoll_wait(int fd, struct epoll_event *ev, int cnt, int to) argument 36 return epoll_pwait(fd, ev, cnt, to, 0);
|
/seL4-refos-master/libs/libmuslc/src/thread/ |
H A D | __timedwait.c | 15 struct timespec to, *top=0; local 21 if (__clock_gettime(clk, &to)) return EINVAL; 22 to.tv_sec = at->tv_sec - to.tv_sec; 23 if ((to.tv_nsec = at->tv_nsec - to.tv_nsec) < 0) { 24 to.tv_sec--; 25 to.tv_nsec += 1000000000; 27 if (to.tv_sec < 0) return ETIMEDOUT; 28 top = &to; [all...] |
/seL4-refos-master/libs/libmuslc/include/sys/ |
H A D | errno.h | 1 #warning redirecting incorrect #include <sys/errno.h> to <errno.h>
|
H A D | fcntl.h | 1 #warning redirecting incorrect #include <sys/fcntl.h> to <fcntl.h>
|
H A D | poll.h | 1 #warning redirecting incorrect #include <sys/poll.h> to <poll.h>
|
H A D | signal.h | 1 #warning redirecting incorrect #include <sys/signal.h> to <signal.h>
|
H A D | termios.h | 1 #warning redirecting incorrect #include <sys/termios.h> to <termios.h>
|
/seL4-refos-master/libs/libmuslc/include/ |
H A D | wait.h | 1 #warning redirecting incorrect #include <wait.h> to <sys/wait.h>
|
/seL4-refos-master/projects/seL4_libs/libsel4platsupport/src/ |
H A D | timer.c | 6 * This software may be distributed and modified according to the terms of 39 assert(timer->to.nirqs < MAX_IRQS); 40 for (size_t i = 0; i < timer->to.nirqs; i++) { 41 cleanup_timer_irq(vka, &timer->to.irqs[i]); 44 assert(timer->to.nobjs < MAX_OBJS); 45 for (size_t i = 0; i < timer->to.nobjs; i++) { 46 vka_free_object(vka, &timer->to.objs[i].obj); 52 assert(timer->to.nirqs < MAX_IRQS); 53 /* check which bits are set to find which irq to handl 191 sel4platsupport_init_timer_irqs(vka_t *vka, simple_t *simple, seL4_CPtr ntfn, seL4_timer_t *timer, timer_objects_t *to) argument 263 sel4platsupport_timer_objs_get_irq_cap(timer_objects_t *to, int id, irq_type_t type) argument [all...] |
/seL4-refos-master/libs/libsel4platsupport/src/ |
H A D | timer.c | 6 * This software may be distributed and modified according to the terms of 39 assert(timer->to.nirqs < MAX_IRQS); 40 for (size_t i = 0; i < timer->to.nirqs; i++) { 41 cleanup_timer_irq(vka, &timer->to.irqs[i]); 44 assert(timer->to.nobjs < MAX_OBJS); 45 for (size_t i = 0; i < timer->to.nobjs; i++) { 46 vka_free_object(vka, &timer->to.objs[i].obj); 52 assert(timer->to.nirqs < MAX_IRQS); 53 /* check which bits are set to find which irq to handl 191 sel4platsupport_init_timer_irqs(vka_t *vka, simple_t *simple, seL4_CPtr ntfn, seL4_timer_t *timer, timer_objects_t *to) argument 263 sel4platsupport_timer_objs_get_irq_cap(timer_objects_t *to, int id, irq_type_t type) argument [all...] |
/seL4-refos-master/kernel/manual/parts/ |
H A D | intro.tex | 11 The seL4 microkernel is an operating-system kernel designed to be 14 services to applications, such as abstractions to create and manage virtual address 16 of services provided by seL4 directly translates to a small 18 the ARMv6 version of the kernel to be formally proven in the Isabelle/HOL 19 theorem prover to adhere to its formal 30 seL4 kernel to userspace. 32 While we have tried to ensure that this manual accurately reflects the 35 under a particular circumstance needs to b [all...] |
H A D | io.tex | 13 may configure the kernel to signal a particular \obj{Notification} 15 interrupts to occur by calling \apifunc{seL4\_Wait}{sel4_wait} or 20 \obj{IRQHandler} capabilities represent the ability of a thread to 28 on this notification to 29 wait for interrupts to arrive. 34 interrupts to the application. 42 \obj{IRQControl} capability. This capability may be used to produce 56 In addition to managing \obj{IRQHandler} capabilities, x86 platforms require 57 the delivery location in the CPU vectors to be configured. Regardless of where 59 for delivery, ranging from VECTOR\_MIN to VECTO [all...] |
H A D | cspace.tex | 17 contain a capability. This may include capabilities to further 22 A CSpace address refers to an individual slot (in 24 capability. Threads refer to capabilities in their CSpaces (e.g. when 27 of the indices of the \obj{CNode} capabilities forming the path to the 31 % FIXME The references to mint in the following paragraph and previously in 32 % this section need to be cleaned up. They were clearly written at a time when 33 % it was not possible to change a capability's rights during a CNode_Copy. 42 selected capability. This mechanism can be used by servers to restore 43 sole authority to an object they have made available to client [all...] |
H A D | ipc.tex | 11 kernel-provided services. Messages are sent by invoking a capability to a 12 kernel object. Messages sent to \obj{Endpoint}s are destined for other 13 threads, while messages sent to other objects are processed by the kernel. This 22 The message words are sent to or received from a thread by placing them in its \emph{message registers}. 28 The IPC buffer is assigned to the calling thread (see \autoref{sec:threads} and \autoref{api:tcb_setipcbuffer}). 35 message registers and capabilities that the sending thread wishes to transfer, 39 label may, for example, be used to specify a requested operation. The 40 \texttt{capsUnwrapped} field is used only on the receive side, to indicate the 57 \ipcparam{seL4\_CPtr[]}{(in)}{caps}{Capabilities to transfer} 60 \ipcparam{seL4\_CPtr}{}{receiveCNode}{CPTR to [all...] |
/seL4-refos-master/libs/libmuslc/src/internal/i386_sel4/ |
H A D | syscall.s | 3 # We do some gymnastics here to pretend that a call to __syscall 5 # the same type we really just want to do a jmp, but need to
|
/seL4-refos-master/libs/libmuslc/src/internal/x86_64_sel4/ |
H A D | syscall.s | 3 # We do some gymnastics here to pretend that a call to __syscall 5 # the same type we really just want to do a jmp, but need to
|
/seL4-refos-master/projects/refos/design/ |
H A D | appendix.tex | 6 % This software may be distributed and modified according to the terms of 39 \caption{Using zero fill to allocate an empty frame.} 56 --- [ label = "assume A has the cap to talk to the pager and they can talk to each other"]; 66 R box R [ label = "find frames win\_capA\_frames mapped to win\_capA and book keep"]; 74 \caption{Protocol for sharing a memory object from client A to client B.} 78 \subsection{Shared buffer initialisation in A for argument passing to B} 147 N box N [ label = "find the object according to \"mobject\_name\""]; 173 R box R [ label = "receive call to fin [all...] |
H A D | intro.tex | 6 % This software may be distributed and modified according to the terms of 15 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}. 24 \texttt{Methods} are conceptual "function calls" although they are usually implemented via communication with another process in which case they are actually remote procedure calls. Regardless of the underlying implementation, methods here refer to the actual procedures of an interface which get invoked. 26 \texttt{Interfaces} are a collection of (usually related) methods that usually serve to abstract a conceptual object. For instance, the \texttt{C} standard library functions \texttt{fopen}, \texttt{fscanf}, \texttt{fprintf}, \texttt{fclose} and so on form an abstract interface and provide abstraction for a file object. 30 \texttt{Protocols} here refer to [all...] |
H A D | interface.tex | 6 % This software may be distributed and modified according to the terms of 13 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. 15 Further implementations beyond \refOS may choose to extend these interfaces to provide extra system functionality and to attach additional interfaces. 20 Servers implement interfaces which provide management (creation, destruction, monitoring, sharing and manipulation) of objects. For example, an audio device may implement the dataspace interface for UNIX \texttt{/dev/audio} which gives the abstraction to manage audio objects. 22 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 uniquel [all...] |
/seL4-refos-master/libs/libmuslc/dist/ |
H A D | config.mak | 17 # Uncomment if you want to build i386 musl on a 64-bit host 20 # Uncomment to fix broken distro-patched toolchains where hash-style=gnu(only) 23 # Uncomment to fix broken distro-patched toolchains where stack-protector=on 29 # Uncomment to omit massive GCC4 DWARF2 bloat (only useful for debugging) 32 # Uncomment for warnings (as errors). Might need tuning to your gcc version. 33 #CFLAGS += -Werror -Wall -Wpointer-arith -Wcast-align -Wno-parentheses -Wno-char-subscripts -Wno-uninitialized -Wno-sequence-point -Wno-missing-braces -Wno-unused-value -Wno-overflow -Wno-int-to-pointer-cast 35 # Uncomment if you want to disable building the shared library.
|
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/doc/ |
H A D | Guidebook.tex | 37 \title{\LARGE A Guide to the Mazes of Menace:\\ 52 Recently, you have begun to find yourself unfulfilled and distant 56 fact been having those dreams all your life, and somehow managed to 59 powerful creatures that seem to be lurking behind every corner of the 61 As each night passes, you feel the desire to enter the mysterious caverns 65 the yearning to seek out the fantastic place in your dreams no longer. 68 through the first time. And who was to say that all of those who did 75 immortality by the gods. The amulet is rumored to be somewhere beyond the 78 undiscovered reason that you are to descend into the caverns and seek 80 powers are untrue, you decide that you should at least be able to sel [all...] |
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/doc/ |
H A D | Guidebook.tex | 37 \title{\LARGE A Guide to the Mazes of Menace:\\ 52 Recently, you have begun to find yourself unfulfilled and distant 56 fact been having those dreams all your life, and somehow managed to 59 powerful creatures that seem to be lurking behind every corner of the 61 As each night passes, you feel the desire to enter the mysterious caverns 65 the yearning to seek out the fantastic place in your dreams no longer. 68 through the first time. And who was to say that all of those who did 75 immortality by the gods. The amulet is rumored to be somewhere beyond the 78 undiscovered reason that you are to descend into the caverns and seek 80 powers are untrue, you decide that you should at least be able to sel [all...] |
/seL4-refos-master/libs/libmuslc/src/signal/mips64/ |
H A D | sigsetjmp.s | 11 # comparing save mask with 0, if equals to 0 then 12 # sigsetjmp is equal to setjmp. 26 move $4, $16 # Restore the pointer-to-sigjmp_buf
|
/seL4-refos-master/libs/libmuslc/src/signal/mipsn32/ |
H A D | sigsetjmp.s | 11 # comparing save mask with 0, if equals to 0 then 12 # sigsetjmp is equal to setjmp. 26 move $4, $16 # Restore the pointer-to-sigjmp_buf
|