February 2017 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

ARM timer driver and interrupts
by Wladislav Wiebe 01 Mar '17

01 Mar '17

Hello, I wrote a new timer driver for this timer device: http://www.ti.com/lit/ug/sprugv5a/sprugv5a.pdf I am already able to run the seL4 testsuite successfully, except the interrupt/timer tests. It waits forever @ wait_for_timer_interrupt(env); I've uploaded the driver temporary to: https://github.com/wwladikw/devel/blob/master/timer.c Any idea what could be wrong? I am able to run the timer periodically or as oneshot. The gic_390 interrupt driver in the kernel should also be compatible with the gic_400, for my understanding, right? The SoC I am using contains a Coretex A15. Thanks a lot in advance! Wladislav Wiebe

3 9

Boot Hyp mode in elfloader
by SHI, Yao 27 Feb '17

27 Feb '17

I am trying to boot CAmkES-ARM-VM and got problem in elfloader. I tested Jetson-TK1 and TK1-SOM. The results are same. I've set bootm_boot_mode=nonsec in u-boot and tracked registers in function switch_to_hyp_mode(). 1) Enter switch_to_hyp_mode(), after asm volatile ("mrc p15, 0, %0, c1, c1, 0":"=r"(scr)); ==> scr == 0x100, in which NS==0, HCE==1, SCD==0, SIF==0 2) Then switch_to_hyp_mode() changes NS to 1, so scr==0x101 asm volatile ("mcr p15, 0, %0, c1, c1, 0"::"r"(scr)); 3) switch_to_hyp_mode() changes cpsr to Hyp mode asm volatile ("cps %0\n\t" "isb\n" ::"I"(HYPERVISOR_MODE)); 4) The final step, switch_to_hyp_mode() reads cpsr, asm volatile ("mrs %0, cpsr":"=r"(scr)); ==> scr == 0x6000001da, in which cpsr.M==0x1a, cpsr.I==1, cpsr.F==1, cpsr.A==1 Finally, the process died here. My questions are, 1) Are NS==0 and HCE==1 correct when entering switch_to_hyp_mode() ? 2) Is the final status (cpsr.F==cpsr.I==cpsr.A==1) expected? 3) Any other mistake I might make? Yao

2 4

Clarification on seL4 on RPi3b
by Joseph Adam Powers 23 Feb '17

23 Feb '17

It seems to be necessary for me to use the debug output using a serial cable on UART0 u-boot seems to be waiting for a Ethernet or serial cable connection to finish boot process. I don't have the serial cable so I just need some understanding that that is the case considering that I followed the rest of the instructions on the blog at https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ , newbie question btw.

2 1

RT and domains
by rad021993＠yandex.ru 22 Feb '17

22 Feb '17

Hi, Could you tell me why did you not implement domains in RT kernel version? Are there any difficulties? I'm going to add support of domains, and at the first sight I don't see any difficulties.

3 3

seL4 no longer support zynq7000 board?
by wang 22 Feb '17

22 Feb '17

Hello, https://wiki.sel4.systems/Hardware On this seL4wiki hardware page I find the link of Zynq7000 turns grey, and the page says "This page does not exist yet. You can create a new empty page, or use one of the page templates." So it means seL4 do not support zynq7000 any more? And how can I run seL4/seL4test on zynq7000 board? Thanks!

2 1

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

camkes DMA with predetermined physical addresses
by Gareth Howard 17 Feb '17

17 Feb '17

1 0