/seL4-l4v-master/seL4/include/api/ |
H A D | debug.h | 16 #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 D | ml_console.scala | 75 val process_result = Future.thread[Int]("process_result") {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/ |
H A D | ml_console.scala | 75 val process_result = Future.thread[Int]("process_result") {
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | objects.tex | 66 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 D | cspace.tex | 10 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 D | machine.h | 97 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 D | objecttype.c | 564 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 D | objecttype.c | 507 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 D | Event_Timer.sml | 6 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 D | Future.sml | 72 | 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 D | vcpu.c | 130 /* 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 D | SingleAssignment.sml | 34 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 D | simplifier_trace.scala | 88 /* 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 D | simplifier_trace.scala | 88 /* 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 D | Thread_Attributes.sml | 30 (* thread attributes *) 43 (* access thread flags *)
|
/seL4-l4v-master/seL4/src/arch/x86/32/ |
H A D | traps.S | 18 # 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 D | debugger_dockable.scala | 66 /* 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 D | debugger_dockable.scala | 66 /* 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 D | bash.scala | 194 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 D | bash.scala | 194 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 D | intro.tex | 24 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 D | vspace.h | 15 #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 D | faults.c | 11 #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 D | objecttype.c | 305 void Arch_prepareThreadDelete(tcb_t *thread) argument 308 fpuThreadDelete(thread);
|
/seL4-l4v-master/seL4/src/object/ |
H A D | objecttype.c | 27 #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
|