/seL4-camkes-master/tools/seL4/elfloader-tool/include/arch-arm/armv/armv6/armv/ |
H A D | smp.h | 14 #error SMP is not supported on ARMv6
|
/seL4-camkes-master/projects/musllibc/src/ldso/powerpc/ |
H A D | dlsym.s | 6 mflr 5 # The return address is arg3.
|
/seL4-camkes-master/projects/musllibc/src/ldso/powerpc64/ |
H A D | dlsym.s | 9 mflr 5 # The return address is arg3.
|
/seL4-camkes-master/projects/picotcp/docs/user_manual/ |
H A D | chap_api_sntp_c.tex | 20 \item \texttt{cb$\_$synced} - Callback function that is called when the synchronisation process is done. The status variable indicates wheter the synchronisation was successful or not. 24 On success, this call returns 0 if the synchronisation operation has successfully started. When both IPv4 and IPv6 are enabled, success on one is sufficient. 25 On error, -1 is returned and \texttt{pico$\_$err} is set appropriately. 52 \item \texttt{cb$\_$synced} - Callback function that is called when the synchronisation process is done. The status variable indicates wheter the synchronisation was successful or not. 56 On success, this call returns 0 if the synchronisation operation has successfully started. When both IPv4 and IPv6 are enabled, success on one is sufficient. 57 On error, -1 is returned and \texttt{pico$\_$err} is se [all...] |
H A D | chap_api_olsr.tex | 4 OLSR is a proactive routing protocol for mobile ad-hoc networks 5 (MANETs). It is well suited to large and dense mobile 12 OLSR is well suited for networks, where the traffic is random and 15 protocol, OLSR is also suitable for scenarios where the communicating 16 pairs change over time: no additional control traffic is generated in 41 0 returned if the device is successfully added.
|
H A D | chap_api_ipv6.tex | 9 The result is stored in the char array that ipbuf points to. 24 On error, -1 is returned and \texttt{pico$\_$err} is set appropriately. 39 Convert the IPv6 colon:hex notation into binary form. The result is stored in the 57 On error, -1 is returned and \texttt{pico$\_$err} is set appropriately. 69 \subsection{pico$\_$ipv6$\_$is$\_$unicast} 72 Check if the provided address is unicast or multicast. 94 \subsection{pico$\_$ipv6$\_$is$\_$multicast} 96 Check if the provided address is [all...] |
H A D | chap_api_aodv.tex | 4 AODV is a reactive routing protocol for mobile ad-hoc networks 7 of nodes is foreseen. 9 towards a remote node, and the route is created ad-hoc upon the demand 12 and maintain routes is kept as low as possible. 34 0 returned if the device is successfully added.
|
H A D | chap_api_mld.tex | 4 This module allows the user to join and leave ipv6 multicast groups. The module is based on the MLD version 2 protocol and it's backwards compatible with version 1. 5 The MLD module is completly driven from socket calls (\ref{socket:setoption}) and non of the MLD application interface functions should be called by the user. If however, by any reason, it's necessary for the user to do this, the following function call is provided: 28 In case of failure, -1 is returned, and the value of pico$\_$err 29 is set as follows:
|
H A D | chap_api_ipv4.tex | 9 The result is stored in the char array that ipbuf points to. The given IP address argument must be in network order (i.e. 0xC0A80101 becomes 192.168.1.1). 24 On error, -1 is returned and \texttt{pico$\_$err} is set appropriately. 41 Convert the IPv4 dotted-decimal notation into binary form. The result is stored in the 42 \texttt{int} that IP points to. Little endian or big endian is not taken into account. 59 On error, -1 is returned and \texttt{pico$\_$err} is set appropriately. 88 On success, this call returns the netmask in CIDR notation is returned if the netmask is valid. 89 On error, -1 is returne [all...] |
H A D | chap_api_sock.tex | 32 \item \texttt{PICO$\_$SOCK$\_$EV$\_$RD} - triggered when new data arrives on the socket. A new receive action can be taken by the socket owner because this event indicates there is new data to receive. 34 \item \texttt{PICO$\_$SOCK$\_$EV$\_$CONN} - triggered when connection is established (TCP only). This event is received either after a successful call to \texttt{pico$\_$socket$\_$connect} to indicate that the connection has been established, or on a listening socket, indicating that a call to \texttt{pico$\_$socket$\_$accept} may now be issued in order to accept the incoming connection from a remote host. 35 \item \texttt{PICO$\_$SOCK$\_$EV$\_$CLOSE} - triggered when a FIN segment is received (TCP only). This event indicates that the other endpont has closed the connection, so the local TCP layer is only allowed to send new data until a local shutdown or close is initiated. PicoTCP is able to keep the connection half-open (only for sending) after the FIN packet has been received, allowing new data to be sent in the TCP CLOSE$\_$WAIT state. 36 \item \texttt{PICO$\_$SOCK$\_$EV$\_$FIN} - triggered when the socket is closed. No further communication is possible from this point on the socket. 42 On error the socket is no [all...] |
H A D | chap_api_dhcp_d.tex | 26 On successful startup of the dhcp server, 0 is returned. 27 On error, -1 is returned, and \texttt{pico$\_$err} is set appropriately. 54 On success, 0 is returned. 55 On error, -1 is returned, and \texttt{pico$\_$err} is set appropriately.
|
H A D | chap_api_igmp.tex | 4 This module allows the user to join and leave ipv4 multicast groups. The module is based on the IGMP version 3 protocol and it's backwards compatible with version 2. Version 1 is not supported. 5 The IGMP module is completly driven from socket calls (\ref{socket:setoption}) and non of the IGMP application interface functions should be called by the user. If however, by any reason, it's necessary for the user to do this, the following function call is provided: 28 In case of failure, -1 is returned, and the value of pico$\_$err 29 is set as follows:
|
/seL4-camkes-master/tools/cogent/cogent/manual/ |
H A D | cogent-manual.tex | 86 For me the best way to do so is by writing it down in an organized way. Since I found that there was no similar documentation, 92 This manual is not intended as a tutorial for programming in \cogent or to prove properties of \cogent programs. The examples 94 ``surface syntax'' which is the interface for the programmer. Note that most publications about \cogent refer to the more 95 concise ``core syntax'' which is created from the surface syntax by applying the ``desugaring rules''. 112 f: U8 -> U8 -- this is a line comment after a function signature 113 f x {- x is the function argument -} = x+1 120 {- This is a comment with a nested {- inner comment. -} 130 @@ This is a standalone documentation block 233 The type of a character literal is \code{U8} (see below), which corresponds to a single byte. 239 \code{'}\verb|\|\code{300'} is no [all...] |
/seL4-camkes-master/projects/musllibc/src/math/ |
H A D | powf.c | 11 * software is freely granted, provided that this notice 12 * is preserved. 53 int32_t hx,hy,ix,iy,is; local 60 /* x**0 = 1, even if x is NaN */ 63 /* 1**y = 1, even if y is NaN */ 66 /* NaN if either arg is NaN */ 70 /* determine if y is an odd int when x < 0 71 * yisint = 0 ... y is not an integer 72 * yisint = 1 ... y is an odd int 73 * yisint = 2 ... y is a [all...] |
/seL4-camkes-master/projects/camkes-tool/camkes/templates/ |
H A D | camkesConstants.sml | 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 18 /*- if value is not none -*/
|
/seL4-camkes-master/kernel/manual/parts/ |
H A D | notifications.tex | 39 select-style wait on the set of semaphores: If the notification word is 40 zero at the time \apifunc{seL4\_Wait}{sel4_wait} is called, the 45 The \apifunc{seL4\_Poll}{sel4_poll} is the same as \apifunc{seL4\_Wait}{sel4_wait}, except if 46 no signals are pending (the notification word is 0) the call will return immediately 50 \apifunc{seL4\_Signal}{sel4_signal} is invoked, the first queued thread 52 next time the notification is signalled. 59 \obj{Notification} is bound to a \obj{TCB}, signals to that notification object 60 will be delivered even if the thread is receiving from an IPC 68 \apifunc{seL4\_Wait}{sel4_wait} on the notification is the bound thread.
|
H A D | ipc.tex | 10 between threads. The same mechanism is also used for communication with 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}). 29 %FIXME: seL4_TCB_SetIPCBuffer is only mentioned in the API reference! 37 transferred. The label is not interpreted by the 38 kernel and is passed unmodified as the first data payload of the message. The 40 \texttt{capsUnwrapped} field is used only on the receive side, to indicate the 41 manner in which capabilities were received. It is described in 91 The situation is similar for the tag field. 92 There is spac [all...] |
H A D | threads.tex | 15 time is also represented by the thread abstraction. 16 A thread is represented in seL4 by its thread control block 19 With MCS, a scheduling context is represented by a scheduling context object 28 (see \autoref{ch:ipc}), which is used to pass extra arguments during IPC 30 registers. While it is not compulsory that a thread has an IPC buffer, 35 %FIXME: there is much more information held in the TCB! 42 \autoref{sec:kernmemalloc}). A newly created thread is initially inactive. It 43 is configured by setting its CSpace and VSpace with the 57 corresponding to the affinity of the thread. For master, this is set using 58 \apifunc{seL4\_TCB\_SetAffinity}{tcb_setaffinity}, while on the MCS kernel the affinity is [all...] |
H A D | bootup.tex | 12 is started at priority \texttt{seL4\_MaxPrio} and maximum control priority \texttt{seL4\_MaxPrio}. 17 On the MCS kernel, the initial thread is configured with a round-robin scheduling context 25 The CNode size can be configured at compile time (default is $2^{12}$ 26 slots), but the guard is always chosen so that the CNode resolves exactly 74 a \emph{BootInfo Frame} which is mapped into the initial thread's address 75 space. The mapped address is chosen by the kernel and given to the initial 80 It is defined in the seL4 userland library. Besides talking about 84 The type \texttt{seL4\_SlotRegion} is a C struct 120 information. If \texttt{extraLen} is greater then zero then 4K after the start of bootinfo 121 is [all...] |
H A D | objects.tex | 16 Note that some services are available only when the kernel is configured for 65 A capability is an unforgeable token that references a specific kernel 73 capability model is an instance of a \emph{segregated} (or \emph{partitioned}) 77 \emph{capability nodes} (\obj{CNode}s). A \obj{CNode} is a table of 79 address of a capability in a capability space is the concatenation of the indices 95 capabilities through the system is controlled by a 114 threads. This mechanism is also used for communication with kernel-provided 115 services. There is a standard message format, each message containing a 120 When an endpoint, notification or reply capability is invoked in this way, the 128 % kernel objects) go to the API reference which is ver [all...] |
H A D | cspace.tex | 16 \obj{CNode}s. A \obj{CNode} is a table of slots, each of which may 19 is the portion of the directed graph that is reachable starting with 20 the \obj{CNode} capability that is its CSpace root. 26 capability in question. An address in a CSpace is the concatenation 49 programmer is responsible for constructing CSpaces as well as 63 memory and has the capacity to hold exactly one capability. This is 16 87 \item[\apifunc{seL4\_CNode\_Copy}{cnode_copy}] is similar to 92 to the slot in which it is currently. 99 capabilities between three specified capability slots. It is [all...] |
H A D | io.tex | 76 Access to I/O ports is controlled by \obj{IO Port} capabilities. Each 78 it. Reading from I/O ports is accomplished with the 83 Similarly, writing to I/O ports is accomplished with the 94 A \texttt{seL4\_IllegalOperation} code is returned if port access is 99 and \texttt{error}, is returned from these API calls. 103 \obj{IO Port} capabilities to sub ranges of I/O ports. Any range that is issued 110 is bypassed when the device accesses memory. In seL4, device drivers run 113 access or corrupt memory that is not part of its address space, thus 141 There is n [all...] |
/seL4-camkes-master/projects/seL4_libs/libsel4platsupport/src/sel4_arch/x86_64/ |
H A D | crt0.S | 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 18 * - _start is an undefined external symbol (force this by passing 46 # the return value is in rax
|
/seL4-camkes-master/projects/camkes-tool/tools/ |
H A D | tpp | 9 # the BSD 2-Clause license. Note that NO WARRANTY is provided. 80 '\'condense\' is True') 89 'fix indentation level of statements when the \'lock_indent\' is ' \ 95 if indentation is not None: 104 if cowsay is not None: 119 'property is set to True') 123 if self.accumulated is None: 131 assert self.accumulated is None 134 if not properties.get('accumulate', False) and self.accumulated is not None: 227 if directive is no [all...] |
/seL4-camkes-master/kernel/include/arch/riscv/arch/64/mode/ |
H A D | hardware.h | 14 * The top half of the address space is reserved for the kernel. This means that 256 top level 23 * that contain a 2nd level PageTable consisting of 2MiB page entries is the entry 25 * of the kernel ELF in the kernel window. The same 2nd level PageTable is used and so both 108 #error Only PT_LEVELS == 3 is supported
|