/seL4-l4v-10.1.1/seL4/include/api/ |
H A D | faults.h | 18 word_t setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer); 19 word_t Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType); 21 bool_t handleFaultReply(tcb_t *receiver, tcb_t *sender); 22 bool_t Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType);
|
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/x86/sel4/arch/ |
H A D | syscalls.h | 22 seL4_Wait(seL4_CPtr src, seL4_Word *sender) argument 24 seL4_Recv(src, sender); 28 seL4_Poll(seL4_CPtr src, seL4_Word *sender) argument 30 return seL4_NBRecv(src, sender);
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/api/ |
H A D | faults.c | 21 Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType) argument 39 Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType) argument 45 va = getRestartPC(sender); 49 setMR(receiver, receiveIPCBuffer, seL4_VMFault_IP, getRestartPC(sender)); 52 seL4_Fault_VMFault_get_address(sender->tcbFault)); 54 seL4_Fault_VMFault_get_instructionFault(sender->tcbFault)); 56 seL4_Fault_VMFault_get_FSR(sender->tcbFault)); 61 if (seL4_Fault_VGICMaintenance_get_idxValid(sender->tcbFault)) { 63 seL4_Fault_VGICMaintenance_get_idx(sender->tcbFault)); 68 return setMR(receiver, receiveIPCBuffer, seL4_VCPUFault_HSR, seL4_Fault_VCPUFault_get_hsr(sender [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/riscv/api/ |
H A D | faults.c | 31 bool_t Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType) argument 43 Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType) argument 47 setMR(receiver, receiveIPCBuffer, seL4_VMFault_IP, getRestartPC(sender)); 49 seL4_Fault_VMFault_get_instructionFault(sender->tcbFault)); 51 seL4_Fault_VMFault_get_address(sender->tcbFault)); 53 seL4_Fault_VMFault_get_FSR(sender->tcbFault));
|
/seL4-l4v-10.1.1/seL4/src/api/ |
H A D | faults.c | 77 copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, MessageID_t id, word_t length) argument 86 word_t v = getRegister(sender, msgRegisters[i]); 91 word_t *sendBuf = lookupIPCBuffer(false, sender); 103 copyMRsFault(tcb_t *sender, tcb_t *receiver, MessageID_t id, argument 108 setRegister(receiver, msgRegisters[i], getRegister(sender, fault_messages[id][i])); 113 receiveIPCBuffer[i + 1] = getRegister(sender, fault_messages[id][i]); 119 handleFaultReply(tcb_t *receiver, tcb_t *sender) argument 122 seL4_MessageInfo_t tag = messageInfoFromWord(getRegister(sender, msgInfoRegister)); 132 copyMRsFaultReply(sender, receiver, MessageID_Syscall, MIN(length, n_syscallMessage)); 136 copyMRsFaultReply(sender, receive 192 setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer) argument [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/include/sel4/ |
H A D | syscalls.h | 48 * @param[out] sender The address to write sender information to. 49 * The sender information is the badge of the 51 * sender, or the notification word of the 61 seL4_Recv(seL4_CPtr src, seL4_Word* sender); 120 * @param[out] sender The address to write sender information to. 121 * The sender information is the badge of the 123 * sender, or the notification word of the 133 seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender); [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/api/ |
H A D | faults.c | 19 bool_t Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType) argument 31 Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType) argument 35 setMR(receiver, receiveIPCBuffer, seL4_VMFault_IP, getRestartPC(sender)); 37 seL4_Fault_VMFault_get_address(sender->tcbFault)); 39 seL4_Fault_VMFault_get_instructionFault(sender->tcbFault)); 41 seL4_Fault_VMFault_get_FSR(sender->tcbFault));
|
/seL4-l4v-10.1.1/seL4/src/object/ |
H A D | endpoint.c | 153 tcb_t *sender; local 160 sender = queue.head; 163 assert(sender); 166 queue = tcbEPDequeue(sender, queue); 173 /* Get sender IPC details */ 174 badge = thread_state_ptr_get_blockingIPCBadge(&sender->tcbState); 176 thread_state_ptr_get_blockingIPCCanGrant(&sender->tcbState); 179 doIPCTransfer(sender, epptr, badge, 182 do_call = thread_state_ptr_get_blockingIPCIsCall(&sender->tcbState); 185 seL4_Fault_get_seL4_FaultType(sender [all...] |
H A D | tcb.c | 266 setupCallerCap(tcb_t *sender, tcb_t *receiver) argument 271 setThreadState(sender, ThreadState_BlockedOnReply); 272 replySlot = TCB_PTR_CTE_PTR(sender, tcbReply); 277 assert(TCB_PTR(cap_reply_cap_get_capTCBPtr(masterCap)) == sender); 282 cteInsert(cap_reply_cap_new(false, TCB_REF(sender)), 332 copyMRs(tcb_t *sender, word_t *sendBuf, tcb_t *receiver, argument 340 getRegister(sender, msgRegisters[i]));
|
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/arm/sel4/arch/ |
H A D | syscalls.h | 82 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 98 /* Return back sender and message information. */ 99 if (sender) { 100 *sender = badge; 106 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 132 /* Return back sender and message information. */ 133 if (sender) { 134 *sender = badge; 140 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 156 /* Return back sender an 227 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) argument 259 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 483 seL4_Wait(seL4_CPtr src, seL4_Word *sender) argument 489 seL4_Poll(seL4_CPtr src, seL4_Word *sender) argument [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | syscalls.h | 341 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 353 if (sender) { 354 *sender = badge; 361 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 378 if (sender) { 379 *sender = badge; 386 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 398 if (sender) { 399 *sender = badge; 448 seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) argument 468 seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1) argument 508 seL4_VMEnter(seL4_Word *sender) argument [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/ |
H A D | syscalls.h | 87 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 103 if (sender) { 104 *sender = badge; 111 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 136 if (sender) { 137 *sender = badge; 144 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 160 if (sender) { 161 *sender = badge; 229 seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) argument 253 seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument 307 seL4_VMEnter(seL4_Word *sender) argument [all...] |
/seL4-l4v-10.1.1/seL4/include/kernel/ |
H A D | thread.h | 94 void doIPCTransfer(tcb_t *sender, endpoint_t *endpoint, 96 void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot); 97 void doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint, 100 void doFaultTransfer(word_t badge, tcb_t *sender, tcb_t *receiver,
|
/seL4-l4v-10.1.1/seL4/src/kernel/ |
H A D | thread.c | 102 doIPCTransfer(tcb_t *sender, endpoint_t *endpoint, word_t badge, argument 109 if (likely(seL4_Fault_get_seL4_FaultType(sender->tcbFault) == seL4_Fault_NullFault)) { 110 sendBuffer = lookupIPCBuffer(false, sender); 111 doNormalTransfer(sender, sendBuffer, endpoint, badge, grant, 114 doFaultTransfer(badge, sender, receiver, receiveBuffer); 119 doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot) argument 125 doIPCTransfer(sender, NULL, 0, true, receiver); 135 restart = handleFaultReply(receiver, sender); 147 doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint, argument 156 tag = messageInfoFromWord(getRegister(sender, msgInfoRegiste 180 doFaultTransfer(word_t badge, tcb_t *sender, tcb_t *receiver, word_t *receiverIPCBuffer) argument [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/riscv/sel4/arch/ |
H A D | syscalls.h | 229 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 245 /* Return back sender and message information. */ 246 if (sender) { 247 *sender = badge; 254 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 280 /* Return back sender and message information. */ 281 if (sender) { 282 *sender = badge; 288 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 304 /* Return back sender an 334 seL4_Wait(seL4_CPtr src, seL4_Word *sender) argument 340 seL4_Poll(seL4_CPtr src, seL4_Word *sender) argument 388 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) argument 422 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument [all...] |
/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/ |
H A D | EventTo.c | 911 sender 1063 /* Return back sender and message information. */ 1066 sender 1070 sender 1089 sender 1241 /* Return back sender and message information. */ 1244 sender 1248 sender
|
H A D | RPCFrom.c | 1143 sender 1295 /* Return back sender and message information. */ 1298 sender 1302 sender 1321 sender 1473 /* Return back sender and message information. */ 1476 sender 1480 sender 1689 sender 1863 /* Return back sender an [all...] |
H A D | RPCTo.c | 1031 sender 1183 /* Return back sender and message information. */ 1186 sender 1190 sender 1212 sender 1386 /* Return back sender and message information. */ 1389 sender 1393 sender
|
/seL4-l4v-10.1.1/seL4/include/object/ |
H A D | tcb.h | 84 void setupCallerCap(tcb_t *sender, tcb_t *receiver); 87 word_t copyMRs(tcb_t *sender, word_t *sendBuf, tcb_t *receiver,
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | ipc.tex | 113 no sender is ready, threads performing the \apifunc{seL4\_Recv}{sel4_recv} 115 will wait for the first available sender. 178 third capability in the sender's message which could not be unwrapped.
|
H A D | notifications.tex | 39 If the signal sender capability was unbadged or 0-badged, the operation degrades
|
H A D | objects.tex | 152 to the receiver, giving the latter the right to reply to the original sender. The reply 175 messages through endpoints or notifications. If no sender or 241 a sender and a receiver rendezvous at the endpoint, and the
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/executable-semantics/ |
H A D | test2.v | 2 // with sender, BUF, receiver clocked on clk1, clk2, clk3 respectively.
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | jiraver443.c | 269 static inline seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender) { argument 289 /* Return back sender and message information. */ 290 if (sender) { 291 *sender = src_and_badge;
|