Hello,

My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial thread:

    int err;

    seL4_timer_t timer;

    vka_object_t ntfn_object;

    ntfn_object.cptr = 0;

    err = vka_alloc_notification(&_env.vka, &ntfn_object);

    assert(err == 0);

        err = sel4platsupport_init_default_timer(&_env.vka, &_env.vspace, &_env.simple, ntfn_object.cptr, &timer);

        err = ltimer_set_timeout(&timer.ltimer, NS_IN_MS * 20, TIMEOUT_PERIODIC);

        assert(err == 0);

        int count = 0;

        int count_s = 0;

        while (1) {

            /* Handle the timer interrupt */

            seL4_Word badge;

            seL4_Wait(ntfn_object.cptr, &badge);

            printf("time_thread: badge=%lx\n", badge);

            sel4platsupport_handle_timer_irq(&timer, badge);

            count++;

            if ((count / 50) * 50 == count)

            {

               count_s++;

               printf("-----------------timer=%d  %d\n", count, count_s);

            }

        }

It works fine (I am not sure why TIMESTAMP timer interrupt coming every ~40 sec, but it’s not an issue right now)

Now I am trying to move all this timer code into a new thread, which I have created in the same vspace

// create thread

void initSleep(env_t penv) //seL4_BootInfo *info)

{

                _penv = penv;

                vka_object_t tcb_object = {0};

                int error = vka_alloc_tcb(&penv->vka, &tcb_object);

    seL4_CPtr cspace_cap;

    cspace_cap = simple_get_cnode(&penv->simple);

    seL4_CPtr pd_cap;

    pd_cap = simple_get_pd(&penv->simple);

                seL4_CPtr ipc_page;

                seL4_Word ipc_buffer = (seL4_Word)vspace_new_ipc_buffer(&penv->vspace, &ipc_page);

                error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page);

                error = seL4_TCB_SetPriority(tcb_object.cptr, simple_get_tcb(&penv->simple), seL4_MaxPrio);

                seL4_UserContext regs = {

                                                .pc = (seL4_Word)time_thread,

                                                .sp = (seL4_Word)thread_time_stack

                };

                error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs);

                error = seL4_TCB_Resume(tcb_object.cptr);

}

And this is thread function

static void time_thread(void)

{

                _tick_number = 0;

                int count_s = 0;

                init_timer();

    while (1)

    {

        /* Handle the timer interrupt */

        seL4_Word badge;

        seL4_Wait(timer_ntfn_object.cptr, &badge);

        printf("time_thread: badge=%lx\n", badge);

        sel4platsupport_handle_timer_irq(&timer, badge);

        _tick_number++;

        if ((_tick_number / 50) * 50 == _tick_number)

        {

               count_s++;

               printf("-----------------timer=%lu  %d\n", _tick_number, count_s);

        }

}

The system crashed:

setup_irq@timer.c:81 Setting up IRQ 8000000000000000

<<seL4(CPU 0) [handleInvocation/281 T0xff8000001200 "child of: 'rootserver'" @42195c]: Invocation of invalid cap #48762580.>>

Here is dump:

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/functions.h:23

  421938:       d53bd066        mrs     x6, tpidrro_el0

setup_irq():

/home/lm/sel4vm/libs/libsel4platsupport/src/timer.c:85

        error =  seL4_IRQHandler_SetNotification(irq->handler_path.capPtr, irq->badged_ntfn_path.capPtr);

  42193c:       f85c8340        ldur    x0, [x26,#-56]

arm_sys_send_recv():

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165

    register seL4_Word msg1 asm("x3") = *in_out_mr1;

  421940:       d2800003        mov     x3, #0x0                        // #0

seL4_SetCap():

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59

  421944:       f901e8c1        str     x1, [x6,#976]

arm_sys_send_recv():

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:166

    register seL4_Word msg2 asm("x4") = *in_out_mr2;

  421948:       d2800004        mov     x4, #0x0                        // #0

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:167

    register seL4_Word msg3 asm("x5") = *in_out_mr3;

  42194c:       d2800005        mov     x5, #0x0                        // #0

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:170

    register seL4_Word scno asm("x7") = sys;

  421950:       92800007        mov     x7, #0xffffffffffffffff         // #-1

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:161

    register seL4_Word info asm("x1") = info_arg;

  421954:       d2941001        mov     x1, #0xa080                     // #41088

  421958:       f2a00021        movk    x1, #0x1, lsl #16

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:171

    asm volatile (

  42195c:       d4000002        hvc     #0x0

seL4_MessageInfo_get_label():

/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/shared_types_gen.h:49

I suspect that  my thread initialization is not right, can somebody see any problem?

Thank you,

Leonid