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