seL4 on TX1 - Devel

28 Jan 2022


      Help me!
    I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port.
At the same time, I follow this instruction  ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format.
Then I use command `sudo screen / dev / ttyusb0 115200`  to open the UART serial port.  After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line.
Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000:
    ```
    ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
    go 0x82000000
    ```
    Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output：
------------------------------------------------------------------------------------------------------------------------------------------
    Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
    5247256 bytes read in 260 ms (19.2 MiB/s)
    Tegra210 (P2371-2180) # go 0x82000000
    ## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1
  paddr=[80a57000..80f58117]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 80b825e0.
Loaded DTB from 80b825e0.
   paddr=[8023d000..8024afff]
ELF-loading image 'kernel' to 80000000
  paddr=[80000000..8023cfff]
  vaddr=[ffffff8080000000..ffffff808023cfff]
  virt_entry=ffffff8080000000
ELF-loading image 'sel4test-driver' to 8024b000
  paddr=[8024b000..80661fff]
  vaddr=[400000..816fff]
  virt_entry=40f0b8
Enabling MMU and paging
Jumping to kernel-image entry point...
Warning:  gpt_cntfrq 19200000, expected 12000000
Bootstrapping kernel
available phys memory regions: 2
  [80000000..ff000000]
  [100000000..180000000]
reserved virt address space regions: 3
  [ffffff8080000000..ffffff808023d000]
  [ffffff808023d000..ffffff808024b000]
  [ffffff808024b000..ffffff8080662000]
seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert
halting...
Kernel entry via Interrupt, irq 0
------------------------------------------------------------------------------------------------------------------------------------------
I'm about to collapse. I really need your help. How can I solve this problem?
1. Why did I get this warning？ "Warning:  gpt_cntfrq 19200000, expected 12000000" ,  It exists in this file  "/sel4test/kernel/src/drivers/timer/generic_timer.c:21"
2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) )  -> cap.words[0] " is equals to  0xffffffffffffffff, so that the         cap_get_capType(destSlot->cap) <=>   (slot_ptr_t) (rootserver.tcb) )  -> cap.words[0]  & 0x1full  != 0 .     I guess it caused the mistake, but i don't know why.
I'm about to collapse. I really need your help. How can I solve this problem?
I'm sorry for sending this email again!