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 …
[View More]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.
[View Less]
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
…
[View More]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
[View Less]
Hey guys,
I've been attempting to put together some rust bindings for the seL4 fault
handling mechanisms, and I'm afraid the bitfield generator is driving me a
bit up a wall at this point. I'd like to find a concise grammar for the
language so I can better understand how bitfield_gen.py works, but there
doesn't seem to be any explicit BNF for it anywhere.
Is there a paper I should be reading or a reference guide somewhere that
would help?
Thanks!
--
June Tate-Gans
Software Engineer
…
[View More]Techlead, Kata OS / AmbiML, Google
[View Less]
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 …
[View More]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
[View Less]
One week to go to submit a talk for seL4 summit 2023 [0]!
If you'd like to submit a talk, please upload an abstract of one page or less to the submission portal [1].
The seL4 Summit 2023 will be held 19 - 21 September 2023 at the Elliot Park Hotel, Minneapolis, USA. The summit will be hosted by the Linux Foundation, and will be an in-person event. Registration details to follow soon.
We're looking forward to many exciting proposals!
[0] https://sel4.systems/Foundation/Summit/2023/cfp
[1] …
[View More]https://sel4.systems/Foundation/Summit/2023/submit
---
Dr. Birgit Brecknell
Project Officer
Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au>
seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems>
0433 880 571
Mon 9am-5pm
Wed 9am-12pm
Fri 9am-5pm
[View Less]
