seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
24 stars 60 forks source link

Create thread with setting pc and call seL4_Send cause vm fault #84

Closed lingcs00 closed 1 year ago

lingcs00 commented 1 year ago

when i creat thread in the end of main.c(sel4test-driver) like this:

//for simple test my code use InitThreadVSpace,not really ipc
seL4_TCB_Configure(new_tcb[0].cptr,0,seL4_CapInitThreadCNode,0,seL4_CapInitThreadVSpace,0, 
                                 (seL4_Word)new_ipc_frame_va,new_ipc_frame.cptr);    
seL4_UserContext regs = {};
sel4utils_arch_init_local_context(thread1,(void *)1,(void *)2,(void *)3,new_stack_top ,&regs);
seL4_Error err = seL4_TCB_WriteRegisters(new_tcp.cptr, true, 0, sizeof(regs)/sizeof(seL4_Word), &regs);

In thread1 function code like this:

printf("thread1 run\n");
seL4_Send(new_ep.cptr,seL4_MessageInfo_new(0,0,0,0));

I will get vm fault because __sel4_ipc_buffer is thread local variable. I guess that i creat the thread1 with set pc = thread1 and not init the thread local variable. But actually i alloc the ipc buffer and set successfully,i wanna know that the situation is seL4_Send function bug or feature?

kent-mcleod commented 1 year ago

There's another invocation for setting the thread local storage area seL4_TCB_SetTLSBase: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/src/thread.c#L189.

The top of sel4utils_start_thread() shows how you can set up the __sel4_ipc_buffer address when starting a new thread: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/src/thread.c#L163-L172