/seL4-camkes-master/kernel/manual/parts/ |
H A D | bootup.tex | 11 The seL4 kernel creates a minimal boot environment for the initial thread, which 23 which contains capabilities to the initial 73 which capabilities are stored where in its CNode, the kernel provides 74 a \emph{BootInfo Frame} which is mapped into the initial thread's address 85 which contains \texttt{start} and \texttt{end} slot CPTRs. It denotes a region 150 ordered by the virtual address at which the corresponding objects are mapped 157 Userland typically has a way of finding out to which virtual addresses its 162 It's also assumed that the initial thread knows which paging structures are 210 On IA-32, seL4 accepts boot command-line arguments which are passed to the
|
H A D | io.tex | 44 system. Typically, the initial thread of a system will determine which 81 \apifunc{seL4\_X86\_IOPort\_In32}{x86_io_port_in32} methods, which 88 and an unsigned integer~\texttt{port}, which indicates the I/O port to read from 102 \obj{IOPortControl} capability, which can be used to \apifunc{seL4\_X86\_IOPort\_Issue}{x86_ioport_issue} 139 which can take the 156 consist of several independent functions, each of which may be addressed 186 which allows system software to manage access rights and address translation for 227 track which VSpace a context bank has bound to it, and which context bank a 234 TLB maintenance is handled by the kernel via tracking which contex [all...] |
H A D | ipc.tex | 41 manner in which capabilities were received. It is described in 60 \ipcparam{seL4\_CPtr}{}{receiveCNode}{CPTR to a CNode from which to 92 There is space for this field in the \texttt{seL4\_IPCBuffer} structure, which the kernel ignores. 143 Messages may contain capabilities, which will be copied to the 155 in which it is willing to receive a capability, with three fields within the IPC buffer: \texttt{receiveCNode}, \texttt{receiveIndex} and \texttt{receiveDepth}. 157 the slot in which to put the capability. Capability 167 which the message is sent, the capability is \emph{unwrapped}: its badge is placed into 182 third capability in the sender's message which could not be unwrapped.
|
H A D | objects.tex | 69 space}; an address in this space refers to a \emph{slot} which may or 128 % kernel objects) go to the API reference which is very terse and not nearly as 136 important variant is the \emph{Call} operation, which consists of a standard 137 \emph{Send} operation atomically followed by a variant of \emph{Receive} which 229 invoking the reply capability with \apifunc{seL4\_Send}{sel4_send} which is 283 Initially, there is a capability to \obj{SchedControl} for each node, which 284 allows scheduling context to be populated with parameters, which combined with priority 297 capabilities can have the grant right, which allows sending 306 is a word-size array of flags, each of which behaves like a binary semaphore. Operations 323 which allow [all...] |
H A D | threads.tex | 26 \autoref{ch:cspace}) and VSpace (see \autoref{ch:vspace}) which 28 (see \autoref{ch:ipc}), which is used to pass extra arguments during IPC 73 % an example of which is demonstrated in \nameref{ex:second_thread}. 82 thread capability from which to use the MCP from. Threads can only set priorities and MCPs 125 Otherwise the kernel uses \emph{sporadic servers} to enforce temporal isolation, which enforce the 144 budget is charged. Round-robin threads have two refills only, both of which are always ready to be 149 Sporadic threads behave differently depending on the amount of replenishments available, which 168 replenishment which can result in preemption if the next replenishment is not yet available. 199 invoke the appropriate \obj{SchedControl} capability, which provides access to CPU time management 203 \apifunc{seL4\_SchedControl\_Configure}{schedcontrol_configure}, which allow [all...] |
H A D | vspace.tex | 58 On IA-32, the VSpace is realised as a \texttt{PageDirectory}, which covers the entire 4\,GiB range 87 Like IA-32, ARM AArch32 realise the VSpace as a \texttt{PageDirectory}, which covers the entire 180 sizes, as well as the \emph{mapping level}, which refers to 181 the level of the paging structure at which this page must be mapped.
|
/seL4-camkes-master/tools/cogent/regression/ |
H A D | run_tests.py | 58 def which(file): function 119 if which("pidspace") != None: 120 command = [which("pidspace"), "--"] + command 284 # Calculate which tests should be run.
|
/seL4-camkes-master/projects/musllibc/src/fenv/sh/ |
H A D | fenv.S | 66 ! preserve the current precision bit, which we do not know a priori
|
/seL4-camkes-master/projects/picotcp/docs/user_manual/ |
H A D | chap_api_dhcp_c.tex | 10 Initiate a DHCP negotiation. The user passes a callback-function, which will be executed on DHCP success or failure. 21 \item \texttt{device} - the device on which a negotiation should be started. 22 \item \texttt{callback} - the function which is executed on success or failure. This function can be called multiple times. F.e.: initially DHCP succeeded, then the DHCP server is removed long enough from the network for the lease to expire, later the server is added again to the network. The callback is called 3 times: first with code \texttt{PICO\_DHCP\_SUCCESS}, then with \texttt{PICO\_DHCP\_RESET} and finally with \texttt{PICO\_DHCP\_SUCCESS}. The callback may be called before \texttt{pico\_dhcp\_initiate\_negotiation} has returned, f.e. in case of failure to open a socket. The callback has two parameters: 32 \item \texttt{PICO\_DHCP\_SUCCESS} - DHCP succeeded, the user can start using the assigned address, which can be obtained by calling \texttt{pico\_dhcp\_get\_address}.
|
H A D | chap_api_dhcp_d.tex | 16 \item \texttt{settings} - a pointer to a struct \texttt{pico\_dhcpd\_settings}, in which the following members matter to the user :
|
H A D | chap_api_sntp_c.tex | 83 \item \texttt{tv} - Pointer to a time$\_$val struct in which the current time will be set.
|
H A D | chap_api_dns_sd.tex | 31 \item \texttt{port} - The portnumber on which the service runs.
|
H A D | chap_api_mdns.tex | 4 This module can register DNS resource records on the network via Multicast DNS as either \textbf{\emph{shared}} or \textbf{\emph{unique}} records. Unique records are, as the name implies, unique on the network (the record-name and -type combination is unique) and one single host has claimed the ownership of them. Shared records are records that are not unique on the network, which means multiple hosts can register records with the same record-name and -type combination. For more information on shared and unique resource record sets, see RFC6762. 114 \item \texttt{record$\_$tree} - mDNS record-tree with records to register on the network via Multicast DNS. Can contain \textbf{\emph{unique records}} as well as \textbf{\emph{shared records}}. Declare a mDNS record-tree with the macro 'PICO$\_$MDNS$\_$RTREE$\_$DECLARE(name)', which is actually just a pico$\_$tree-struct, with a comparing-function already set. Records can be added with the preprocessor macro 'PICO$\_$MDNS$\_$RTREE$\_$ADD(pico$\_$mdns$\_$rtree *, struct pico$\_$mdns$\_$record *)'. To create mDNS records see 'pico$\_$mdns$\_$record$\_$create'.
|
/seL4-camkes-master/tools/cogent/cogent/scripts/ |
H A D | man-gen.pl | 18 use File::Which qw(which); 35 system "which $cogent_bin >/dev/null";
|
/seL4-camkes-master/projects/musllibc/src/internal/i386/ |
H A D | syscall.s | 6 # ebx or ebp (which are unavailable in PIC and frame-pointer-using
|
/seL4-camkes-master/projects/camkes-tool/camkes/templates/tests/ |
H A D | testmacros.py | 35 from camkes.internal.tests.utils import CAmkESTest, which namespace
|
/seL4-camkes-master/projects/capdl/capDL-tool/ |
H A D | Makefile | 22 which xmllint && xmllint --noout --dtdvalid ./capdl.dtd $*.xml
|
/seL4-camkes-master/tools/cogent/cogent/doc/ |
H A D | doc.tex | 441 8-bit integer, which corresponds to 445 \inlinecogent{String} is a type which does not relate to \inlinecogent{U8} in any way. This type is mainly used 460 \paragraph{Unit type} Unit type (\inlinecogent{()}) has only one inhabitant, which is unit (also spelt as \inlinecogent{()}). 465 statically and implicitly allocated on the stack. For heap-allocated objects, we need to manage the references to them, which is 467 given point in the program.~\footnote{There are exceptions to this, which will be discussed shortly.} 478 In some cases, we want to create read-only ``copies'' of an object (say, giving them to other functions which only needs to inspect them). 492 In this expression, \inlinecogent{obj} is a linear object. \inlinecogent{!obj} creates a context inside which 503 which violates the uniqueness type system. 516 be a type which is non-linear, whereas no constraints are posed on what permissions \inlinecogent{b} can have. 530 one reference (to the ``box'' itself because the ``box'' is on the heap) regardless of its fields (which [all...] |
/seL4-camkes-master/projects/projects_libs/libjansson/jansson-2.7/ |
H A D | compile | 2 # Wrapper for compilers which do not understand '-c -o'. 243 Wrapper for compilers which do not understand '-c -o'.
|
/seL4-camkes-master/tools/rumprun/tests/configure/build-aux/ |
H A D | compile | 2 # Wrapper for compilers which do not understand '-c -o'. 243 Wrapper for compilers which do not understand '-c -o'.
|
/seL4-camkes-master/tools/cogent/cogent/ |
H A D | Makefile | 112 ifeq ($(shell which cogent 2> /dev/null; echo $$? ),1)
|
/seL4-camkes-master/projects/camkes/apps/cakeml_regex/components/CakeMLFilter/ |
H A D | filterProgScript.sml | 16 (* The regexp wrt. which we're filtering *) 17 (* Read from the cmakeConstants SML module which is generated by the *)
|
/seL4-camkes-master/tools/rumprun/platform/xen/xen/arch/x86/ |
H A D | x86_32.S | 151 # provides the number of bytes which have already been popped from the
|
/seL4-camkes-master/kernel/src/arch/x86/32/ |
H A D | traps.S | 516 # ESP : points to tss.esp0 which points to the end of the thread's registers array
|
/seL4-camkes-master/tools/cogent/cogent/tests/ |
H A D | run-test-suite.py | 72 # Takes in a function which returns 448 cogent = shutil.which(args.cogent)
|