March 2019 - 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

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

16 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 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

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Sel4 for quadcore riscv64imafd
by Sreenadh S 03 Oct '19

03 Oct '19

I want to build sel4 for quadcore riscv64imafd and run the test programs, how to do that? Regards, Sreenadh S, CDAC, Trivandrum, India

2 1

Interested in Contributing to SeL4
by Aditya Upadhyay 26 Mar '19

26 Mar '19

Hi Developers, This is Aditya Upadhyay, would like to contribute in SeL4 microkernel. I am trying to figure out any open projects on wiki page of SeL4 Systems. One project that is related to POSIX Compliance. I can see here: https://docs.sel4.systems/SuggestedProjects.html but I am still figuring out the stuff to contribute. Any Valuable suggestions would be appreciated. Would you like to point any blogs related to SeL4? I have some experience of contributing the code in Open Source Organisation Newlib-Cygwin. I was working on POSIX Compliance for RTEMS as a part of Google Summer of Code 2017 Students internship. To stick to Open Source, I am mentoring RTEMS Google Summer of Code Project this year also. I have always learned from mentoring and contributing to open source. I have deep understanding of Linux Operating System Internals and Monolithic Kernels as well. I am also looking for Research Internship in Distributed Systems especially in Microkernel and Microhypervisor field. I am open for any research oriented projects in this field. Regards, Aditya Upadhyay

3 2

Re: [seL4] Devel Digest, Vol 58, Issue 5
by KIM MK 26 Mar '19

26 Mar '19

Okay! Aditya, Let’s research together :) BR, MK Sent from my iPhone > On 26 Mar 2019, at 6:43 AM, "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: some questions about camkes-manifest > (Anna.Lyons(a)data61.csiro.au) > 2. Interested in Contributing to SeL4 (Aditya Upadhyay) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 25 Mar 2019 02:23:22 +0000 > From: <Anna.Lyons(a)data61.csiro.au> > To: <yadong.li(a)horizon.ai>, <devel(a)sel4.systems> > Subject: Re: [seL4] some questions about camkes-manifest > Message-ID: <1553480602203.73891(a)data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi, > > > 1. You can find the library in https://github.com/SEL4PROJ/projects_libs? > > 2. Sorry, we do not have any public demos that use this library. It has mainly been used in experimental contexts. > > > Cheers > > Anna. > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://sel4.systems/pipermail/devel/attachments/20190325/580f5330/attachmen…> > > ------------------------------ > > Message: 2 > Date: Mon, 25 Mar 2019 22:01:09 +0530 > From: Aditya Upadhyay <aditya.sidd.upadhyay(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Interested in Contributing to SeL4 > Message-ID: > <CAP7bF08qCr2dxd=WwbRwKuJP8ZqNc1RswNJbsfnyZ5Dxg1rjCg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Hi Developers, > > This is Aditya Upadhyay, would like to contribute in SeL4 microkernel. > > I am trying to figure out any open projects on wiki page of SeL4 Systems. > One project that is related to POSIX Compliance. I can see here: > https://docs.sel4.systems/SuggestedProjects.html > but I am still figuring out the stuff to contribute. Any Valuable > suggestions would be appreciated. Would you like to point any blogs related > to SeL4? > > I have some experience of contributing the code in Open Source Organisation > Newlib-Cygwin. I was working on POSIX Compliance for RTEMS as a part of > Google Summer of Code 2017 Students internship. > > To stick to Open Source, I am mentoring RTEMS Google Summer of Code Project > this year also. I have always learned from mentoring and contributing to > open source. > > I have deep understanding of Linux Operating System Internals and > Monolithic Kernels as well. I am also looking for Research Internship in > Distributed Systems especially in Microkernel and Microhypervisor field. I > am open for any research oriented projects in this field. > > Regards, > Aditya Upadhyay > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://sel4.systems/pipermail/devel/attachments/20190325/3cbbe26b/attachmen…> > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 58, Issue 5 > ************************************

1 0

speed up sel4
by Sreenadh S 26 Mar '19

26 Mar '19

When running sel4 in my processor it is taking too long to get this line "vka_alloc_object_at_maybe_dev@object.h:65 Failed to allocate object of size 268435456, error 1" Is there any options to reduce allocation object size? Or any other methods to speed up Regards, Sreenadh S CDAC, Trivandrum, India

2 1

some questions about camkes-manifest
by yadong.li 25 Mar '19

25 Mar '19

hi, I have some questions about camkes-manifest 1、I find the libsdhcdrivers in /projects/projects_libs of the project. But where can I find the superset of these libs by git? I can't find the maintenance branch about libsdhcdrivers (like 'seL4_libs' ) in https://github.com/seL4 2、I can't find who use the function of libsdhcdrivers, what is the plan of the lib ? Is there some demo using sdhc ? Thank you very much

2 1

Hello. Nice to meet you. I’m MK
by KIM MK 11 Mar '19

11 Mar '19

Hello Micro kernel develper I’m MK. Nice to meet u. I’ll research and commit ARMv8 and virtualization in Sel4 你好。谢谢。 반갑습니다 Thank you BR， MK Sent from my iPhone

1 0