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




________________________________
This message and all attachments are PRIVATE, and contain information that is 
PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit 
or otherwise disclose this message or any attachments to any third party 
whatsoever without the express written consent of Intelligent Automation, Inc. 
If you received this message in error or you are not willing to view this 
message or any attachments on a confidential basis, please immediately delete 
this email and any attachments and notify Intelligent Automation, Inc.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to