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.Felizzi@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 < jidongxu1993@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(&regs, (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(&regs, thread_2_stack_top);
error=sel4utils_get_sp(regs);

/* actually write the TCB registers. */
error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs);

/* 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