[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(, info); /* create an allocator */ allocman = bootstrap_use_current_simple(, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); /* create a vka */ allocman_make_vka(, allocman); /* create a vspace */ error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(, , simple_get_pd(), , platsupport_get_bootinfo()); /* fill the allocator with virtual memory */ void *vaddr; virtual_reservation = vspace_reserve_range(, ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_AllRights, 1, ); 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()); /* Allocate slots for, and obtain the caps for, the hardware we will be * using, in the same function. */ sel4platsupport_init_default_serial_caps(, , , _objects); vka_t serial_vka = env.vka; serial_vka.utspace_alloc_at = arch_get_serial_utspace_alloc_at(); /* Construct a simple wrapper for returning the I/O ports. */ simple_t serial_simple = env.simple; /* enable serial driver */ platsupport_serial_setup_simple(, _simple, _vka); simple_print(); /* get our cspace root cnode */ seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(); /* get our vspace root page diretory */ seL4_CPtr pd_cap; pd_cap = simple_get_pd(); /* create a new TCB */ vka_object_t tcb_object = {0}; error = vka_alloc_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(, (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(, thread_2_stack_top); error=sel4utils_get_sp(regs); /* actually write the TCB registers. */ error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, ); /* 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 1208 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
Re: [seL4] SMC in seL4
Hi Yanyan, According to your advice,I modified the avail_p_regs[] in hardware.h file as tk1. 1 MiB starting from 0x37f0 is reserved for monitor mode. { /* .start = */ 0x1000, /* .end = */ 0x37f0} And then #define MON_PA_START (0x1000 + 0x27f0) #define MON_PA_SIZE (1 << 20) #define MON_PA_END (MON_PA_START + MON_PA_SIZE) #define MON_PA_STACK (MON_PA_END - 0x10) #define MON_VECTOR_START (MON_PA_START) set sp: asm volatile ("cps %0\n\t" "isb\n" "mov sp, %1\n\t" ::"I"(MONITOR_MODE),"r"(MON_PA_STACK)); copy monitor mode vector and write into MVBAR: uint32_t size = arm_monitor_vector_end - arm_monitor_vector; printf("Copy monitor mode vector from %x to %x size %x \n", (arm_monitor_vector), MON_VECTOR_START, size); memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size); asm volatile ("dmb\n isb\n"); asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START)); I used the arm_monitor_vector provided by the source code in monitor.S and just didn't perform the operation 'blx r0'. I think the it can jump to smc_handler and return successfully. #define VECTOR_BASE 0x37f0 #define STACK_TOP (VECTOR_BASE + (1 << 20) - 0x10) arm_monitor_vector: ldr pc, [pc, #28] ldr pc, [pc, #24] ldr pc, [pc, #16] ldr pc, [pc, #16] ldr pc, [pc, #12] ldr pc, [pc, #8] ldr pc, [pc, #4] ldr pc, [pc, #0] smc_handler_addr: .word VECTOR_BASE + (smc_handler - arm_monitor_vector)//0x102c smc_halt_addr: .word VECTOR_BASE + (smc_halt - arm_monitor_vector) smc_stack: .word STACK_TOP smc_handler: /* always have a valid stack */ ldr sp, [pc, #-12] push {lr} //blx r0 isb mrc p15, 0, r5, c1, c1, 0 /* set the NS bit */ orr r5, r5, #1 mcr p15, 0, r5, c1, c1, 0 pop {lr} isb movs pc, lr However, the problem still exists. And I have another question that why set the sp in monitor mode to sp in SVC mode. asm volatile ("mov r8, sp\n\t" "cps %0\n\t" "isb\n" "mov sp, r8\n\t" ::"I"(MONITOR_MODE)); Thank you, Dongxu Ji 于2018年8月28日周二 下午10:10写道: > Hi Dongxu, > > > As you can see, the arm_monitor_vector uses PC-relative addressing so that > the code can be moved around in memory. I think ldr pc, =smc_handler > breaks this. Also, please set the NS bit in SCR to 1 before returning. > > > To reserve a memory region for the monitor-mode code and data, I suggest > you modify the avail_p_regs[] in > kernel/include/plat/imx6/plat/machine/hardware.h > file. See the kernel/include/plat/tk1/plat/machine/hardware.h as an example. > > > > > Regards, > > Yanyan > > > -- > *From:* Dongxu Ji > *Sent:* Wednesday, August 29, 2018 12:02 AM > *To:* devel@sel4.systems; Shen, Yanyan (Data61, Kensington NSW) > *Subject:* Fwd: [seL4] SMC in seL4 > > Hi Yanyan, > 1. It doesn't set the NS bit to 1 in SCR(I just want it to return without > do anything). The arm_monitor_vector and the smc_handler(): > > arm_monitor_vector: > ldr pc, [pc, #28] > ldr pc, [pc, #24] > ldr pc, =smc_handler > ldr pc, [pc, #16] > ldr pc, [pc, #12] > ldr pc, [pc, #8] > ldr pc, [pc, #4] > ldr pc, [pc, #0] > > smc_handler: > movs pc, lr > > 2. I didn't do any extra work other than the boot log: > > .. > ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 > > paddr=[2000..203fbfff] > > ELF-loading image 'kernel' > > paddr=[1000..10026fff] > > vaddr=[e000..e0026fff] > > virt_entry=e000 > > ELF-loading image 'sel4test-driver' > > paddr=[10027000..10500fff] > > vaddr=[8000..4e1fff] > > virt_entry=25a6c > > Enabling MMU and paging > > Jumping to kernel-image entry point... > > 3. The initialization operations in platform_init.c: > set sp: > #define MONITOR_MODE(0x16) > #define MON_VECTOR_START(0x1100) > #define VECTOR_BASE 0x1100 > #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) > > asm volatile ( "mrs r1, cpsr\n\t" > "cps %0\n\t" > "isb\n" > "mov sp, %1\n\t" > "msr cpsr, r1\n\t" > ::"I"(MONITOR_MODE),"r"(STACK_TOP)); > > copy monitor mode vector to MON_VECTOR_START and write into MVBAR: > uint32_t size = arm_monitor_vector_end - arm_monitor_vector;
[seL4] Fwd: SMC in seL4
Hi Yanyan, 1. It doesn't set the NS bit to 1 in SCR(I just want it to return without do anything). The arm_monitor_vector and the smc_handler(): arm_monitor_vector: ldr pc, [pc, #28] ldr pc, [pc, #24] ldr pc, =smc_handler ldr pc, [pc, #16] ldr pc, [pc, #12] ldr pc, [pc, #8] ldr pc, [pc, #4] ldr pc, [pc, #0] smc_handler: movs pc, lr 2. I didn't do any extra work other than the boot log: .. ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[2000..203fbfff] ELF-loading image 'kernel' paddr=[1000..10026fff] vaddr=[e000..e0026fff] virt_entry=e000 ELF-loading image 'sel4test-driver' paddr=[10027000..10500fff] vaddr=[8000..4e1fff] virt_entry=25a6c Enabling MMU and paging Jumping to kernel-image entry point... 3. The initialization operations in platform_init.c: set sp: #define MONITOR_MODE(0x16) #define MON_VECTOR_START(0x1100) #define VECTOR_BASE 0x1100 #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) asm volatile ( "mrs r1, cpsr\n\t" "cps %0\n\t" "isb\n" "mov sp, %1\n\t" "msr cpsr, r1\n\t" ::"I"(MONITOR_MODE),"r"(STACK_TOP)); copy monitor mode vector to MON_VECTOR_START and write into MVBAR: uint32_t size = arm_monitor_vector_end - arm_monitor_vector; printf("Copy monitor mode vector from %x to %x size %x\n", (arm_monitor_vector), MON_VECTOR_START, size); memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size); asm volatile ("dmb\n isb\n"); asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START)); I enter into SVC mode by software interrupt and call the function smc(): asm (".arch_extension sec\n"); asm volatile ("stmfdsp!, {r3-r11, lr}\n\t" "dsb\n" "smc #0\n" "ldmfdsp!, {r3-r11, pc}"); and then the problem arises. Thank you, Dongxu Ji 于2018年8月28日周二 下午8:30写道: > Hi, > > The smc_handle() in monitor.S, it does nothing but "movs pc, lr". > > Does it set the NS bit to 1 in SCR? > > Also, what did you do to ensure that 0x1100 is not used by the kernel? > > Could you share the code (if possible) so that I could better understand > the problem. > > Regards, > Yanyan > > > -- > *From:* Devel on behalf of 冀东旭 < > jidongxu1...@gmail.com> > *Sent:* Tuesday, August 28, 2018 1:02 PM > *To:* devel@sel4.systems > *Subject:* [seL4] SMC in seL4 > > Hello, > > I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I > initialize the monitor mode by setting the sp to STACK_TOP and copying > arm_monitor_vector to MON_VECTOR_START according to the functions > "install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c". > > #define VECTOR_BASE 0x1100(addr is not used by the seL4 kernel) > > #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) > > #define MON_VECTOR_START0x1100(The VECTOR_BASE is the same as > MON_VECTOR_START) > > The smc_handle() in monitor.S, it does nothing but "movs pc, lr". After > calling smc in SVC mode, it hangs without any log. If I comment the "smc > #0", it can return the caller successfully in usr mode. > > stmfdsp!, {r3-r11, lr} > dsb > smc #0 > ldmfdsp!, {r3-r11, pc} > > Is the sp in monitor mode appropriate? Or I need to do something else in > initialization operations? What's wrong with it? Do you have any ideas? > > Thank you! > > Dongxu Ji > > ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel