August 2018 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 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

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

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

18 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

Network lwip for imx6
by wong xuguo 10 Dec '18

10 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

seL4 - getting the execution time of different threads
by Mr. Peace 10 Sep '18

10 Sep '18

Hello together, I was wondering how you do get the execution time in seL4 if you are using multiple threads. In the initial thread I can use the timer as it is shown in the tutorial about timers since I do have the bootinfo, vka, allocman and so on. But how do I use the timer to measure the execution time of the other threads without stopping their execution to "pull" the time from the initial thread? Is it possible to share the timer or create new ones in the other threads? Or is there another way to measure the execution time? Some background information: The threads have different VSpace's and CSpace's. Used tutorials: seL4-tutorial 4, seL4-tutorial timer. The other threads do not have a bootinfo in their environment. Kind regards, Chris

4 5

Does seL4 support raspberry pi 3B+
by talos 04 Sep '18

04 Sep '18

Hi I saw that seL4 supported raspberry pi 3B, did it support 3B+ now? If it did not, how can I modify it for 3B+? Thanks! Sincerely

2 1

SMC in seL4
by 冀东旭 31 Aug '18

31 Aug '18

Hello, I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode directly using the functions "install_monitor_hook()" and “switch_to_mon_mode()”. Is the sp in monitor mode appropriate? After calling smc in SVC mode, it hangs(do nothing in smc_handle()). What's wrong with it? Do you have any ideas? Thank you! Dongxu Ji

2 1

seL4 benchmark configure
by 송대영 30 Aug '18

30 Aug '18

Hi, I want to change seL4 benchmark configuration in ninja build tool. First, I want to change seL4's cache use. Sencond, I want to change CPU core number. How can I change these configuration?

2 1

32 bit vs 64 bit
by Chris Rothrock 30 Aug '18

30 Aug '18

When building the x86 demo for both 32 and 64 bit builds, it looks like the kernel is still a 32 bit elf file regardless of the build and only the sel4test-driver file is what is either 32 bit or 64 bit depending on which is selected. Is this normal or should the kernel also be 64 bit on the 64 bit build? -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 1

Fwd: SMC in seL4
by Dongxu Ji 29 Aug '18

29 Aug '18

Hi Yanyan, 1. It doesn't set the NS bit to 1 in SCR(I just want it to return without do anything). The arm_monitor_vector and the smc_handler(): arm_monitor_vector: ldr pc, [pc, #28] ldr pc, [pc, #24] ldr pc, =smc_handler ldr pc, [pc, #16] ldr pc, [pc, #12] ldr pc, [pc, #8] ldr pc, [pc, #4] ldr pc, [pc, #0] smc_handler: movs pc, lr 2. I didn't do any extra work other than the boot log: .......... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..203fbfff] ELF-loading image 'kernel' paddr=[10000000..10026fff] vaddr=[e0000000..e0026fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[10027000..10500fff] vaddr=[8000..4e1fff] virt_entry=25a6c Enabling MMU and paging Jumping to kernel-image entry point... 3. The initialization operations in platform_init.c: set sp: #define MONITOR_MODE (0x16) #define MON_VECTOR_START (0x11000000) #define VECTOR_BASE 0x11000000 #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) asm volatile ( "mrs r1, cpsr\n\t" "cps %0\n\t" "isb\n" "mov sp, %1\n\t" "msr cpsr, r1\n\t" ::"I"(MONITOR_MODE),"r"(STACK_TOP)); copy monitor mode vector to MON_VECTOR_START and write into MVBAR: uint32_t size = arm_monitor_vector_end - arm_monitor_vector; printf("Copy monitor mode vector from %x to %x size %x\n", (arm_monitor_vector), MON_VECTOR_START, size); memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size); asm volatile ("dmb\n isb\n"); asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START)); I enter into SVC mode by software interrupt and call the function smc(): asm (".arch_extension sec\n"); asm volatile ("stmfd sp!, {r3-r11, lr}\n\t" "dsb\n" "smc #0\n" "ldmfd sp!, {r3-r11, pc}"); and then the problem arises. Thank you, Dongxu Ji <Yanyan.Shen(a)data61.csiro.au> 于2018年8月28日周二下午8:30写道： > Hi, > > The smc_handle() in monitor.S, it does nothing but "movs pc, lr". > > Does it set the NS bit to 1 in SCR? > > Also, what did you do to ensure that 0x11000000 is not used by the kernel? > > Could you share the code (if possible) so that I could better understand > the problem. > > Regards, > Yanyan > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of 冀东旭 < > jidongxu1993(a)gmail.com> > *Sent:* Tuesday, August 28, 2018 1:02 PM > *To:* devel(a)sel4.systems > *Subject:* [seL4] SMC in seL4 > > Hello, > > I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode by setting the sp to STACK_TOP and copying arm_monitor_vector to MON_VECTOR_START according to the functions "install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c". > > #define VECTOR_BASE 0x11000000(addr is not used by the seL4 kernel) > > #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) > > #define MON_VECTOR_START 0x11000000(The VECTOR_BASE is the same as MON_VECTOR_START) > > The smc_handle() in monitor.S, it does nothing but "movs pc, lr". After calling smc in SVC mode, it hangs without any log. If I comment the "smc #0", it can return the caller successfully in usr mode. > > stmfd sp!, {r3-r11, lr} > dsb > smc #0 > ldmfd sp!, {r3-r11, pc} > > Is the sp in monitor mode appropriate? Or I need to do something else in initialization operations? What's wrong with it? Do you have any ideas? > > Thank you! > > Dongxu Ji > >

2 2