Hi Adam, Thank you for your reply. I tried to continue to do the tutorial 3. The tutorial 3 is based on the tutorial 2 but adds an endpoint for IPC between the main thread and the child thread. Surprisingly, it works as expected:
main: hello world thread_2: hallo wereld thread_2: got a message 0x6161 from 0x61 main: got a reply: 0xffff9e9e I think this issue is similar to the previous one [1]. Regards, Dongxu Ji [1] http://sel4.systems/pipermail/devel/2018-May/001956.html <adam.feli...@data61.csiro.au> 于2018年9月24日周一 上午9:31写道： > Hi Dongxu, > > > Apologies for the late reply. If your working in the seL4test project with > the adapted sel4 tutorial code, the two things I would try are: > > > - Making sure you register a stdio write function e.g > > size_t kernel_putchar_write(void *data, size_t count) { > char *cdata = (char*)data; > for (size_t i = 0; i < count; i++) { > seL4_DebugPutChar(cdata[i]); > } > return count; > } > > void CONSTRUCTOR(200) register_putchar(void) { > sel4muslcsys_register_stdio_write_fn(kernel_putchar_write); > } > > - Disable the 'LibSel4MuslcSysDebugHalt' cmake option. By default this > would enabled in the sel4test project, however your root-server may > possibly be aborting before you can see thread_2's printing. > > > Kind Regards, > > Adam > > > ------------------------------ > *From:* Devel <devel-bounces@sel4.systems> on behalf of Dongxu Ji < > jidongxu1...@gmail.com> > *Sent:* Wednesday, 19 September 2018 12:24 PM > *To:* devel@sel4.systems > *Subject:* [seL4] create a new thread in sel4 > > Hello, > My platform is imx6q sabrelite and I have run sel4-test successfully. Now > I'm trying to create a new thread in the initial thread according to sel4 > tutorial2. But it didn't run. > > The code is shown below: > > struct driver_env env; > allocman_t *allocman; > > /* function to run in the new thread */ > void thread_2(void) { > > printf("thread_2: hallo wereld\n"); > > while (1); > } > > int main(void) > { > int error; > reservation_t virtual_reservation; > seL4_BootInfo *info = platsupport_get_bootinfo(); > > seL4_DebugNameThread(seL4_CapInitThreadTCB, "sel4test-driver"); > > /* initialise libsel4simple */ > simple_default_init_bootinfo(&env.simple, info); > > /* create an allocator */ > allocman = bootstrap_use_current_simple(&env.simple, > ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); > > /* create a vka */ > allocman_make_vka(&env.vka, allocman); > > /* create a vspace */ > error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&env.vspace, > &data, > simple_get_pd(&env.simple), > &env.vka, > platsupport_get_bootinfo()); > > /* fill the allocator with virtual memory */ > void *vaddr; > virtual_reservation = vspace_reserve_range(&env.vspace, > > ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_AllRights, 1, &vaddr); > if (virtual_reservation.res == 0) { > ZF_LOGF("Failed to provide virtual memory for allocator"); > } > > bootstrap_configure_virtual_pool(allocman, vaddr, > ALLOCATOR_VIRTUAL_POOL_SIZE, > simple_get_pd(&env.simple)); > > /* Allocate slots for, and obtain the caps for, the hardware we will be > * using, in the same function. > */ > sel4platsupport_init_default_serial_caps(&env.vka, &env.vspace, > &env.simple, &env.serial_objects); > > vka_t serial_vka = env.vka; > serial_vka.utspace_alloc_at = arch_get_serial_utspace_alloc_at(&env); > > /* Construct a simple wrapper for returning the I/O ports. */ > simple_t serial_simple = env.simple; > > /* enable serial driver */ > platsupport_serial_setup_simple(&env.vspace, &serial_simple, > &serial_vka); > > simple_print(&env.simple); > > /* get our cspace root cnode */ > seL4_CPtr cspace_cap; > cspace_cap = simple_get_cnode(&env.simple); > > /* get our vspace root page diretory */ > seL4_CPtr pd_cap; > pd_cap = simple_get_pd(&env.simple); > > /* create a new TCB */ > vka_object_t tcb_object = {0}; > error = vka_alloc_tcb(&env.vka, &tcb_object); > > /* initialise the new TCB */ > error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, > seL4_NilData, pd_cap, seL4_NilData, 0, 0); > > /* give the new thread a name */ > name_thread(tcb_object.cptr, "hello-2: thread_2"); > > UNUSED seL4_UserContext regs = {0}; > > /* set instruction pointer where the thread shoud start running */ > sel4utils_set_instruction_pointer(®s, (seL4_Word)thread_2); > error=sel4utils_get_instruction_pointer(regs); > > /* check that stack is aligned correctly */ > const int stack_alignment_requirement = sizeof(seL4_Word) * 2; > uintptr_t thread_2_stack_top = (uintptr_t)thread_2_stack + > sizeof(thread_2_stack); > > /* set stack pointer for the new thread */ > sel4utils_set_stack_pointer(®s, thread_2_stack_top); > error=sel4utils_get_sp(regs); > > /* actually write the TCB registers. */ > error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, ®s); > > /* start the new thread running */ > error = seL4_TCB_Resume(tcb_object.cptr); > > /* we are done, say hello */ > printf("main: hello world \n"); > > return 0; > } > > And I can get some output: > cspace_cap is 2 > > pd_cap is 3 > > tcb_object.cptr is 5f7 > > tcb_object.ut is 10000208 > > tcb_object.type is 1 > > tcb_object.size_bits is a > regs.pc is > 9640 > regs.sp is 3f24f0 > > Any advice about the issue? > > Thank you, > Dongxu Ji > > > >
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
