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
