Searched refs:thread (Results 76 - 100 of 155) sorted by relevance

1234567

/seL4-l4v-master/seL4/include/api/
H A Ddebug.h16 #include <kernel/thread.h>
68 /* Prints the user context and stack trace of the current thread */
72 printf("Current thread: %s\n", TCB_PTR_DEBUG_PTR(tptr)->tcbName);
113 fail("Unknown thread state");
/seL4-l4v-master/isabelle/src/Pure/ML/
H A Dml_console.scala75 val process_result = Future.thread[Int]("process_result") {
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/
H A Dml_console.scala75 val process_result = Future.thread[Int]("process_result") {
/seL4-l4v-master/seL4/manual/parts/
H A Dobjects.tex66 object (such as a thread control block) and carries access rights that
121 message will be transferred through the kernel to another thread.
124 object. For example, invoking a thread control block (TCB) capability with a
125 correctly formatted message will suspend the target thread.
156 calling thread's timeslice and causes invocation of the kernel's scheduler.
158 the calling thread will immediately be scheduled with a fresh timeslice. In
164 ready to receive the message immediately, the sending thread will block
168 \item[\apifunc{seL4\_Recv}{sel4_recv}] (``receive'') is used by a thread to
194 dropped. The sending thread continues execution. As with
197 \item[\apifunc{seL4\_NBRecv}{sel4_nbrecv}] is used by a thread t
[all...]
H A Dcspace.tex10 capability-based access control model. Each userspace thread has an
12 capabilities that the thread possesses, thereby governing which
13 resources the thread can access.
18 \obj{CNode}s, forming a directed graph. Conceptually a thread's CSpace
114 kernel-generated reply capability of the current thread from the
290 CNode containing the last capability to the TCB of the thread
292 deleted as a result of the revoke. In this case the thread performing
310 When performing a system call, a thread specifies to the kernel the
327 The kernel stores a capability to the root \obj{CNode} of each thread's
328 CSpace in the thread'
[all...]
/seL4-l4v-master/seL4/include/arch/x86/arch/
H A Dmachine.h97 word_t PURE getRestartPC(tcb_t *thread);
98 void setNextPC(tcb_t *thread, word_t v);
326 static inline void x86_load_fsgs_base(tcb_t *thread, cpu_id_t cpu) argument
334 word_t fs_base = getRegister(thread, FS_BASE);
336 word_t gs_base = getRegister(thread, GS_BASE);
/seL4-l4v-master/seL4/src/arch/arm/32/object/
H A Dobjecttype.c564 Arch_prepareThreadDelete(tcb_t * thread) { argument
566 fpuThreadDelete(thread);
570 if (thread->tcbArch.tcbVCPU) {
571 dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);
/seL4-l4v-master/seL4/src/arch/arm/64/object/
H A Dobjecttype.c507 Arch_prepareThreadDelete(tcb_t * thread) { argument
509 fpuThreadDelete(thread);
513 if (thread->tcbArch.tcbVCPU) {
514 dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/
H A DEvent_Timer.sml6 Note: events are run as synchronized action within a dedicated thread
75 State of {requests: requests, status: status, manager: Thread.thread option};
92 (* manager thread *)
H A DFuture.sml72 | NONE => raise Fail "Missing worker thread context");
139 val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
150 val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
163 val _ = running |> List.app (fn thread =>
164 if Standard_Thread.is_self thread then ()
165 else Standard_Thread.interrupt_unsynchronized thread);
344 (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
518 (* task context for running thread *)
633 raise Fail "Cannot shutdown while running as worker thread"
[all...]
/seL4-l4v-master/seL4/src/arch/arm/object/
H A Dvcpu.c130 /* Current VCPU being active should indicate that the current thread
204 /* Current VCPU being active should indicate that the current thread
291 /* sanitize the CPSR as without a VCPU a thread should only be in user mode */
328 tcb_t *thread; local
329 thread = NODE_STATE(ksCurThread);
332 word_t *ipcBuffer = lookupIPCBuffer(true, thread);
333 setRegister(thread, badgeRegister, 0);
334 unsigned int length = setMR(thread, ipcBuffer, 0, value);
335 setRegister(thread, msgInfoRegister, wordFromMessageInfo(
/seL4-l4v-master/HOL4/polyml/basis/
H A DSingleAssignment.sml34 this will raise `Locked`. Note that this function is not thread-safe. A `mutex`
88 be built and a thread created to build it. When the thread completes it assigns
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dsimplifier_trace.scala88 /* manager thread */
290 case Some(thread) if thread.is_active => thread
291 case _ => error("Bad Simplifier_Trace.manager thread")
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dsimplifier_trace.scala88 /* manager thread */
290 case Some(thread) if thread.is_active => thread
291 case _ => error("Bad Simplifier_Trace.manager thread")
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DThread_Attributes.sml30 (* thread attributes *)
43 (* access thread flags *)
/seL4-l4v-master/seL4/src/arch/x86/32/
H A Dtraps.S18 # On kernel entry, ESP points to the end of the thread's registers array.
379 # __idle_thread_end then this is the idle thread. Interrupts from the idle thread
424 * userspace thread.
436 * EFLAGS.TF for the userspace thread before it returns.
516 # ESP : points to tss.esp0 which points to the end of the thread's registers array
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Ddebugger_dockable.scala66 /* component state -- owned by GUI thread */
143 for (thread <- thread_contexts) {
144 val thread_node = new DefaultMutableTreeNode(thread)
145 for ((debug_state, i) <- thread.debug_states.zipWithIndex)
146 thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
210 tooltip = "Continue program on current thread, until next breakpoint"
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Ddebugger_dockable.scala66 /* component state -- owned by GUI thread */
143 for (thread <- thread_contexts) {
144 val thread_node = new DefaultMutableTreeNode(thread)
145 for ((debug_state, i) <- thread.debug_states.zipWithIndex)
146 thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
210 tooltip = "Continue program on current thread, until next breakpoint"
/seL4-l4v-master/isabelle/src/Pure/System/
H A Dbash.scala194 Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
196 Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
/seL4-l4v-master/l4v/isabelle/src/Pure/System/
H A Dbash.scala194 Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
196 Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
/seL4-l4v-master/l4v/camkes/adl-spec/document/
H A Dintro.tex24 can have a thread of control or be invoked via an event loop. CAmkES
/seL4-l4v-master/seL4/include/arch/x86/arch/kernel/
H A Dvspace.h15 #define IT_ASID 1 /* initial thread's ASID */
80 word_t *PURE lookupIPCBuffer(bool_t isReceiver, tcb_t *thread);
81 exception_t handleVMFault(tcb_t *thread, vm_fault_type_t vm_faultType);
/seL4-l4v-master/seL4/src/api/
H A Dfaults.c11 #include <kernel/thread.h>
12 #include <arch/kernel/thread.h>
152 * set, we can still allow the thread to continue because replying
153 * should uniformly resume thread execution, based on the general seL4
178 /* Replying will always resume the thread: the only variant behaviour
179 * is whether or not the thread will be resumed with stepping still
/seL4-l4v-master/seL4/src/arch/riscv/object/
H A Dobjecttype.c305 void Arch_prepareThreadDelete(tcb_t *thread) argument
308 fpuThreadDelete(thread);
/seL4-l4v-master/seL4/src/object/
H A Dobjecttype.c27 #include <kernel/thread.h>
710 userError("Cannot invoke thread capabilities in the first phase of an invocation");
805 exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant) argument
807 doReplyTransfer(thread, reply, canGrant);
811 exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant) argument
813 doReplyTransfer(NODE_STATE(ksCurThread), thread, slot, canGrant); local

Completed in 184 milliseconds

1234567